Publications of Matthias Kettl
Articles in conference or workshop proceedings
-
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)
-
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}, } -
A Collection of Real-World Benchmark Tasks for Repair of Partial Program Fixes.
Research Internship, LMU Munich, Software Systems Lab,
2021.
BibTeX Entry
@misc{KettlPartialProgramFixesBenchmarkSet, author = {Matthias Kettl}, title = {A Collection of Real-World Benchmark Tasks for Repair of Partial Program Fixes}, year = {2021}, keyword = {}, howpublished = {Research Internship, LMU Munich, Software Systems Lab}, } -
Fault Localization for Formal Verification: An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores.
Bachelor's Thesis, LMU Munich, Software Systems Lab,
2020.
Keyword(s): CPAchecker, Software Model Checking
PDF
Presentation
BibTeX Entry
@misc{KettlFaultLocalization, author = {Matthias Kettl}, title = {Fault Localization for Formal Verification: An Implementation and Evaluation of Algorithms based on Error Invariants and UNSAT-cores}, year = {2020}, pdf = {https://www.sosy-lab.org/research/bsc/2020.Kettl.Fault_Localization_for_Formal_Verification_An_Implementation_and_Evaluation_of_Algorithms_based_on_Error_Invariants_and_UNSAT-cores.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2020-07-22_BA_FaultLocalizationWithUnsatCores_Kettl.pdf}, keyword = {CPAchecker, Software Model Checking}, annote = {Won the LMU research award for excellent students (LMU Forschungspreis f{\"u}r exzellente Studierende) of LMU Munich}, field = {Computer Science}, howpublished = {Bachelor's Thesis, LMU Munich, Software Systems Lab}, }Additional Infos
Won the LMU research award for excellent students (LMU Forschungspreis für exzellente Studierende) of LMU Munich
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.