Software and Computational Systems Lab

Publications of year 2022

1. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, Thomas Lemberger, and Michael Tautschnig. Verification Witnesses. ACM Trans. Softw. Eng. Methodol., 31(4):57:1-57:69, 2022. doi:10.1145/3477579 Keyword(s): CPAchecker, Ultimate, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Publisher's Version PDF Supplement
   BibTeX Entry

   @article{Witnesses-TOSEM, author = {Dirk Beyer and Matthias Dangl and Daniel Dietsch and Matthias Heizmann and Thomas Lemberger and Michael Tautschnig}, title = {Verification Witnesses}, journal = {ACM Trans. Softw. Eng. Methodol.}, volume = {31}, number = {4}, pages = {57:1-57:69}, year = {2022}, doi = {10.1145/3477579}, url = {https://www.sosy-lab.org/research/verification-witnesses-tosem/}, keyword = {CPAchecker,Ultimate,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TOSEM.Verification_Witnesses.pdf}, _sha256 = {48acf3f35251df635e829b29fe8f16fd50498f8f99a082b8b9e0aa094a97a432}, }
2. Martin Wirsing and and Alexander Knapp. A Reduction-based Cut-free Gentzen Calculus for Dynamic Epistemic Logic. Logic Journal of the IGPL, 12 2022. doi:10.1093/jigpal/jzac078 Publisher's Version PDF
   Abstract

   Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We present a novel cut-free ordinary sequent calculus, called G4_P,A[], for propositional DEL. In contrast to the known sequent calculi, our calculus does not internalize the accessibility relations, but—similar to Hilbert style proof calculi—action formulas are reduced to epistemic formulas. Since no ordinary sequent calculus for full S5 modal logic is known, the proof rules for the knowledge operator and the Boolean operators are those of an underlying S4 modal calculus. We show the soundness and completeness of G4_P,A[] and prove also the admissibility of the cut-rule and of several other rules for introducing the action modality.
   BibTeX Entry

   @article{WirsingJ22, author = {Martin Wirsing and and Alexander Knapp}, title = {A Reduction-based Cut-free Gentzen Calculus for Dynamic Epistemic Logic}, journal = {Logic Journal of the IGPL}, year = {2022}, doi = {10.1093/jigpal/jzac078}, pdf = {https://sosy-lab.org/research/pub/2022-LogJIGPL.A_Reduction-based_Cut-free_Gentzen_Calculus_for_Dynamic_Epistemic_Logic.pdf}, abstract = {Dynamic epistemic logic (DEL) is a multi-modal logic for reasoning about the change of knowledge in multi-agent systems. It extends epistemic logic by a modal operator for actions which announce logical formulas to other agents. In Hilbert-style proof calculi for DEL, modal action formulas are reduced to epistemic logic, whereas current sequent calculi for DEL are labelled systems which internalize the semantic accessibility relation of the modal operators, as well as the accessibility relation underlying the semantics of the actions. We present a novel cut-free ordinary sequent calculus, called G4_P,A[], for propositional DEL. In contrast to the known sequent calculi, our calculus does not internalize the accessibility relations, but—similar to Hilbert style proof calculi—action formulas are reduced to epistemic formulas. Since no ordinary sequent calculus for full S5 modal logic is known, the proof rules for the knowledge operator and the Boolean operators are those of an underlying S4 modal calculus. We show the soundness and completeness of G4_P,A[] and prove also the admissibility of the cut-rule and of several other rules for introducing the action modality.}, issn = {1367-0751}, month = {12}, }

3. Dirk Beyer and Andreas Podelski. Software Model Checking: 20 Years and Beyond. In Principles of Systems Design, LNCS 13660, pages 554-582, 2022. Springer. doi:10.1007/978-3-031-22337-2_27 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{Henzinger22, author = {Dirk Beyer and Andreas Podelski}, title = {Software Model Checking: 20 Years and Beyond}, booktitle = {Principles of Systems Design}, pages = {554-582}, year = {2022}, series = {LNCS~13660}, publisher = {Springer}, doi = {10.1007/978-3-031-22337-2_27}, sha256 = {87a441617d1194266dff5fd5bd143370e9b318e72848b2d6e3c49f152a136799}, url = {}, abstract = {}, keyword = {Software Model Checking}, _pdf = {}, editors = {J-F.~Raskin and K.~Chatterjee and L.~Doyen and R.~Majumdar}, funding = {}, }
4. Dirk Beyer and Jan Strejček. Case Study on Verification-Witness Validators: Where We Are and Where We Go. In Proceedings of the 29th International Symposium on Static Analysis, (SAS 2022, Auckland, New Zealand, December 5-7, 2022), LNCS 13790, pages 160-174, 2022. Springer. doi:10.1007/978-3-031-22308-2_8 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SAS22, author = {Dirk Beyer and Jan Strejček}, title = {Case Study on Verification-Witness Validators: Where We Are and Where We Go}, booktitle = {Proceedings of the 29th International Symposium on Static Analysis, (SAS~2022, Auckland, New Zealand, December 5-7, 2022)}, pages = {160-174}, year = {2022}, series = {LNCS~13790}, publisher = {Springer}, doi = {10.1007/978-3-031-22308-2_8}, sha256 = {8003de86c73be27da528c44f440a49cd03a877649c9cb61a328a37507bc963da}, url = {}, abstract = {}, keyword = {Software Model Checking}, _pdf = {}, editors = {Gagandeep Singh and Caterina Urban}, funding = {}, }
5. Stefan Winter, Christopher Steven Timperley, Ben Hermann, Jürgen Cito, Jonathan Bell, Michael Hilton, and Dirk Beyer. A Retrospective Study of One Decade of Artifact Evaluations. In Abhik Roychoudhury, Cristian Cadar, and Miryung Kim, editors, Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, pages 145-156, 2022. ACM. doi:10.1145/3540250.3549172 Keyword(s): Software Model Checking Publisher's Version PDF
   BibTeX Entry

   @inproceedings{FSE22, author = {Stefan Winter and Christopher Steven Timperley and Ben Hermann and Jürgen Cito and Jonathan Bell and Michael Hilton and Dirk Beyer}, title = {A Retrospective Study of One Decade of Artifact Evaluations}, booktitle = {Proceedings of the 30th {ACM} Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18}, editor = {Abhik Roychoudhury and Cristian Cadar and Miryung Kim}, pages = {145-156}, year = {2022}, publisher = {ACM}, doi = {10.1145/3540250.3549172}, keyword = {Software Model Checking}, _sha256 = {5ad5c04b173c8c68f651b955545d44a7d74c0cf497b2c7ec988768d7459e26b4}, funding = {}, }
6. Dirk Beyer, Martin Spiessl, and Sven Umbricht. Cooperation between Automatic and Interactive Software Verifiers. In Bernd-Holger Schlingloff and Ming Chai, editors, Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM 2022, Berlin, Germany, September 26-30, LNCS 13550, pages 111–128, 2022. Springer. doi:10.1007/978-3-031-17108-6_7 Keyword(s): Software Model Checking, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SEFM22b, author = {Dirk Beyer and Martin Spiessl and Sven Umbricht}, title = {Cooperation between Automatic and Interactive Software Verifiers}, booktitle = {Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM~2022, Berlin, Germany, September 26-30}, editor = {Bernd-Holger Schlingloff and Ming Chai}, pages = {111–128}, year = {2022}, series = {LNCS~13550}, publisher = {Springer}, doi = {10.1007/978-3-031-17108-6_7}, sha256 = {a310ff0ac97f37ee817c6f05a4cc9a635cbacd09ad301b483095f133040e8e48}, url = {}, abstract = {}, keyword = {Software Model Checking, CPAchecker}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.Cooperation_between_Automatic_and_Interactive_Software_Verifiers.pdf}, funding = {DFG-CONVEY}, }
7. Dirk Beyer, Marian Lingsch Rosenfeld, and Martin Spiessl. A Unifying Approach for Control-Flow-Based Loop Abstraction. In Bernd-Holger Schlingloff and Ming Chai, editors, Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM 2022, Berlin, Germany, September 26-30, LNCS 13550, pages 3-19, 2022. Springer. doi:10.1007/978-3-031-17108-6_1 Keyword(s): Software Model Checking, CPAchecker Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @inproceedings{SEFM22a, author = {Dirk Beyer and Marian Lingsch Rosenfeld and Martin Spiessl}, title = {A Unifying Approach for Control-Flow-Based Loop Abstraction}, booktitle = {Proceedings of the 20th International Conference on Software Engineering and Formal Methods, (SEFM~2022, Berlin, Germany, September 26-30}, editor = {Bernd-Holger Schlingloff and Ming Chai}, pages = {3-19}, year = {2022}, series = {LNCS~13550}, publisher = {Springer}, doi = {10.1007/978-3-031-17108-6_1}, sha256 = {047a8a9062e143741623320cf80ec963ce5f7200a5a75d263fa6615c12f2199e}, url = {}, abstract = {}, keyword = {Software Model Checking, CPAchecker}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.A_Unifying_Approach_for_Control-Flow-Based_Loop_Abstraction.pdf}, funding = {DFG-CONVEY}, }
8. Dirk Beyer, Jan Haltermann, Thomas Lemberger, and Heike Wehrheim. Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR. In Proceedings of the 44th International Conference on Software Engineering (ICSE 2022, Pittsburgh, PA, USA, May 8-20 (Virtual), May 22-27 (In-Person)), pages 536-548, 2022. ACM. doi:10.1145/3510003.3510064 Keyword(s): CPAchecker, Software Model Checking, Interfaces for Component-Based Design Funding: DFG-COOP Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.5301636
   Abstract

   Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that - despite the necessity of exchanging complex data via interfaces - the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.
   BibTeX Entry

   @inproceedings{ICSE22, author = {Dirk Beyer and Jan Haltermann and Thomas Lemberger and Heike Wehrheim}, title = {Decomposing Software Verification into Off-the-Shelf Components: An Application to {CEGAR}}, booktitle = {Proceedings of the 44th International Conference on Software Engineering (ICSE~2022, Pittsburgh, PA, USA, May 8-20 (Virtual), May 22-27 (In-Person))}, pages = {536-548}, year = {2022}, publisher = {ACM}, doi = {10.1145/3510003.3510064}, url = {https://www.sosy-lab.org/research/component-based-cegar/}, abstract = {Techniques for software verification are typically realized as cohesive units of software with tightly coupled components. This makes it difficult to re-use components, and the potential for workload distribution is limited. Innovations in software verification might find their way into practice faster if provided in smaller, more specialized components. In this paper, we propose to strictly decompose software verification: the verification task is split into independent subtasks, implemented by only loosely coupled components communicating via clearly defined interfaces. We apply this decomposition concept to one of the most frequently employed techniques in software verification: counterexample-guided abstraction refinement (CEGAR). CEGAR is a technique to iteratively compute an abstract model of the system. We develop a decomposition of CEGAR into independent components with clearly defined interfaces that are based on existing, standardized exchange formats. Its realization component-based CEGAR (C-CEGAR) concerns the three core tasks of CEGAR: abstract-model exploration, feasibility check, and precision refinement. We experimentally show that --- despite the necessity of exchanging complex data via interfaces --- the efficiency thereby only reduces by a small constant factor while the precision in solving verification tasks even increases. We furthermore illustrate the advantages of C-CEGAR by experimenting with different implementations of components, thereby further increasing the overall effectiveness and testing that substitution of components works well.}, keyword = {CPAchecker,Software Model Checking,Interfaces for Component-Based Design}, _pdf = {https://www.sosy-lab.org/research/pub/2022-ICSE.Decomposing_Software_Verification_into_Off-the-Shelf-Components.pdf}, _sha256 = {be1c5d744475af00f5a0cddd51d92353296d1d8e5ba60f5439ba5b98217e0e03}, artifact = {10.5281/zenodo.5301636}, funding = {DFG-COOP}, }
9. Dirk Beyer and Martin Spiessl. The Static Analyzer Frama-C in SV-COMP (Competition Contribution). In Dana Fisman and Grigore Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13244, pages 429-434, 2022. Springer. doi:10.1007/978-3-030-99527-0_26 Keyword(s): Competition on Software Verification (SV-COMP), Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @inproceedings{TACAS22c, author = {Dirk Beyer and Martin Spiessl}, title = {The Static Analyzer {Frama-C} in {SV-COMP} (Competition Contribution)}, booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7}, editor = {Dana Fisman and Grigore Rosu}, pages = {429--434}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_26}, sha256 = {77ed425c2b30a4f9424ed46c9cb5a846f5c21677ececdbf098e30f37aca67a3d}, url = {}, abstract = {}, keyword = {Competition on Software Verification (SV-COMP),Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TACAS.The_Static_Analyzer_Frama-C_in_SV-COMP_Competition_Contribution.pdf}, funding = {DFG-CONVEY}, }
10. Dirk Beyer. Progress on Software Verification: SV-COMP 2022. In D. Fisman and G. Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13244, pages 375-402, 2022. Springer. doi:10.1007/978-3-030-99527-0_20 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Funding: DFG-COOP Publisher's Version PDF
    BibTeX Entry

    @inproceedings{TACAS22b, author = {Dirk Beyer}, title = {Progress on Software Verification: {SV-COMP 2022}}, booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7}, editor = {D.~Fisman and G.~Rosu}, pages = {375-402}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_20}, sha256 = {88d2b7552d79ad77c4e000f83a18f9d71038f7ddfca6c0f0700644405a115943}, url = {}, abstract = {}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TACAS.Progress_on_Software_Verification_SV-COMP_2022.pdf}, funding = {DFG-COOP}, }
