Publications of year 2022
Articles in journal or book chapters
-
Verification Witnesses.
ACM Trans. Softw. Eng. Methodol.,
2022.
doi:10.1145/3477579
Publisher's Version
PDF
Supplement
BibTeX Entry
@article{WitnessesACM, 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.}, year = {2022}, doi = {10.1145/3477579}, sha256 = {f1e792b1d6bbdb1bbd125ecda1cf76a937699421ae5702b7688e3e60a4837289}, url = {https://www.sosy-lab.org/research/verification-witnesses-tosem/}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TOSEM.Verification_Witnesses.pdf}, } -
Agile governance for innovating higher education teaching and learning.
Rivista di Digital Politics,
2022.
To appear.
PDF
BibTeX Entry
@article{WirsingF21, author = {Martin Wirsing and Dieter Frey}, title = {Agile governance for innovating higher education teaching and learning}, journal = {Rivista di Digital Politics}, year = {2022}, pdf = {https://sosy-lab.org/research/pub/2022-Rivista.Agile_governance_for_innovating_higher_education_teaching_and_learning.pdf}, doinone = {Unpublished: Last checked: 2022-03-07}, note = {To appear.}, }
Articles in conference or workshop proceedings
-
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)),
2022.
ACM.
Keyword(s): CPAchecker, Software Model Checking, Interfaces for Component-Based Design Funding: DFG-COOP
PDF
Supplement
Artifact(s)
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))}, year = {2022}, publisher = {ACM}, url = {https://www.sosy-lab.org/research/component-based-cegar/}, pdf = {https://www.sosy-lab.org/research/pub/2022-ICSE.Decomposing_Software_Verification_into_Off-the-Shelf-Components.pdf}, 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}, artifact = {10.5281/zenodo.5301636}, doinone = {Unpublished: Last checked: 2022-02-19}, funding = {DFG-COOP}, } -
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}, } -
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}, } -
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 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_TACAS/2022-04-06_TACAS22_CoVeriTeam_Sudeep.pdf}, abstract = {}, keyword = {Software Model Checking}, funding = {DFG-COOP}, } -
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}, } -
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}, } -
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.
To appear.
BibTeX Entry
@inproceedings{ernst:saner2022, author = {Dongge Liu and Van-Thuan Pham and Gidon Ernst and Toby Murray and Benjamin 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}, note = {To appear.}, } -
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 = {Gidon Ernst}, 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}, } -
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)}, }
Theses and projects (PhD, MSc, BSc, Project)
-
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 -
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}, } -
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}, } -
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}, } -
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 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}, } -
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 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}, }
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.