Falsification of Hybrid Systems Using Adaptive Probabilistic Search.

Publications of year 2017

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, 2017. Springer. doi:10.1007/978-3-662-54712-0_5 Link to this entry Keyword(s): Software Model Checking Publisher's Version PDF
    BibTeX Entry
    @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}, pages = {75-86}, year = {2017}, publisher = {Springer}, isbn = {978-3-662-54711-3}, doi = {10.1007/978-3-662-54712-0_5}, sha256 = {}, pdf = {https://www.sosy-lab.org/research/pub/2017-50JahreInfMUC.Software-Verifikation.pdf}, keyword = {Software Model Checking}, }

Articles in conference or workshop proceedings

  1. 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. doi:10.1007/978-3-319-70389-3_7 Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    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.
    BibTeX Entry
    @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}, pages = {99-114}, year = {2017}, series = {LNCS~10629}, publisher = {Springer}, isbn = {978-3-319-70389-3}, doi = {10.1007/978-3-319-70389-3_7}, sha256 = {}, url = {https://www.sosy-lab.org/research/test-study/}, pdf = {https://www.sosy-lab.org/research/pub/2017-HVC.Software_Verification_Testing_vs_Model_Checking.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2017-11-15_HVC17_TestStudy_Thomas.pdf}, 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}, annote = {Won the HVC 2017 Best Paper Award}, }
    Additional Infos
    Won the HVC 2017 Best Paper Award
  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. doi:10.1007/978-3-662-54580-5_20 Link to this entry Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking, Witness-Based Validation Publisher's Version PDF Supplement
    BibTeX Entry
    @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}, pages = {331-349}, year = {2017}, series = {LNCS~10206}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-54579-9}, doi = {10.1007/978-3-662-54580-5_20}, sha256 = {}, url = {https://sv-comp.sosy-lab.org/2017/}, pdf = {https://www.sosy-lab.org/research/pub/2017-TACAS.Software_Verification_with_Validation_of_Results.pdf}, 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). Link to this entry Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation
    BibTeX Entry
    @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)}, editor = {J.~J{\"{u}}rjens and K.~Schneider}, pages = {93-94}, year = {2017}, series = {{LNI}~P-267}, publisher = {Gesellschaft f{\"{u}}r Informatik ({GI})}, url = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation}, doinone = {DOI not available}, }
  4. 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), LNCS, pages 375-390, 2017. Springer. Link to this entry PDF
    BibTeX Entry
    @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)}, volume = {10510}, pages = {375--390}, year = {2017}, series = {LNCS}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2017-iFM.Modular_Verification_of_Order-Preserving_Write-Back_Caches.pdf}, }
  5. 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. doi:10.1007/978-3-662-54580-5_22 Link to this entry Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
    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.
    BibTeX Entry
    @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}, pages = {355--359}, year = {2017}, series = {LNCS~10206}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-662-54579-9}, doi = {10.1007/978-3-662-54580-5_22}, sha256 = {}, url = {https://doi.org/10.1007/978-3-662-54580-5_22}, 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.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, }

Theses and projects (PhD, MSc, BSc, Project)

  1. Philipp Wendler. Towards Practical Predicate Analysis. PhD Thesis, University of Passau, Software Systems Lab, 2017. Link to this entry Keyword(s): Benchmarking, CPAchecker, Software Model Checking Publisher's Version PDF Presentation Supplement
    BibTeX Entry
    @misc{PhilippPredicateAnalysis, author = {Philipp Wendler}, title = {Towards Practical Predicate Analysis}, year = {2017}, url = {https://www.sosy-lab.org/research/phd/wendler/}, pdf = {https://www.sosy-lab.org/research/phd/2017.Wendler.Towards_Practical_Predicate_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2017-11-20_RigorosumWendler_TowardsPracticalPredicateAnalysis.pdf}, keyword = {Benchmarking,CPAchecker,Software Model Checking}, annote = {Nominated for the Dissertation award 2017 of the German Gesellschaft für Informatik (GI)}, howpublished = {PhD Thesis, University of Passau, Software Systems Lab}, urn = {urn:nbn:de:bvb:739-opus4-5098}, }
    Additional Infos
  2. Stefan Löwe. Effective Approaches to Abstraction Refinement for Automatic Software Verification. PhD Thesis, University of Passau, Software Systems Lab, 2017. Link to this entry Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
    BibTeX Entry
    @misc{StefanValueDomain, author = {Stefan L{\"{o}}we}, title = {Effective Approaches to Abstraction Refinement for Automatic Software Verification}, year = {2017}, url = {https://www.sosy-lab.org/research/phd/loewe/}, pdf = {https://www.sosy-lab.org/research/phd/2017.Loewe.Effective_Approaches_to_Abstraction_Refinement_for_Automatic_Software_Verification.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {PhD Thesis, University of Passau, Software Systems Lab}, urn = {urn:nbn:de:bvb:739-opus4-4815}, }
  3. Evgeny Dunaev. Entwurf und Implementierung einer Abstraktionsschicht für Zuweisungs-basierte Analysen. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017. Link to this entry Keyword(s): CPAchecker, Software Model Checking, Refactoring
    BibTeX Entry
    @misc{DunaevUnifyingAnalysis, author = {Evgeny Dunaev}, title = {{Entwurf und Implementierung einer Abstraktionsschicht f{\"u}r Zuweisungs-basierte Analysen}}, year = {2017}, keyword = {CPAchecker,Software Model Checking,Refactoring}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  4. Deyan Ivanov. Interactive Visualization of Verification Results from CPAchecker with D3. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2017. Link to this entry Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry
    @misc{IvanovVisualization, author = {Deyan Ivanov}, title = {Interactive Visualization of Verification Results from {{\sc CPAchecker}} with {{\sc D3}}}, year = {2017}, pdf = {https://www.sosy-lab.org/research/bsc/2017.Ivanov.Interactive_Visualization_of_Verification_Results_from_CPAchecker_with_D3.pdf}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
  5. Nils Steinger. Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters. Bachelor's Thesis, University of Passau, Software Systems Lab, 2017. Link to this entry Keyword(s): Benchmarking PDF Supplement
    BibTeX Entry
    @misc{SteingerMeasuring, author = {Nils Steinger}, title = {Measuring, Visualizing, and Optimizing the Energy Consumption of Computer Clusters}, year = {2017}, url = {https://www.sosy-lab.org/research/bsc/steinger}, pdf = {https://www.sosy-lab.org/research/bsc/2017.Steinger.Measuring,_Visualizing,_and_Optimizing_the_Energy_Consumption_of_Computer_Clusters.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
  6. Gernot Zoerneck. Implementing PDR in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2017. Link to this entry Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry
    @misc{ZoerneckPDR, author = {Gernot Zoerneck}, title = {Implementing {PDR} in {{\sc CPAchecker}}}, year = {2017}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }

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: Sat Oct 23 23:51:13 2021