11. Dirk Beyer and Sudeep Kanav. CoVeriTeam: On-Demand Composition of Cooperative Verification Systems. In D. Fisman and G. Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7, LNCS 13243, pages 561-579, 2022. Springer. doi:10.1007/978-3-030-99524-9_31 Keyword(s): Software Model Checking, Cooperative Verification Funding: DFG-COOP Publisher's Version PDF Presentation Supplement
    BibTeX Entry

    @inproceedings{TACAS22a, author = {Dirk Beyer and Sudeep Kanav}, title = {{CoVeriTeam}: {O}n-Demand Composition of Cooperative Verification Systems}, booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7}, editor = {D.~Fisman and G.~Rosu}, pages = {561-579}, year = {2022}, series = {LNCS~13243}, publisher = {Springer}, doi = {10.1007/978-3-030-99524-9_31}, sha256 = {e38311ae071351301b08d16849ee309a86efdc07fc45e18e466b4735ef21f241}, url = {https://www.sosy-lab.org/research/coveriteam/}, presentation = {https://www.sosy-lab.org/research/prs/2022-04-06_TACAS22_CoVeriTeam_Sudeep.pdf}, abstract = {}, keyword = {Software Model Checking,Cooperative Verification}, funding = {DFG-COOP}, }
12. Dirk Beyer. Advances in Automatic Software Testing: Test-Comp 2022. In E. B. Johnsen and M. Wimmer, editors, Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE 2022, Munich, Germany, April 2-7), LNCS 13241, pages 321-335, 2022. Springer. doi:10.1007/978-3-030-99429-7_18 Keyword(s): Competition on Software Testing (Test-Comp), Competition on Software Testing (Test-Comp Report), Software Testing Funding: DFG-COOP Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{FASE22b, author = {Dirk Beyer}, title = {Advances in Automatic Software Testing: {Test-Comp 2022}}, booktitle = {Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7)}, editor = {E.~B.~Johnsen and M.~Wimmer}, pages = {321-335}, year = {2022}, series = {LNCS~13241}, publisher = {Springer}, isbn = {}, doi = {10.1007/978-3-030-99429-7_18}, sha256 = {3f921c8f232a5c970f678889de8c402313049522a5dfa69ca68cd01d9dd9fce3}, url = {https://test-comp.sosy-lab.org/2022/}, abstract = {}, keyword = {Competition on Software Testing (Test-Comp),Competition on Software Testing (Test-Comp Report),Software Testing}, _pdf = {https://www.sosy-lab.org/research/pub/2022-FASE.Advances_in_Automatic_Software_Testing_Test-Comp_2022.pdf}, funding = {DFG-COOP}, }
13. Dirk Beyer, Sudeep Kanav, and Cedric Richter. Construction of Verifier Combinations Based on Off-the-Shelf Verifiers. In E. B. Johnsen and M. Wimmer, editors, Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE 2022, Munich, Germany, April 2-7), LNCS 13241, pages 49-70, 2022. Springer. doi:10.1007/978-3-030-99429-7_3 Keyword(s): Software Model Checking Funding: DFG-COOP Publisher's Version PDF Presentation Supplement
    BibTeX Entry

    @inproceedings{FASE22a, author = {Dirk Beyer and Sudeep Kanav and Cedric Richter}, title = {Construction of Verifier Combinations Based on Off-the-Shelf Verifiers}, booktitle = {Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7)}, editor = {E.~B.~Johnsen and M.~Wimmer}, pages = {49-70}, year = {2022}, series = {LNCS~13241}, publisher = {Springer}, isbn = {}, doi = {10.1007/978-3-030-99429-7_3}, sha256 = {fa50620b5b60e7c8761ea251b3ab30ef1e18320d49d76f417eac6dcd5b4a0bbc}, url = {https://www.sosy-lab.org/research/coveriteam-combinations/}, presentation = {https://www.sosy-lab.org/research/prs/2022-04-04_FASE22-CoVeriTeam-Combinations_Cedric.pdf}, abstract = {}, keyword = {Software Model Checking}, funding = {DFG-COOP}, }
14. Ernst, G., Knapp, A., and Murray, T.. A Hoare Logic with Regular Behavioral Specifications. In Proc. of International Symposium on Leveraging Applications of Formal Methods (ISoLA), LNCS, 2022. Springer.
    BibTeX Entry

    @inproceedings{ernst:isola2022, author = {Ernst, G. and Knapp, A. and Murray, T.}, title = {A {Hoare} Logic with Regular Behavioral Specifications}, booktitle = {Proc. of International Symposium on Leveraging Applications of Formal Methods (ISoLA)}, volume = {13701}, year = {2022}, series = {LNCS}, publisher = {Springer}, }
15. D. Liu, V.-T. Pham, G. Ernst, T. Murray, and B.I.P. Rubinstein. State selection algorithms and their impact on the performance of stateful network protocol fuzzing. In Proc. of Software Analysis, Evolution and Reengineering (SANER), 2022. IEEE.
    BibTeX Entry

    @inproceedings{ernst:saner2022, author = {D. Liu and V.-T. Pham and G. Ernst and T. Murray and B.I.P. Rubinstein}, title = {State selection algorithms and their impact on the performance of stateful network protocol fuzzing}, booktitle = {Proc. of Software Analysis, Evolution and Reengineering (SANER)}, year = {2022}, publisher = {IEEE}, }
16. Ernst, G.. Loop Verification with Invariants and Summaries. In Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI), LNCS, 2022. Springer.
    BibTeX Entry

    @inproceedings{ernst:vmcai2022, author = {Ernst, G.}, title = {Loop Verification with Invariants and Summaries}, booktitle = {Proc. of Verification, Model-Checking, and Abstract Interpretation (VMCAI)}, volume = {13182}, year = {2022}, series = {LNCS}, publisher = {Springer}, }
