Gastvorträge am Mittwoch 27.11.: "Klimawandel und Extremereignisse – neue Erkenntnisse für die Klimafolgenforschung durch die Nutzung von HPC" im Rahmen der Public Climate School von Students for Future Munich.

Publications of year 2017

(All PublicationsIndex)

Articles in journal or book chapters

  1. Dirk Beyer, Rolf Hennicker, Martin Hofmann, Tobias Nipkow, and Martin Wirsing.
    Software-Verifikation.
    In A. Bode, M. Broy, H.-J. Bungartz, and F. Matthes, editors, 50 Jahre Universitäts-Informatik in München, pages 75-86.
    Springer, 2017.
    [ Article ] Keyword(s): Software Model Checking.

    @InCollection{InfMUC17,
    author = {Dirk Beyer and Rolf Hennicker and Martin Hofmann and Tobias Nipkow and Martin Wirsing},
    title = {Software-Verifikation},
    booktitle = {50 Jahre Universit{\"a}ts-Informatik in M{\"u}nchen},
    editor = {A.~Bode and M.~Broy and H.-J.~Bungartz and F.~Matthes},
    publisher = {Springer},
    pages = {75-86},
    year = {2017},
    isbn = {978-3-662-54711-3},
    doi = {10.1007/978-3-662-54712-0_5},
    pdf = {https://www.sosy-lab.org/research/pub/2017-50JahreInfMUC.Software-Verifikation.pdf},
    keyword = {Software Model Checking},
    annote = {DOI: 10.1007/978-3-662-54712-0_5},
    
    }
    

Articles in conference or workshop proceedings

  1. Pavel Andrianov, Karlheinz Friedberger, Mikhail U. Mandrykin, Vadim S. Mutilin, and Anton Volkov.
    CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution).
    In Axel Legay and Tiziana Margaria, editors, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, Uppsala, Sweden, April 22-29), LNCS 10206, pages 355--359, 2017.
    Springer-Verlag, Heidelberg.
    [ Material ] Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking.
    Abstract

    Our submission to SV-COMP'17 is based on the software verification framework CPAchecker. Combined with value analysis and predicate analysis we use the concept of block-abstraction memoization with optimization and several fixes relative to the version of SV-COMP'16. A novelty of our approach is usage of BnB memory model for predicate analysis, which efficiently divides the accessed memory into memory regions and thus leads to smaller formulas.

    @inproceedings{CPABAM-COMP17,
    author = {Pavel Andrianov and Karlheinz Friedberger and Mikhail U. Mandrykin and Vadim S. Mutilin and Anton Volkov},
    title = {{CPA-BAM-BnB}: {Block}-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)},
    booktitle = {Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2017, Uppsala, Sweden, April 22-29)},
    editor = {Axel Legay and Tiziana Margaria},
    series = {LNCS~10206},
    pages = {355--359},
    year = {2017},
    publisher = {Springer-Verlag, Heidelberg},
    isbn = {978-3-662-54579-9},
    url = {http://dx.doi.org/10.1007/978-3-662-54580-5_22},
    doi = {10.1007/978-3-662-54580-5_22},
    keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking},
    abstract = { Our submission to SV-COMP'17 is based on the software verification framework CPAchecker. Combined with value analysis and predicate analysis we use the concept of block-abstraction memoization with optimization and several fixes relative to the version of SV-COMP'16. A novelty of our approach is usage of BnB memory model for predicate analysis, which efficiently divides the accessed memory into memory regions and thus leads to smaller formulas. },
    
    }
    

  2. Dirk Beyer.
    Software Verification with Validation of Results (Report on SV-COMP 2017).
    In A. Legay and T. Margaria, editors, Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017, Uppsala, Sweden, April 22-29), LNCS 10206, pages 331-349, 2017.
    Springer-Verlag, Heidelberg.
    [ Material ] [ Article ] Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking, Witness-Based Validation.

    @inproceedings{TACAS17,
    author = {Dirk Beyer},
    title = {Software Verification with Validation of Results ({R}eport on {SV-COMP} 2017)},
    booktitle = {Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2017, Uppsala, Sweden, April 22-29)},
    editor = {A.~Legay and T.~Margaria},
    series = {LNCS~10206},
    pages = {331-349},
    year = {2017},
    publisher = {Springer-Verlag, Heidelberg},
    isbn = {978-3-662-54579-9},
    doi = {10.1007/978-3-662-54580-5_20},
    pdf = {https://www.sosy-lab.org/research/pub/2017-TACAS.Software_Verification_with_Validation_of_Results.pdf},
    url = {http://sv-comp.sosy-lab.org/},
    keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking,Witness-Based Validation},
    
    }
    

  3. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann.
    Exchanging Verification Witnesses between Verifiers.
    In J. Jürjens and K. Schneider, editors, Tagungsband Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik (21.-24. Februar 2017, Hannover, Deutschland), LNI P-267, pages 93-94, 2017.
    Gesellschaft für Informatik (GI).
    Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation.

    @inproceedings{SE17-Witnesses,
    author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann},
    title = {Exchanging Verification Witnesses between Verifiers},
    booktitle = {Tagungsband Software Engineering 2017, Fachtagung des GI-Fachbereichs Softwaretechnik (21.-24. Februar 2017, Hannover, Deutschland)},
    publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})},
    editor = {J.~J{\"{u}}rjens and K.~Schneider},
    series = {{LNI}~P-267},
    pages = {93-94},
    year = {2017},
    url = {},
    keyword = {CPAchecker,Software Model Checking,Witness-Based Validation},
    
    }
    

  4. Dirk Beyer and Thomas Lemberger.
    Software Verification: Testing vs. Model Checking.
    In O. Strichman and R. Tzoref-Brill, editors, Proceedings of the 13th Haifa Verification Conference (HVC 2017, Haifa, Israel, November 13-25), LNCS 10629, pages 99-114, 2017.
    Springer.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): CPAchecker, Software Model Checking.
    Abstract

    In practice, software testing has been the established method for finding bugs in programs for a long time. But in the last 15 years, software model checking has received a lot of attention, and many successful tools for software model checking exist today. We believe it is time for a careful comparative evaluation of automatic software testing against automatic software model checking. We chose six existing tools for automatic test-case generation, namely AFL-fuzz, CPATiger, Crest-ppc, FShell, Klee, and PRtest, and four tools for software model checking, namely CBMC, CPA-Seq, ESBMC-incr, and ESBMC-kInd, for the task of finding specification violations in a large benchmark suite consisting of 5693 C programs. In order to perform such an evaluation, we have implemented a framework for test-based falsification (TBF) that executes and validates test cases produced by test-case generation tools in order to find errors in programs. The conclusion of our experiments is that software model checkers can (i) find a substantially larger number of bugs (ii) in less time, and (iii) require less adjustment to the input programs.
    Won the HVC 2017 Best Paper Award

    @inproceedings{HVC17,
    author = {Dirk Beyer and Thomas Lemberger},
    title = {Software Verification: Testing vs. Model Checking},
    booktitle = {Proceedings of the 13th Haifa Verification Conference (HVC~2017, Haifa, Israel, November 13-25)},
    editor = {O.~Strichman and R.~Tzoref-Brill},
    series = {LNCS~10629},
    pages = {99-114},
    year = {2017},
    publisher = {Springer},
    isbn = {978-3-319-70389-3},
    doi = {https://doi.org/10.1007/978-3-319-70389-3_7},
    pdf = {https://www.sosy-lab.org/research/pub/2017-HVC.Software_Verification_Testing_vs_Model_Checking.pdf},
    postscript = {https://www.sosy-lab.org/research/prs/2017-11-15_HVC17_TestStudy_Thomas.pdf},
    url = {https://www.sosy-lab.org/research/test-study/},
    annote = {Won the HVC 2017 Best Paper Award},
    abstract = { In practice, software testing has been the established method for finding bugs in programs for a long time. But in the last 15 years, software model checking has received a lot of attention, and many successful tools for software model checking exist today. We believe it is time for a careful comparative evaluation of automatic software testing against automatic software model checking. We chose six existing tools for automatic test-case generation, namely AFL-fuzz, CPATiger, Crest-ppc, FShell, Klee, and PRtest, and four tools for software model checking, namely CBMC, CPA-Seq, ESBMC-incr, and ESBMC-kInd, for the task of finding specification violations in a large benchmark suite consisting of 5693 C programs. In order to perform such an evaluation, we have implemented a framework for test-based falsification (TBF) that executes and validates test cases produced by test-case generation tools in order to find errors in programs. The conclusion of our experiments is that software model checkers can (i) find a substantially larger number of bugs (ii) in less time, and (iii) require less adjustment to the input programs. },
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  5. J. Pfähler, G. Ernst, S. Bodenmüller, G. Schellhorn, and W. Reif.
    Modular verification of order-preserving writeback caches.
    In Proc. of Integrated Formal Methods (iFM), volume 10510 of LNCS, pages 375--390, 2017.
    Springer.
    [ Article ]
    @inproceedings{ernst:ifm2017,
    author = {J. Pf{\"a}hler and G. Ernst and S. Bodenm{\"u}ller and G. Schellhorn and W. Reif},
    title = {Modular verification of order-preserving writeback caches},
    booktitle = {Proc. of Integrated Formal Methods (iFM)},
    pages = {375--390},
    publisher = {Springer},
    series = {LNCS},
    volume = {10510},
    year = {2017},
    pdf = {https://www.sosy-lab.org/research/pub/2017-iFM.Modular_Verification_of_Order-Preserving_Write-Back_Caches.pdf},
    
    }
    

Theses (PhD, MSc, BSc, Project)

  1. Evgeny Dunaev.
    Entwurf und Implementierung einer Abstraktionsschicht für Zuweisungs-basierte Analysen.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017.
    Keyword(s): CPAchecker, Software Model Checking, Refactoring.

    @misc{DunaevUnifyingAnalysis,
    author = {Evgeny Dunaev},
    title = {Entwurf und Implementierung einer Abstraktionsschicht f{\"u}r Zuweisungs-basierte Analysen},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2017},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking,Refactoring},
    
    }
    

  2. Deyan Ivanov.
    Interactive Visualization of Verification Results from CPAchecker with D3.
    Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017.
    [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{IvanovVisualization,
    author = {Deyan Ivanov},
    title = {Interactive Visualization of Verification Results from {{\sc CPAchecker}} with D3},
    howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab},
    year = {2017},
    pdf = {https://www.sosy-lab.org/research/bsc/2017.Ivanov.Interactive_Visualization_of_Verification_Results_from_CPAchecker_with_D3.pdf},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  3. Stefan Löwe.
    Effective Approaches to Abstraction Refinement for Automatic Software Verification.
    PhD Thesis, University of Passau, Software Systems Lab, 2017.
    [ Material ] [ Article ] Keyword(s): CPAchecker, Software Model Checking.

    @misc{StefanValueDomain,
    author = {Stefan L{\"{o}}we},
    title = {Effective Approaches to Abstraction Refinement for Automatic Software Verification},
    howpublished = {PhD Thesis, University of Passau, Software Systems Lab},
    year = {2017},
    pdf = {https://www.sosy-lab.org/research/phd/2017.Loewe.Effective_Approaches_to_Abstraction_Refinement_for_Automatic_Software_Verification.pdf},
    url = {https://www.sosy-lab.org/research/phd/loewe/},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

  4. Nils Steinger.
    Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters.
    Bachelor's Thesis, University of Passau, Software Systems Lab, 2017.
    [ Material ] [ Article ] Keyword(s): Benchmarking.

    @misc{SteingerMeasuring,
    author = {Nils Steinger},
    title = {Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2017},
    pdf = {https://www.sosy-lab.org/research/bsc/2017.Steinger.Measuring,_Visualizing,_and_Optimizing_the_Energy_Consumption_of_Computer_Clusters.pdf},
    url = {https://www.sosy-lab.org/research/bsc/steinger},
    field = {Computer Science},
    keyword = {Benchmarking},
    
    }
    

  5. Philipp Wendler.
    Towards Practical Predicate Analysis.
    PhD Thesis, University of Passau, Software Systems Lab, 2017.
    [ Material ] [ Article ] [ Presentation ] Keyword(s): Benchmarking, CPAchecker, Software Model Checking.

    @misc{PhilippPredicateAnalysis,
    author = {Philipp Wendler},
    title = {Towards Practical Predicate Analysis},
    howpublished = {PhD Thesis, University of Passau, Software Systems Lab},
    year = {2017},
    pdf = {https://www.sosy-lab.org/research/phd/2017.Wendler.Towards_Practical_Predicate_Analysis.pdf},
    url = {https://www.sosy-lab.org/research/phd/wendler/},
    keyword = {Benchmarking,CPAchecker,Software Model Checking},
    postscript= {https://www.sosy-lab.org/research/prs/2017-11-20_RigorosumWendler_TowardsPracticalPredicateAnalysis.pdf},
    annote = {Nominated for the Dissertation award 2017 of the German Gesellschaft für Informatik (GI)},
    
    }
    

  6. Gernot Zoerneck.
    Implementing PDR in CPAchecker.
    Bachelor's Thesis, University of Passau, Software Systems Lab, 2017.
    Keyword(s): CPAchecker, Software Model Checking.

    @misc{ZoerneckPDR,
    author = {Gernot Zoerneck},
    title = {Implementing PDR in {{\sc CPAchecker}}},
    howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab},
    year = {2017},
    field = {Computer Science},
    keyword = {CPAchecker,Software Model Checking},
    
    }
    

(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: Mon Dec 16 10:15:29 2019


This document was translated from BibTEX by bibtex2html