Software and Computational Systems Lab

Publications of Martin Spiessl

1. Paulína Ayaziová, Dirk Beyer, Marian Lingsch-Rosenfeld, Martin Spiessl, and Jan Strejček. Software Verification Witnesses 2.0. In Proc. SPIN, LNCS , 2024. Springer. Keyword(s): Software Model Checking, Cooperative Verification, Witness-Based Validation, CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX PDF Supplement
   BibTeX Entry

   @inproceedings{SPIN24c, author = {Paulína Ayaziová and Dirk Beyer and Marian Lingsch-Rosenfeld and Martin Spiessl and Jan Strejček}, title = {Software Verification Witnesses 2.0}, booktitle = {Proc.\ SPIN}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, url = {https://gitlab.com/sosy-lab/benchmarking/sv-witnesses/}, pdf = {https://www.sosy-lab.org/research/pub/2024-SPIN.Software_Verification_Witnesses_2.0.pdf}, abstract = {}, keyword = {Software Model Checking, Cooperative Verification, Witness-Based Validation, CPAchecker}, annote = {}, artifact = {}, doinone = {Unpublished: Last checked: 2024-03-25}, funding = {DFG-CONVEY,DFG-IDEFIX}, }
2. Daniel Baier, Dirk Beyer, Po-Chun Chien, Marek Jankola, Matthias Kettl, Nian-Ze Lee, Thomas Lemberger, Marian Lingsch-Rosenfeld, Martin Spiessl, Henrik Wachowitz, and Philipp Wendler. CPAchecker 2.3 with Strategy Selection (Competition Contribution). In Proc. TACAS (3), LNCS 14572, pages 359-364, 2024. Springer. doi:10.1007/978-3-031-57256-2_21 Keyword(s): Software Model Checking, Witness-Based Validation, CPAchecker Funding: DFG-CONVEY, DFG-IDEFIX Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10203297
   Abstract

   CPAchecker is a versatile framework for software verification, rooted in the established concept of configurable program analysis. Compared to the last published system description at SV-COMP 2015, the CPAchecker submission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses in CPAchecker and cover the full spectrum of the diverse program characteristics and specifications in the competition, we use strategy selection to predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses using k-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms in CPAchecker enables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories. CPAchecker also generates verification witnesses in the new YAML format.
   BibTeX Entry

   @inproceedings{TACAS24c, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Martin Spiessl and Henrik Wachowitz and Philipp Wendler}, title = {{CPAchecker} 2.3 with Strategy Selection (Competition Contribution)}, booktitle = {Proc.\ TACAS~(3)}, pages = {359-364}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_21}, url = {https://cpachecker.sosy-lab.org/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPAchecker_2.3_with_Strategy_Selection_Competition_Contribution.pdf}, abstract = {CPAchecker is a versatile framework for software verification, rooted in the established concept of configurable program analysis. Compared to the last published system description at SV-COMP 2015, the CPAchecker submission to SV-COMP 2024 incorporates new analyses for reachability safety, memory safety, termination, overflows, and data races. To combine forces of the available analyses in CPAchecker and cover the full spectrum of the diverse program characteristics and specifications in the competition, we use strategy selection to predict a sequential portfolio of analyses that is suitable for a given verification task. The prediction is guided by a set of carefully picked program features. The sequential portfolios are composed based on expert knowledge and consist of bit-precise analyses using <i>k</i>-induction, data-flow analysis, SMT solving, Craig interpolation, lazy abstraction, and block-abstraction memoization. The synergy of various algorithms in CPAchecker enables support for all properties and categories of C programs in SV-COMP 2024 and contributes to its success in many categories. CPAchecker also generates verification witnesses in the new YAML format.}, keyword = {Software Model Checking, Witness-Based Validation, CPAchecker}, artifact = {10.5281/zenodo.10203297}, funding = {DFG-CONVEY, DFG-IDEFIX}, }
3. Dirk Beyer and Martin Spiessl. LIV: Invariant Validation using Straight-Line Programs. In Proc. ASE, pages 2074-2077, 2023. IEEE. doi:10.1109/ASE56229.2023.00214 Keyword(s): Software Model Checking, Witness-Based Validation Funding: DFG-CONVEY Publisher's Version PDF Video Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.8289101
   Abstract

   Validation of correctness proofs is an established procedure in software verification. While there are steady advances when it comes to verification of more and more complex software systems, it becomes increasingly hard to determine which information is actually useful for validation of the correctness proof. Usually, the central piece that verifiers struggle to come up with are good loop invariants. While a proof using inductive invariants is easy to validate, not all invariants used by verifiers necessarily are inductive. In order to alleviate this problem, we propose LIV, an approach that makes it easy to check if the invariant information provided by the verifier is sufficient to establish an inductive proof. This is done by emulating a Hoare-style proof, splitting the program into Hoare triples and converting these into verification tasks that can themselves be efficiently verified by an off-the-shelf verifier. In case the validation fails, useful information about the failure reason can be extracted from the overview of which triples could be established and which were refuted. We show that our approach works by evaluating it on a state-of-the-art benchmark set.
   BibTeX Entry

   @inproceedings{ASE23b, author = {Dirk Beyer and Martin Spiessl}, title = {LIV: Invariant Validation using Straight-Line Programs}, booktitle = {Proc.\ ASE}, pages = {2074-2077}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00214}, url = {https://www.sosy-lab.org/research/liv}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.LIV_Loop-Invariant_Validation_using_Straight-Line_Programs.pdf}, abstract = {Validation of correctness proofs is an established procedure in software verification. While there are steady advances when it comes to verification of more and more complex software systems, it becomes increasingly hard to determine which information is actually useful for validation of the correctness proof. Usually, the central piece that verifiers struggle to come up with are good loop invariants. While a proof using inductive invariants is easy to validate, not all invariants used by verifiers necessarily are inductive. In order to alleviate this problem, we propose LIV, an approach that makes it easy to check if the invariant information provided by the verifier is sufficient to establish an inductive proof. This is done by emulating a Hoare-style proof, splitting the program into Hoare triples and converting these into verification tasks that can themselves be efficiently verified by an off-the-shelf verifier. In case the validation fails, useful information about the failure reason can be extracted from the overview of which triples could be established and which were refuted. We show that our approach works by evaluating it on a state-of-the-art benchmark set.}, keyword = {Software Model Checking, Witness-Based Validation}, artifact = {10.5281/zenodo.8289101}, funding = {DFG-CONVEY}, video = {https://youtu.be/mZhoGAa08Rk}, }
4. Dirk Beyer, Marian Lingsch-Rosenfeld, and Martin Spiessl. CEGAR-PT: A Tool for Abstraction by Program Transformation. In Proc. ASE, pages 2078-2081, 2023. IEEE. doi:10.1109/ASE56229.2023.00215 Keyword(s): Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Video Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.8287183
   Abstract

   Abstraction is a key technology for proving the correctness of computer programs. There are many approaches available, but unfortunately, the various techniques are difficult to combine and the successful techniques have to be re-implemented again and again.
   We address this problem by using the tool CEGAR-PT, which views abstraction as program transformation and integrates different verification components off-the-shelf. The idea is to use existing components without having to change their implementation, while still adjusting the precision of the abstraction using the successful CEGAR approach. The approach is largely general: it only restricts the abstraction to transform, given a precision that defines the level of abstraction, one program into another program. The abstraction by program transformation can over-approximate the data flow (e.g., havoc some variables, use more abstract types) or the control flow (e.g., loop abstraction, slicing).
   BibTeX Entry

   @inproceedings{ASE23c, author = {Dirk Beyer and Marian Lingsch-Rosenfeld and Martin Spiessl}, title = {CEGAR-PT: A Tool for Abstraction by Program Transformation}, booktitle = {Proc.\ ASE}, pages = {2078-2081}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00215}, url = {https://www.sosy-lab.org/research/cegar-pt}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.CEGAR-PT_A_Tool_for_Abstraction_by_Program_Transformation.pdf}, abstract = {Abstraction is a key technology for proving the correctness of computer programs. There are many approaches available, but unfortunately, the various techniques are difficult to combine and the successful techniques have to be re-implemented again and again. <br> We address this problem by using the tool CEGAR-PT, which views abstraction as program transformation and integrates different verification components off-the-shelf. The idea is to use existing components without having to change their implementation, while still adjusting the precision of the abstraction using the successful CEGAR approach. The approach is largely general: it only restricts the abstraction to transform, given a precision that defines the level of abstraction, one program into another program. The abstraction by program transformation can over-approximate the data flow (e.g., havoc some variables, use more abstract types) or the control flow (e.g., loop abstraction, slicing).}, keyword = {Software Model Checking}, artifact = {10.5281/zenodo.8287183}, funding = {DFG-CONVEY}, video = {https://youtu.be/ASZ6hoq8asE}, }
5. 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}, }
6. 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}, }
7. 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}, }
8. Dirk Beyer and Martin Spiessl. MetaVal: Witness Validation via Verification. In S. K. Lahiri and C. Wang, editors, Proceedings of the 32nd International Conference on Computer Aided Verification (CAV 2020, Virtual, USA, July 21-24), part 2, LNCS 12225, pages 165-177, 2020. Springer. doi:10.1007/978-3-030-53291-8_10 Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{CAV20, author = {Dirk Beyer and Martin Spiessl}, title = {MetaVal: {W}itness Validation via Verification}, booktitle = {Proceedings of the 32nd International Conference on Computer Aided Verification (CAV~2020, Virtual, USA, July 21-24), part 2}, editor = {S.~K.~Lahiri and C.~Wang}, pages = {165-177}, year = {2020}, series = {LNCS~12225}, publisher = {Springer}, doi = {10.1007/978-3-030-53291-8_10}, sha256 = {7431085a248c7e2cab70318096622ff19ce1124067158d08866d3f9b250df44e}, url = {https://gitlab.com/sosy-lab/software/metaval}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, isbnnote = {978-3-030-53290-1}, }

1. Martin Spiessl. Configurable Software Verification based on Slicing Abstractions. Master's Thesis, LMU Munich, Software Systems Lab, 2018. Keyword(s): CPAchecker, Software Model Checking PDF
   BibTeX Entry

   @misc{MartinSplitting, author = {Martin Spiessl}, title = {Configurable Software Verification based on Slicing Abstractions}, year = {2018}, pdf = {https://www.sosy-lab.org/research/msc/2018.Spiessl.Configurable_Software_Verification_based_on_Slicing_Abstractions.pdf}, keyword = {CPAchecker,Software Model Checking}, howpublished = {Master's Thesis, LMU Munich, Software Systems Lab}, }