17. Ernst, G. and others. ARCH-COMP 2022 category report: Falsification with Unbounded Resources. In Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH), EPiC, pages 204-221, 2022. EasyChair.
    BibTeX Entry

    @inproceedings{ernst:arch2022, author = {Ernst, G. and others}, title = {{ARCH-COMP} 2022 category report: Falsification with Unbounded Resources}, booktitle = {Proc. of Applied Verification of Continuous and Hybrid Systems (ARCH)}, volume = {90}, pages = {204--221}, year = {2022}, series = {EPiC}, publisher = {EasyChair}, }
18. Matthias Kettl and Thomas Lemberger. The Static Analyzer Infer in SV-COMP (Competition Contribution). In Dana Fisman and Grigore Rosu, editors, Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022, Munich, Germany, April 2-7), Part 2, LNCS 13244, pages 451-456, 2022. Springer. doi:10.1007/978-3-030-99527-0_30 Keyword(s): Competition on Software Verification (SV-COMP) Publisher's Version PDF Presentation
    Abstract

    We present Infer-SV, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-SV, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.
    BibTeX Entry

    @inproceedings{INFER-SVCOMP22, author = {Matthias Kettl and Thomas Lemberger}, title = {The Static Analyzer Infer in {SV-COMP} (Competition Contribution)}, booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7), Part 2}, editor = {Dana Fisman and Grigore Rosu}, pages = {451--456}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_30}, pdf = {https://www.sosy-lab.org/research/pub/2022-SVCOMP.The_Static_Analyzer_Infer_in_SV-COMP.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-04-07_TACAS_Infer.pdf}, abstract = {We present Infer-SV, a wrapper that adapts Infer for SV-COMP. Infer is a static-analysis tool for C and other languages, developed by Facebook and used by multiple large companies. It is strongly aimed at industry and the internal use at Facebook. Despite its popularity, there are no reported numbers on its precision and efficiency. With Infer-SV, we take a first step towards an objective comparison of Infer with other SV-COMP participants from academia and industry.}, keyword = {Competition on Software Verification (SV-COMP)}, }
19. Martin Wirsing, Rocco De Nicola, and Stefan Jähnichen. Rigorous Engineering of Collective Adaptive Systems Introduction to the 4th Track Edition. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part III, LNCS 13703, pages 3-12, 2022. Springer. doi:10.1007/978-3-031-19759-8_1 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/isola/WirsingNJ22, author = {Martin Wirsing and Rocco De Nicola and Stefan J{\"{a}}hnichen}, title = {Rigorous Engineering of Collective Adaptive Systems Introduction to the 4th Track Edition}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part {III}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {3--12}, year = {2022}, series = {LNCS~13703}, publisher = {Springer}, doi = {10.1007/978-3-031-19759-8_1}, pdf = {https://sosy-lab.org/research/pub/2022-ISOLA.Rigorous_Engineering_of_Collective_Adaptive_Systems.pdf}, }
20. Rolf Hennicker, Alexander Knapp, and Martin Wirsing. Epistemic Ensembles. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part III, LNCS 13703, pages 110-126, 2022. Springer. doi:10.1007/978-3-031-19759-8_8 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/isola/HennickerKW22, author = {Rolf Hennicker and Alexander Knapp and Martin Wirsing}, title = {Epistemic Ensembles}, booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part {III}}, editor = {Tiziana Margaria and Bernhard Steffen}, pages = {110--126}, year = {2022}, series = {LNCS~13703}, publisher = {Springer}, doi = {10.1007/978-3-031-19759-8_8}, pdf = {https://sosy-lab.org/research/pub/2022-ISOLA.Epistemic_Ensembles.pdf}, }
21. Xiyue Sun, Fabian Pieroth, Kyrill Schmid, Martin Wirsing, and Lenz Belzner. On Learning Stable Cooperation in the Iterated Prisoner's Dilemma with Paid Incentives. In 42nd IEEE International Conference on Distributed Computing Systems, ICDCS Workshops, Bologna, Italy, July 10, 2022, pages 113-118, 2022. IEEE. doi:10.1109/ICDCSW56584.2022.00031 Publisher's Version PDF
    BibTeX Entry

    @inproceedings{DBLP:conf/icdcs/SunPSWB22, author = {Xiyue Sun and Fabian Pieroth and Kyrill Schmid and Martin Wirsing and Lenz Belzner}, title = {On Learning Stable Cooperation in the Iterated Prisoner's Dilemma with Paid Incentives}, booktitle = {42nd {IEEE} International Conference on Distributed Computing Systems, {ICDCS} Workshops, Bologna, Italy, July 10, 2022}, pages = {113--118}, year = {2022}, publisher = {{IEEE}}, doi = {10.1109/ICDCSW56584.2022.00031}, pdf = {https://sosy-lab.org/research/pub/2022-ICDCSW.On_Learning_Stable_Cooperation_in_the_Iterated_Prisoners_Dilemma_with_Paid_Incentives.pdf}, }

22. Dirk Beyer, Nian-Ze Lee, and Philipp Wendler. Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification. Technical report 2208.05046, arXiv/CoRR, August 2022. doi:10.48550/arXiv.2208.05046 Keyword(s): Software Model Checking, CPAchecker Publisher's Version PDF Presentation Supplement
    Abstract

    Interpolation-based model checking (McMillan, 2003) is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model checking algorithm from 2003 has not been used to verify programs so far. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.
    BibTeX Entry

    @techreport{TechReport22a, author = {Dirk Beyer and Nian-Ze Lee and Philipp Wendler}, title = {Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification}, number = {2208.05046}, year = {2022}, doi = {10.48550/arXiv.2208.05046}, url = {https://www.sosy-lab.org/research/cpa-imc/}, presentation = {https://www.sosy-lab.org/research/prs/2022-08-11_iPRA22_Interpolation_and_SAT-Based_Model_Checking_Revisited.pdf}, abstract = {Interpolation-based model checking <a href="https://doi.org/10.1007/978-3-540-45069-6_1">(McMillan, 2003)</a> is a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. The algorithm is state-of-the-art in hardware model checking. It derives interpolants from unsatisfiable BMC queries, and collects them to construct an overapproximation of the set of reachable states. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's <em>interpolation-based model checking</em> algorithm from 2003 has not been used to verify programs so far. This paper closes this significant, 19 years old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker, and evaluated the implementation against other state-of-the-art software-verification techniques over the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that interpolation-based model checking is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results might have important implications for software verification, because researchers and developers now have a richer set of approaches to choose from.}, keyword = {Software Model Checking, CPAchecker}, _pdf = {https://www.sosy-lab.org/research/cpa-imc/Interpolation_and_SAT-Based_Model_Checking_Revisited.pdf}, institution = {arXiv/CoRR}, month = {August}, }

23. Matthias Dangl. Witness-Based Validation of Verification Results with Applications to Software-Model Checking. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.31508 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    BibTeX Entry

    @misc{DanglWitnesses, author = {Matthias Dangl}, title = {Witness-Based Validation of Verification Results with Applications to Software-Model Checking}, year = {2022}, doi = {10.5282/edoc.31508}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/31508/3/Dangl_Matthias.pdf}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at ARS, Munich, Germany}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-315089}, }
    Additional Infos

    Now at ARS, Munich, Germany
24. Thomas Lemberger. Towards Cooperative Software Verification with Test Generation and Formal Verification. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.32852 Keyword(s): CPAchecker, Software Model Checking, Cooperative Verification Publisher's Version PDF Presentation
    BibTeX Entry

    @misc{LembergerCoop, author = {Thomas Lemberger}, title = {Towards Cooperative Software Verification with Test Generation and Formal Verification}, year = {2022}, doi = {10.5282/edoc.32852}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/32852/1/Lemberger_Thomas.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-12-12_PhD_TowardsCooperativeSoftwareVerification_Thomas.pdf}, keyword = {CPAchecker,Software Model Checking,Cooperative Verification}, annote = {Nominated for the <a href="https://se2024.se.jku.at/ernst-denert-se-preis/">Ernst Denert SE-Preis 2024</a>}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-328522}, }
    Additional Infos

    Nominated for the Ernst Denert SE-Preis 2024
25. Karlheinz Friedberger. Efficient Software Model Checking with Block-Abstraction Memoization. PhD Thesis, LMU Munich, Software Systems Lab, 2022. doi:10.5282/edoc.29976 Keyword(s): CPAchecker, Software Model Checking Publisher's Version PDF
    BibTeX Entry

    @misc{FriedbergerBAM, author = {Karlheinz Friedberger}, title = {Efficient Software Model Checking with Block-Abstraction Memoization}, year = {2022}, doi = {10.5282/edoc.29976}, url = {}, pdf = {https://edoc.ub.uni-muenchen.de/29976/1/Friedberger_Karlheinz.pdf}, presentation = {}, keyword = {CPAchecker,Software Model Checking}, annote = {Now at MSG Systems, Munich, Germany}, howpublished = {PhD Thesis, LMU Munich, Software Systems Lab}, urn = {urn:nbn:de:bvb:19-296471}, }
    Additional Infos

    Now at MSG Systems, Munich, Germany
26. Daniel Baier. Implementation of Value Analysis over Symbolic Memory Graphs in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking, Symbolic Memory Graphs PDF Presentation
    BibTeX Entry

    @misc{BaierSymbolicMemoryGraphs, author = {Daniel Baier}, title = {Implementation of Value Analysis over Symbolic Memory Graphs in CPAchecker}, year = {2022}, pdf = {https://www.sosy-lab.org/research/msc/2022.Baier.Implementation_of_Value_Analysis_over_Symbolic_Memory_Graphs_in_CPAchecker.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-09-28_MA_Implementation_of_Value_Analysis_over_Symbolic_Memory_Graphs_in_CPAchecker_Baier.pdf}, keyword = {CPAchecker,Software Model Checking,Symbolic Memory Graphs}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
27. Martin Pletl. A New Spin on Verification with Symbolic Execution: Symbolic Execution as Formula-Based Predicate Analysis in CPAchecker. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{PletlSymbolicExecution, author = {Martin Pletl}, title = {A New Spin on Verification with Symbolic Execution: Symbolic Execution as Formula-Based Predicate Analysis in CPAchecker}, year = {2022}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
28. Maximilian Hailer. New Approaches and Visualization for Verification Coverage. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry

    @misc{HailerVerificationCoverage, author = {Maximilian Hailer}, title = {New Approaches and Visualization for Verification Coverage}, year = {2022}, pdf = {https://www.sosy-lab.org/research/msc/2022.Hailer.New_Approaches_and_Visualization_for_Verification_Coverage.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-06-16_MA_New_Approaches_and_Visualization_for_Verification_Coverage_Hailer.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
29. Matthias Kettl. Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking PDF Presentation
    BibTeX Entry

    @misc{Kettl, author = {Matthias Kettl}, title = {Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification}, year = {2022}, pdf = {https://www.sosy-lab.org/research/msc/2022.Kettl.Adjustable_Block_Analysis.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-02-24_MA_Adjustable_Block_Analysis.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
30. Philipp Waldinger. Concurrent Software Verification through Block-based Task Partitioning and Continuous Summary Refinement. Master's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker, Software Model Checking
    BibTeX Entry

    @misc{WaldingerTaskPartitioning, author = {Philipp Waldinger}, title = {Concurrent Software Verification through Block-based Task Partitioning and Continuous Summary Refinement}, year = {2022}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }
31. Klara Cimbalnik. Program Transformation in CPAchecker: Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): CPAchecker
    BibTeX Entry

    @misc{CimbalnikCfaExport, author = {Klara Cimbalnik}, title = {Program Transformation in \textsc{CPAchecker}: Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code}, year = {2022}, keyword = {CPAchecker}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
32. Tobias Kleinert. Developing a Verifier Based on Parallel Portfolio with CoVeriTeam. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): Benchmarking PDF Presentation
    BibTeX Entry

    @misc{KleinertParPortfolioCoVeriTeam, author = {Tobias Kleinert}, title = {Developing a Verifier Based on Parallel Portfolio with \textsc{CoVeriTeam}}, year = {2022}, pdf = {https://www.sosy-lab.org/research/bsc/2022.Kleinert.Parallel_Portfolio_CoVeriTeam.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-03-16_BA_Parallel_Portfolio_CoVeriTeam.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }
33. Robin Gloster. Cgroups v2 Support for BenchExec. Bachelor's Thesis, LMU Munich, Software Systems Lab, 2022. Keyword(s): Benchmarking PDF Presentation
    BibTeX Entry

    @misc{GlosterCgroupsV2, author = {Robin Gloster}, title = {Cgroups v2 Support for \textsc{BenchExec}}, year = {2022}, pdf = {https://www.sosy-lab.org/research/bsc/2022.Gloster.Cgroups_v2_Support_for_BenchExec.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2022-03-09_BA_Cgroups_v2_Support_for_BenchExec_Gloster.pdf}, keyword = {Benchmarking}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }