Software and Computational Systems Lab

Funding by DFG-CONVEY

1. Dirk Beyer, Sudeep Kanav, and Henrik Wachowitz. CoVeriTeam Service: Verification as a Service. In TBD, 2023. ACM. To appear. Keyword(s): Software Model Checking, Incremental Verification, Cooperative Verification Funding: DFG-CONVEY PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.7276532
   Abstract

   The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the CoVeriTeam Service and demonstrate its use in a continuous-integration process.
   BibTeX Entry

   @inproceedings{ICSE23, author = {Dirk Beyer and Sudeep Kanav and Henrik Wachowitz}, title = {{CoVeriTeam} Service: Verification as a Service}, booktitle = {TBD}, pages = {}, year = {2023}, publisher = {ACM}, url = {https://coveriteam-service.sosy-lab.org/static/index.html}, pdf = {https://www.sosy-lab.org/research/pub/2023-ICSE.CoVeriTeam_Service_Verification_as_a_Service.pdf}, abstract = {The research community has developed numerous tools for solving verification problems, but we are missing a common interface for executing them. This means users have to spend considerable effort on the installation and parameter setup, for each new tool (version) they want to execute. The situation could make a verification researcher wanting to experiment with a new verification tool turn away from it. We aim to make it easier for users to execute verification tools, as well as provide mechanism for tool developers to make their tools easily accessible. Our solution combines a web service and a common interface for verification tools. The presented service has been used during the 2023 competitions on software verification and testing, for integration testing. As another use- case, we developed a service for incremental verification on top of the {CoVeriTeam} Service and demonstrate its use in a continuous-integration process.}, keyword = {Software Model Checking,Incremental Verification,Cooperative Verification}, _sha256 = {604dd391b6a49e46e97b6faafbb3cc331ccf5c04e3d364cf1e76a2c99c1c267f}, artifact = {10.5281/zenodo.7276532}, doinone = {Unpublished: Last checked: 2023-01-23}, funding = {DFG-CONVEY}, note = {To appear.}, }
2. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Bridging Hardware and Software Analysis with 2C: A Word-Level-Circuit-to-C Translator. In Proc. TACAS, LNCS , 2023. Springer. Keyword(s): Software Model Checking, Cooperative Verification Funding: DFG-CONVEY PDF
   BibTeX Entry

   @inproceedings{TACAS23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Bridging Hardware and Software Analysis with \textsc{Btor2C}: {A} Word-Level-Circuit-to-C Translator}, booktitle = {Proc.\ TACAS}, pages = {}, year = {2023}, series = {LNCS~}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/btor2c/Bridging_Hardware_and_Software_Analysis_with_Btor2C.pdf}, keyword = {Software Model Checking,Cooperative Verification}, doinone = {Unpublished: Last checked: 2023-01-30}, funding = {DFG-CONVEY}, }
