Software and Computational Systems Lab

Publications of year 2012

1. Dirk Beyer, Arie van Deursen, and Michael W. Godfrey, editors. Proceedings of the 20th IEEE International Conference on Program Comprehension. 2012. IEEE. doi:10.1109/ICPC19659.2012 Publisher's Version PDF Supplement
   BibTeX Entry

   @proceedings{ICPC12, title = {Proceedings of the 20th IEEE International Conference on Program Comprehension}, editor = {Dirk Beyer and Arie van Deursen and Michael W. Godfrey}, year = {2012}, publisher = {IEEE}, isbn = {978-1-4673-1216-5}, doi = {10.1109/ICPC19659.2012}, url = {https://icpc12.sosy-lab.org/}, pdf = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6230782}, }

2. Dirk Beyer, Thomas A. Henzinger, M. Erkan Keremoglu, and Philipp Wendler. Conditional Model Checking: A Technique to Pass Information between Verifiers. In Tevfik Bultan and Martin Robillard, editors, Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2012, Cary, NC, November 10-17), 2012. ACM. doi:10.1145/2393596.2393664 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   Abstract

   Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P -usually a state predicate- such that the program satisfies the specification under the condition P -that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.
   BibTeX Entry

   @inproceedings{FSE12, author = {Dirk Beyer and Thomas A. Henzinger and M. Erkan Keremoglu and Philipp Wendler}, title = {Conditional Model Checking: {A} Technique to Pass Information between Verifiers}, booktitle = {Proceedings of the 20th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE~2012, Cary, NC, November 10-17)}, editor = {Tevfik Bultan and Martin Robillard}, pages = {}, year = {2012}, publisher = {ACM}, isbn = {978-1-4503-1614-9}, doi = {10.1145/2393596.2393664}, url = {https://www.sosy-lab.org/research/cpa-cmc/}, pdf = {https://www.sosy-lab.org/research/pub/2012-FSE.Conditional_Model_Checking.pdf}, abstract = {Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave the states in which P is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.}, keyword = {CPAchecker,Software Model Checking}, }
3. Dirk Beyer and Philipp Wendler. Algorithms for Software Model Checking: Predicate Abstraction vs. IMPACT. In Gianpiero Cabodi and Satnam Singh, editors, Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2012, Cambrige, UK, October 22-25), pages 106-113, 2012. FMCAD. Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF Supplement
   Abstract

   CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in BLAST) and lazy abstraction with interpolants (as in IMPACT). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the IMPACT algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).
   BibTeX Entry

   @inproceedings{FMCAD12, author = {Dirk Beyer and Philipp Wendler}, title = {Algorithms for Software Model Checking: Predicate Abstraction vs. {IMPACT}}, booktitle = {Proceedings of the 12th International Conference on Formal Methods in Computer-Aided Design (FMCAD~2012, Cambrige, UK, October 22-25)}, editor = {Gianpiero Cabodi and Satnam Singh}, pages = {106-113}, year = {2012}, publisher = {FMCAD}, isbn = {978-1-4673-4831-7}, url = {https://www.sosy-lab.org/research/cpa-uni/}, pdf = {https://www.sosy-lab.org/research/pub/2012-FMCAD.Algorithms_for_Software_Model_Checking.pdf}, abstract = {CEGAR, SMT solving, and Craig interpolation are successful approaches for software model checking. We compare two of the most important algorithms that are based on these techniques: lazy predicate abstraction (as in BLAST) and lazy abstraction with interpolants (as in IMPACT). We unify the algorithms formally (by expressing both in the CPA framework) as well as in practice (by implementing them in the same tool). This allows us to flexibly experiment with new configurations and gain new insights, both about their most important differences and commonalities, as well as about their performance characteristics. We show that the essential contribution of the IMPACT algorithm is the reduction of the number of refinements, and compare this to another approach for reducing refinement effort: adjustable-block encoding (ABE).}, keyword = {CPAchecker,Software Model Checking}, doinone = {DOI not available}, urlpub = {https://ieeexplore.ieee.org/document/6462562/}, }
4. Dirk Beyer. Competition on Software Verification (SV-COMP). In C. Flanagan and B. König, editors, Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012, Tallinn, Estonia, March 27-30), LNCS 7214, pages 504-524, 2012. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-28756-5_38 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Publisher's Version PDF Supplement
   Abstract

   This report describes the definitions, rules, setup, procedure, and results of the 1st International Competition on Software Verification. The verification community has performed competitions in various areas in the past, and SV-COMP'12 is the first competition of verification tools that take software programs as input and run a fully automatic verification of a given safety property. This year's competition is organized as a satellite event of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
   BibTeX Entry

   @inproceedings{TACAS12, author = {Dirk Beyer}, title = {Competition on Software Verification ({SV-COMP})}, booktitle = {Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2012, Tallinn, Estonia, March 27-30)}, editor = {C.~Flanagan and B.~K{\"o}nig}, pages = {504--524}, year = {2012}, series = {LNCS~7214}, publisher = {Springer-Verlag, Heidelberg}, isbn = {}, doi = {10.1007/978-3-642-28756-5_38}, sha256 = {77183c925bfa38fdd3cae2f65ed8d94aceb39a0805bad96adec5e4e70048e49b}, url = {https://sv-comp.sosy-lab.org/2012/}, abstract = {This report describes the definitions, rules, setup, procedure, and results of the 1st International Competition on Software Verification. The verification community has performed competitions in various areas in the past, and SV-COMP'12 is the first competition of verification tools that take software programs as input and run a fully automatic verification of a given safety property. This year's competition is organized as a satellite event of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, }
5. Dirk Beyer and Alexander K. Petrenko. Linux Driver Verification. In T. Margaria and B. Steffen, editors, Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part II, Heraklion, Crete, October 15-18), LNCS 7610, pages 1-6, 2012. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-34032-1_1 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{LDV12, author = {Dirk Beyer and Alexander K. Petrenko}, title = {{Linux} Driver Verification}, booktitle = {Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2012, Part II, Heraklion, Crete, October 15-18)}, editor = {T.~Margaria and B.~Steffen}, pages = {1-6}, year = {2012}, series = {LNCS~7610}, publisher = {Springer-Verlag, Heidelberg}, isbn = {}, doi = {10.1007/978-3-642-34032-1_1}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2012-ISOLA.Linux_Driver_Verification.pdf}, keyword = {Software Model Checking}, }
6. Falk Howar, Malte Isberner, Maik Merten, Bernhard Steffen, and Dirk Beyer. The RERS Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems. In T. Margaria and B. Steffen, editors, Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2012, Part I, Heraklion, Crete, October 15-18), LNCS 7609, pages 608-614, 2012. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-34026-0_45 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{RERS12, author = {Falk Howar and Malte Isberner and Maik Merten and Bernhard Steffen and Dirk Beyer}, title = {The {RERS} Grey-Box Challenge 2012: Analysis of Event-Condition-Action Systems}, booktitle = {Proceedings of the 5th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2012, Part I, Heraklion, Crete, October 15-18)}, editor = {T.~Margaria and B.~Steffen}, pages = {608-614}, year = {2012}, series = {LNCS~7609}, publisher = {Springer-Verlag, Heidelberg}, isbn = {}, doi = {10.1007/978-3-642-34026-0_45}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2012-ISOLA.The_RERS_Grey-Box_Challenge_2012_Analysis_of_Event-Condition-Action_Systems.pdf}, keyword = {Software Model Checking}, }
7. Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, and Wolfgang Reif. A formal model of a Virtual Filesystem Switch. In Proc. of Software and Systems Modeling (SSV), EPTCS, pages 33-45, 2012. PDF
   BibTeX Entry

   @inproceedings{ernst:ssv2012, author = {Gidon Ernst and Gerhard Schellhorn and Dominik Haneberg and Jörg Pfähler and Wolfgang Reif}, title = {{A formal model of a Virtual Filesystem Switch}}, booktitle = {Proc. of Software and Systems Modeling (SSV)}, volume = {102}, pages = {33--45}, year = {2012}, series = {EPTCS}, pdf = {https://www.sosy-lab.org/research/pub/2012-SSV.A_Formal_Model_of_a_Virtual_Filesysem_Switch.pdf}, }
8. Stefan Löwe and Philipp Wendler. CPAchecker with Adjustable Predicate Analysis (Competition Contribution). In C. Flanagan and B. König, editors, Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012, Tallinn, Estonia, March 27-30), LNCS 7214, pages 528-530, 2012. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-28756-5_40 Keyword(s): CPAchecker, Competition on Software Verification (SV-COMP), Software Model Checking Publisher's Version PDF Supplement
   Abstract

   CPAchecker is a freely available software-verification framework, built on the concepts of configurable program analysis (CPA). CPAchecker integrates most of the state-of-the-art technologies for software model checking, such as counterexample-guided abstraction refinement (CEGAR), lazy predicate abstraction, interpolation-based refinement, and large-block encoding. The CPA for predicate analysis with adjustable-block encoding (ABE) is very promising in many categories, and thus, we submit a CPAchecker configuration that uses this analysis approach to the competition.
   BibTeX Entry

   @inproceedings{CPACHECKERABE-COMP12, author = {Stefan L{\"{o}}we and Philipp Wendler}, title = {{{\sc CPAchecker}} with Adjustable Predicate Analysis (Competition Contribution)}, booktitle = {Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2012, Tallinn, Estonia, March 27-30)}, editor = {C.~Flanagan and B.~K{\"o}nig}, pages = {528--530}, year = {2012}, series = {LNCS~7214}, publisher = {Springer-Verlag, Heidelberg}, doi = {10.1007/978-3-642-28756-5_40}, sha256 = {}, url = {https://doi.org/10.1007/978-3-642-28756-5_40}, pdf = {https://www.sosy-lab.org/research/pub/2012-TACAS.CPAchecker_with_Adjustable_Predicate_Analysis.pdf}, abstract = {CPAchecker is a freely available software-verification framework, built on the concepts of configurable program analysis (CPA). CPAchecker integrates most of the state-of-the-art technologies for software model checking, such as counterexample-guided abstraction refinement (CEGAR), lazy predicate abstraction, interpolation-based refinement, and large-block encoding. The CPA for predicate analysis with adjustable-block encoding (ABE) is very promising in many categories, and thus, we submit a CPAchecker configuration that uses this analysis approach to the competition.}, keyword = {CPAchecker,Competition on Software Verification (SV-COMP),Software Model Checking}, annote = {Won category ControlFlowInteger and received one silver and two bronze medals in <span style="white-space: nowrap"><a href="https://sv-comp.sosy-lab.org/2012/">SV-COMP'12</a></span>}, }
   Additional Infos

   Won category ControlFlowInteger and received one silver and two bronze medals in SV-COMP'12

9. Dirk Beyer and Stefan Löwe. Explicit-Value Analysis Based on CEGAR and Interpolation. Technical report MIP-1205, Department of Computer Science and Mathematics (FIM), University of Passau (PA), December 2012. doi:10.48550/arXiv.1212.6542 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @techreport{TR1205-PA12, author = {Dirk Beyer and Stefan L{\"o}we}, title = {Explicit-Value Analysis Based on {CEGAR} and Interpolation}, number = {MIP-1205}, year = {2012}, doi = {10.48550/arXiv.1212.6542}, url = {}, abstract = {}, keyword = {CPAchecker,Software Model Checking}, annote = {}, institution = {Department of Computer Science and Mathematics (FIM), University of Passau (PA)}, month = {December}, }

10. Christopher Jahn. Implementation of a CFA and ARG Visualization and Navigation Tool in Java. Master's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{JahnVisualization, author = {Christopher Jahn}, title = {Implementation of a {CFA} and {ARG} Visualization and Navigation Tool in {Java}}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, }
11. Andreas Stahlbauer. Block-Encoding Strategies for Predicate Analysis: An Experimental Study. Master's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{StahlbauerStrategies, author = {Andreas Stahlbauer}, title = {Block-Encoding Strategies for Predicate Analysis: An Experimental Study}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, permit = {Permission for making available online not granted (Dirk asked on 2020-07-17 and received denial on 2020-07-18)}, }
12. Peter Häring. A Comparative Study of Software Measures as Problem-Predictors. Master's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{HaeringMeasures, author = {Peter H{\"a}ring}, title = {A Comparative Study of Software Measures as Problem-Predictors}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, University of Passau, Software Systems Lab}, permit = {}, }
13. Alexander Driemeyer. Software-Verifikation von Java-Programmen in CPAchecker. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{DriemeyerJava, author = {Alexander Driemeyer}, title = {Software-Verifikation von Java-Programmen in CPAchecker}, year = {2012}, keyword = {CPAchecker,Software Model Checking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
14. Karlheinz Friedberger. Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken. Bachelor's Thesis, University of Passau, Software Systems Lab, 2012. Keyword(s): CPAchecker, Software Model Checking PDF
    BibTeX Entry

    @misc{KarlheinzDomainTypes, author = {Karlheinz Friedberger}, title = {{Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken}}, year = {2012}, pdf = {https://www.sosy-lab.org/research/bsc/2012.Friedberger.Ein_typbasierter_Ansatz_zur_Kombination_verschiedener_Verifikationstechniken.pdf}, keyword = {CPAchecker,Software Model Checking}, annote = {Won the yearly award of the chamber of industry and commerce of Lower Bavaria (IHK Niederbayern) for an excellent Bachelor's thesis}, field = {Computer Science}, howpublished = {Bachelor's Thesis, University of Passau, Software Systems Lab}, }
    Additional Infos

    Won the yearly award of the chamber of industry and commerce of Lower Bavaria (IHK Niederbayern) for an excellent Bachelor's thesis