Software and Computational Systems Lab

Publications of Matthias Kettl

1. 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)}, }

1. 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}, }
2. Matthias Kettl. 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}, }
3. Matthias Kettl. 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