3. 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 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}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.Cooperation_between_Automatic_and_Interactive_Software_Verifiers.pdf}, funding = {DFG-CONVEY}, }
4. 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 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}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.A_Unifying_Approach_for_Control-Flow-Based_Loop_Abstraction.pdf}, funding = {DFG-CONVEY}, }
5. 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}, }
6. Dirk Beyer, Karlheinz Friedberger, and Stephan Holzner. PJBDD: A BDD Library for Java and Multi-Threading. In Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21 2021, Gold Coast (Online), Australia, October 18-22), 2021. Springer. doi:10.1007/978-3-030-88885-5_10 Keyword(s): PJBDD, BDD Funding: DFG-CONVEY Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.5070156
   Abstract

   PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.
   BibTeX Entry

   @inproceedings{ATVA21, author = {Dirk Beyer and Karlheinz Friedberger and Stephan Holzner}, title = {{PJBDD}: {A} BDD Library for Java and Multi-Threading}, booktitle = {Proceedings of the 19th International Symposium on Automated Technology for Verification and Analysis (ATVA21~2021, Gold Coast (Online), Australia, October 18-22)}, year = {2021}, publisher = {Springer}, doi = {10.1007/978-3-030-88885-5_10}, pdf = {https://www.sosy-lab.org/research/pub/2021-ATVA.PJBDD_A_BDD_Library_for_Java_and_Multi_Threading.pdf}, abstract = {PJBDD is a flexible and modular Java library for binary decision diagrams (BDD), which are a well-known data structure for performing efficient operations on compressed sets and relations. BDDs have practical applications in composing and analyzing boolean functions, e.g., for computer-aided verification. Despite its importance, there are only a few BDD libraries available. PJBDD is based on a slim object-oriented design, supports multi-threaded execution of the BDD operations (internal) as well as thread-safe access to the operations from applications (external). It provides automatic reference counting and garbage collection. The modular design of the library allows us to provide a uniform API for binary decision diagrams, zero-suppressed decision diagrams, and also chained decision diagrams. This paper includes a compact evaluation of PJBDD, to demonstrate that concurrent operations on large BDDs scale well and parallelize nicely on multi-core CPUs.}, keyword = {PJBDD,BDD}, artifact = {10.5281/zenodo.5070156}, funding = {DFG-CONVEY}, }
7. Daniel Baier, Dirk Beyer, and Karlheinz Friedberger. JavaSMT 3: Interacting with SMT Solvers in Java. In A. Silva and K. R. M. Leino, editors, Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021, Los Angeles, California, USA, July 18-24), LNCS 12760, pages 1-13, 2021. Springer. doi:10.1007/978-3-030-81688-9_9 Keyword(s): JavaSMT Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{CAV21, author = {Daniel Baier and Dirk Beyer and Karlheinz Friedberger}, title = {JavaSMT 3: Interacting with SMT Solvers in Java}, booktitle = {Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV~2021, Los Angeles, California, USA, July 18-24)}, editor = {A.~Silva and K.~R.~M.~Leino}, pages = {1-13}, year = {2021}, series = {LNCS~12760}, publisher = {Springer}, doi = {10.1007/978-3-030-81688-9_9}, sha256 = {6c0ff13c5dd8596e19be4176eefaafe5853d60a082b78ebd3f5e64381fdcb100}, url = {https://github.com/sosy-lab/java-smt}, abstract = {}, keyword = {JavaSMT}, _pdf = {https://www.sosy-lab.org/research/pub/2021-CAV.JavaSMT_3_Interacting_with_SMT_Solvers_in_Java.pdf}, funding = {DFG-CONVEY}, }
8. Dirk Beyer. Software Verification: 10th Comparative Evaluation (SV-COMP 2021). In J. F. Groote and K. G. Larsen, editors, Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021, Luxembourg, Luxembourg, March 27 - April 1), part 2, LNCS 12652, pages 401-422, 2021. Springer. doi:10.1007/978-3-030-72013-1_24 Keyword(s): Competition on Software Verification (SV-COMP), Competition on Software Verification (SV-COMP Report), Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{TACAS21, author = {Dirk Beyer}, title = {Software Verification: 10th Comparative Evaluation ({SV-COMP 2021})}, booktitle = {Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2021, Luxembourg, Luxembourg, March 27 - April 1), part 2}, editor = {J.~F.~Groote and K.~G.~Larsen}, pages = {401-422}, year = {2021}, series = {LNCS~12652}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_24}, sha256 = {d78bb586715b0650702665510258d8e53a7bd16ae2a3cc4568b5986527b29051}, url = {https://sv-comp.sosy-lab.org/2021/}, abstract = {}, keyword = {Competition on Software Verification (SV-COMP),Competition on Software Verification (SV-COMP Report),Software Model Checking}, funding = {DFG-CONVEY}, }
9. Dirk Beyer and Karlheinz Friedberger. Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization. In P. Devanbu, M. Cohen, and T. Zimmermann, editors, Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2020, Virtual Event, USA, November 8-13), pages 50-62, 2020. ACM. doi:10.1145/3368089.3409718 Keyword(s): CPAchecker, Software Model Checking Funding: DFG-CONVEY Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.4024268
   BibTeX Entry

   @inproceedings{FSE20, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization}, booktitle = {Proceedings of the 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE~2020, Virtual Event, USA, November 8-13)}, editor = {P.~Devanbu and M.~Cohen and T.~Zimmermann}, pages = {50-62}, year = {2020}, publisher = {ACM}, doi = {10.1145/3368089.3409718}, url = {https://cpachecker.sosy-lab.org}, keyword = {CPAchecker,Software Model Checking}, _sha256 = {36dc2a423425ee8bec03f0f4073e04f9121d299cc475e27190828e8276e00cb8}, artifact = {10.5281/zenodo.4024268}, funding = {DFG-CONVEY}, fundingid = {378803395}, }
10. Dirk Beyer and Karlheinz Friedberger. Violation Witnesses and Result Validation for Multi-Threaded Programs. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 449-470, 2020. Springer. doi:10.1007/978-3-030-61362-4_26 Keyword(s): CPAchecker, Software Model Checking, Witness-Based Validation, Witness-Based Validation (main) Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    BibTeX Entry

    @inproceedings{ISoLA20c, author = {Dirk Beyer and Karlheinz Friedberger}, title = {Violation Witnesses and Result Validation for Multi-Threaded Programs}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {449-470}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_26}, sha256 = {65fc5325c4e77a80d8e47f9c0e7f0ac02379bfa15dcd9fb54d6587185b8efd77}, url = {https://www.sosy-lab.org/research/witnesses-concurrency/}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-25_ISOLA21_ValidationMultiThreaded_Dirk.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Witness-Based Validation,Witness-Based Validation (main)}, funding = {DFG-CONVEY}, }
11. Dirk Beyer and Sudeep Kanav. An Interface Theory for Program Verification. In T. Margaria and B. Steffen, editors, Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2020, Rhodos, Greece, October 26-30), part 1, LNCS 12476, pages 168-186, 2020. Springer. doi:10.1007/978-3-030-61362-4_9 Keyword(s): CPAchecker, Software Model Checking, Interfaces for Component-Based Design Funding: DFG-CONVEY Publisher's Version PDF Presentation
    BibTeX Entry

    @inproceedings{ISoLA20b, author = {Dirk Beyer and Sudeep Kanav}, title = {An Interface Theory for Program Verification}, booktitle = {Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA~2020, Rhodos, Greece, October 26-30), part~1}, editor = {T.~Margaria and B.~Steffen}, pages = {168-186}, year = {2020}, series = {LNCS~12476}, publisher = {Springer}, doi = {10.1007/978-3-030-61362-4_9}, sha256 = {f15159da0e648a25e57c769639c989e68cd3407bfad10db5ee1dc25e1d2fd672}, url = {}, presentation = {https://www.sosy-lab.org/research/prs/2021-10-29_ISOLA21_VerificationInterfaces_Dirk.pdf}, abstract = {}, keyword = {CPAchecker,Software Model Checking,Interfaces for Component-Based Design}, funding = {DFG-CONVEY}, }
12. Dirk Beyer, Marie-Christine Jakobs, and Thomas Lemberger. Difference Verification with Conditions. In F. d. Boer and A. Cerone, editors, Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM 2020, Virtual, Netherlands, September 14-18), LNCS 12310, pages 133-154, 2020. Springer. doi:10.1007/978-3-030-58768-0_8 Keyword(s): CPAchecker, Software Model Checking Funding: DFG-COOP, DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Abstract

    Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.
    BibTeX Entry

    @inproceedings{SEFM20b, author = {Dirk Beyer and Marie-Christine Jakobs and Thomas Lemberger}, title = {Difference Verification with Conditions}, booktitle = {Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18)}, editor = {F.~d.~Boer and A.~Cerone}, pages = {133--154}, year = {2020}, series = {LNCS~12310}, publisher = {Springer}, doi = {10.1007/978-3-030-58768-0_8}, sha256 = {8e5219da9a998b26f59013c809fbb1db6f92e3f08125fa1bfaacafcfafafef7f}, url = {https://www.sosy-lab.org/research/difference/}, presentation = {https://www.sosy-lab.org/research/prs/2020-09-17_SEFM20_DifferenceVerificationWithConditions_Thomas.pdf}, abstract = {Modern software-verification tools need to support development processes that involve frequent changes. Existing approaches for incremental verification hard-code specific verification techniques. Some of the approaches must be tightly intertwined with the development process. To solve this open problem, we present the concept of difference verification with conditions. Difference verification with conditions is independent from any specific verification technique and can be integrated in software projects at any time. It first applies a change analysis that detects which parts of a software were changed between revisions and encodes that information in a condition. Based on this condition, an off-the-shelf verifier is used to verify only those parts of the software that are influenced by the changes. As a proof of concept, we propose a simple, syntax-based change analysis and use difference verification with conditions with three off-the-shelf verifiers. An extensive evaluation shows the competitiveness of difference verification with conditions.}, keyword = {CPAchecker,Software Model Checking}, funding = {DFG-COOP,DFG-CONVEY}, isbnnote = {}, video = {https://youtu.be/dG02602c9oo}, }
13. 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}, }