Paper "CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering" accepted at TACAS'20 and preprint available now!

Publications of year 2020

(All PublicationsIndex)

Books and proceedings

  1. Dirk Beyer and Damien Zufferey, editors.
    Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS 11990, 2020.
    Springer.
    [ Material ] [ Article ]
    @Proceedings{VMCAI20,
    editor = {Dirk Beyer and Damien Zufferey},
    title = {Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)},
    publisher = {Springer},
    series = {LNCS~11990},
    year = {2020},
    isbn = {978-3-030-39321-2},
    doi = {10.1007/978-3-030-39322-9},
    pdf = {https://doi.org/10.1007/978-3-030-39322-9},
    url = {https://popl20.sigplan.org/home/VMCAI-2020},
    
    }
    

Articles in conference or workshop proceedings

  1. Dirk Beyer.
    Advances in Automatic Software Verification: SV-COMP 2020.
    In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 2, LNCS 12079, 2020.
    Springer.
    [ Material ] [ Article ] Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking.
    Abstract


    @InProceedings{TACAS20c,
    author = {Dirk Beyer},
    title = {Advances in Automatic Software Verification: SV-COMP 2020},
    booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 2},
    series = {LNCS~12079},
    publisher = {Springer},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-TACAS.Advances_in_Automatic_Software_Verification_SV-COMP_2020.pdf},
    url = {https://sv-comp.sosy-lab.org/},
    keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking},
    abstract = { },
    
    }
    

  2. Dirk Beyer.
    Second Competition on Software Testing: Test-Comp 2020.
    In Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE 2020, Dublin, Ireland, April 25-30), LNCS 12076, 2020.
    Springer.
    [ Material ] [ Article ] Keyword(s): Competition on Software Testing (Test-Comp), Competition on Software Testing (Test-Comp Report), Software Testing.
    Abstract


    @InProceedings{FASE20,
    author = {Dirk Beyer},
    title = {Second Competition on Software Testing: Test-Comp 2020},
    booktitle = {Proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering (FASE~2020, Dublin, Ireland, April 25-30)},
    series = {LNCS~12076},
    publisher = {Springer},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-FASE.Second_Competition_on_Software_Testing_Test-Comp_2020.pdf},
    url = {https://test-comp.sosy-lab.org/},
    keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing},
    abstract = { },
    
    }
    

  3. Dirk Beyer and Matthias Dangl.
    Software Verification with PDR: An Implementation of the State of the Art.
    In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 1, LNCS 12078, 2020.
    Springer.
    [ Material ] [ Article ] Keyword(s): Software Model Checking.
    Abstract


    @InProceedings{TACAS20a,
    author = {Dirk Beyer and Matthias Dangl},
    title = {Software Verification with PDR: An Implementation of the State of the Art},
    booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 1},
    series = {LNCS~12078},
    publisher = {Springer},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-TACAS.Software_Verification_with_PDR_An_Implementation_of_the_State_of_the_Art.pdf},
    url = {https://www.sosy-lab.org/research/pdr-compare/},
    keyword = {Software Model Checking},
    abstract = { },
    
    }
    

  4. Dirk Beyer and Philipp Wendler.
    CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering.
    In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020, Dublin, Ireland, April 25-30), part 2, LNCS 12079, 2020.
    Springer.
    [ Material ] [ Article ] Keyword(s): Benchmarking.
    Abstract

    Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time.

    @InProceedings{TACAS20b,
    author = {Dirk Beyer and Philipp Wendler},
    title = {CPU Energy Meter: A Tool for Energy-Aware Algorithms Engineering},
    booktitle = {Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2020, Dublin, Ireland, April 25-30), part 2},
    series = {LNCS~12079},
    publisher = {Springer},
    pages = {},
    year = {2020},
    doi = {},
    pdf = {https://www.sosy-lab.org/research/pub/2020-TACAS.CPU_Energy_Meter_A_Tool_for_Energy-Aware_Algorithms_Engineering.pdf},
    url = {https://www.sosy-lab.org/research/energy-measurement/},
    keyword = {Benchmarking},
    abstract = { Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or even wall time). Perhaps one reason for this is that measuring energy consumption of computational processes is not as convenient as measuring the consumed time and there is no sufficient tool support. To close this gap, we contribute CPU Energy Meter, a small tool that takes care of reading the energy values that Intel CPUs track inside the chip. In order to make energy measurements as easy as possible, we integrated CPU Energy Meter into BenchExec, a benchmarking tool that is already used by many researchers and competitions in the domain of formal methods. As evidence for usefulness, we explored the energy consumption of some state-of-the-art verifiers and report some interesting insights, for example, that energy consumption is not necessarily correlated with CPU time. },
    
    }
    

Theses (PhD, MSc, BSc, Project)

  1. Alexander Ried.
    Design and Implementation of a Cluster-Based Approach for Software Verification.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2020.
    [ Article ] [ Presentation ] Keyword(s): CPAchecker, BAM, Akka.

    @misc{RiedClusterBAM,
    pdf = {https://www.sosy-lab.org/research/bsc/2020.Ried.Design_and_Implementation_of_a_Cluster_Based_Approach_for_Software_Verification.pdf},
    postscript = {https://www.sosy-lab.org/research/bsc/2020-01-29_BA_ClusterBasedSoftwareVerification_Ried.pdf},
    author = {Alexander Ried},
    title = {Design and Implementation of a Cluster-Based Approach for Software Verification},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2020},
    field = {Computer Science},
    keyword = {CPAchecker, BAM, Akka},
    
    }
    

(All PublicationsIndex)



Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.




Last modified: Fri Apr 10 00:20:37 2020


This document was translated from BibTEX by bibtex2html