Software and Computational Systems Lab

Publications about Model Checking

1. Dirk Beyer and Henrik Wachowitz. FM-Weck: Containerized Execution of Formal-Methods Tools. In Proceedings of the 26th International Symposium on Formal Methods (FM 2024, Milan, Italy, September 9-13), LNCS 14934, pages 39-47, 2024. Springer. doi:10.1007/978-3-031-71177-0_3 Keyword(s): Software Model Checking, Software Testing, Formal Methods, Verification, Model Checking, Testing, FM-Tools, Tool Conservation, Reproducibility, Satisfiability Modulo Theories, Provers Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.12606323
   Abstract

   Software is ubiquitous in the digital world, and the correct function of software systems is critical for our society, industry, and infrastructure. While testing and static analysis are long-established techniques in software-development processes, it became widely acknowledged only in the past two decades that formal methods are required for giving guarantees of functional correctness. Both academia and industry worked hard to develop tools for formal verification of software during the past two decades, with the result that many software verifiers are available now (for example, 59 freely available verifiers for C and Java programs). However, most software verifiers are challenging to find, install, and use for both external researchers and potential users. FM-Weck changes this: It provides a fully automatic, zero-configuration container-based setup and execution for more than 50 software verifiers for C and Java. Both the setup requirements and execution parameters of every supported verifier are provided by the tool developers themselves as part of the FM-Tools metadata format that was established recently and was already used by the international competitions SV-COMP and Test-Comp. With our solution FM-Weck, anyone gets fast and easy access to state-of-the-art formal verifiers, no expertise required, fully reproducible.
   BibTeX Entry

   @inproceedings{FM24b, author = {Dirk Beyer and Henrik Wachowitz}, title = {FM-Weck: Containerized Execution of Formal-Methods Tools}, booktitle = {Proceedings of the 26th International Symposium on Formal Methods (FM~2024, Milan, Italy, September 9-13)}, pages = {39-47}, year = {2024}, series = {LNCS~14934}, publisher = {Springer}, doi = {10.1007/978-3-031-71177-0_3}, sha256 = {f8f72bb58c83f5622a65e780622182fe592333eefd633b9586fa59df5e913602}, url = {https://gitlab.com/sosy-lab/software/fm-weck}, pdf = {https://www.sosy-lab.org/research/pub/2024-FM.FM-Weck_Containerized_Execution_of_Formal-Methods_Tools.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-09-13_FM_FM-Weck_Henrik.pdf}, abstract = {Software is ubiquitous in the digital world, and the correct function of software systems is critical for our society, industry, and infrastructure. While testing and static analysis are long-established techniques in software-development processes, it became widely acknowledged only in the past two decades that formal methods are required for giving guarantees of functional correctness. Both academia and industry worked hard to develop tools for formal verification of software during the past two decades, with the result that many software verifiers are available now (for example, 59 freely available verifiers for C and Java programs). However, most software verifiers are challenging to find, install, and use for both external researchers and potential users. FM-Weck changes this: It provides a fully automatic, zero-configuration container-based setup and execution for more than 50 software verifiers for C and Java. Both the setup requirements and execution parameters of every supported verifier are provided by the tool developers themselves as part of the FM-Tools metadata format that was established recently and was already used by the international competitions SV-COMP and Test-Comp. With our solution FM-Weck, anyone gets fast and easy access to state-of-the-art formal verifiers, no expertise required, fully reproducible.}, keyword = {Software Model Checking, Software Testing, Formal Methods, Verification, Model Checking, Testing, FM-Tools, Tool Conservation, Reproducibility, Satisfiability Modulo Theories, Provers}, artifact = {10.5281/zenodo.12606323}, funding = {DFG-CONVEY}, }