Software and Computational Systems Lab

Publications about Incremental Verification

1. Dirk Beyer, Sudeep Kanav, and Henrik Wachowitz. CoVeriTeam Service: Verification as a Service. In Proc. ICSE, pages 21-25, 2023. IEEE. doi:10.1109/ICSE-Companion58688.2023.00017 Keyword(s): Software Model Checking, Incremental Verification, Cooperative Verification Funding: DFG-CONVEY, DFG-COOP Publisher's Version 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 = {Proc.\ ICSE}, pages = {21-25}, year = {2023}, publisher = {IEEE}, doi = {10.1109/ICSE-Companion58688.2023.00017}, 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}, funding = {DFG-CONVEY,DFG-COOP}, }
2. Marie-Christine Jakobs and Tim Pollandt. diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions. In Proc. iFM, LNCS 14300, pages 40-61, 2023. Springer. doi:10.1007/978-3-031-47705-8_3 Keyword(s): Incremental Verification, Regression Verification, Software Model Checking, CPAchecker Funding: Software-Factory 4.0, DFG-ReVeriX Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.8272913
   BibTeX Entry

   @inproceedings{diffDP, author = {Marie{-}Christine Jakobs and Tim Pollandt}, title = {diffDP: Using Data Dependencies and Properties in Difference Verification with Conditions}, booktitle = {Proc.\ iFM}, pages = {40-61}, year = {2023}, series = {LNCS~14300}, publisher = {Springer}, doi = {10.1007/978-3-031-47705-8_3}, url = {}, pdf = {}, keyword = {Incremental Verification, Regression Verification, Software Model Checking, CPAchecker}, annote = {}, artifact = {10.5281/zenodo.8272913}, funding = {Software-Factory 4.0, DFG-ReVeriX}, }

3. Marie-Christine Jakobs and Tim Pollandt. Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report). Technical report 2309.01585, arXiv/CoRR, 2023. doi:10.48550/arXiv.2309.01585 Keyword(s): Incremental Verification, Regression Verification, Software Model Checking, CPAchecker Funding: Software-Factory 4.0, DFG-ReVeriX Publisher's Version PDF
   Artifact(s)

   1. doi:10.5281/zenodo.8272913
   BibTeX Entry

   @techreport{diffDP-TechReport, author = {Marie{-}Christine Jakobs and Tim Pollandt}, title = {Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report)}, number = {2309.01585}, year = {2023}, doi = {10.48550/arXiv.2309.01585}, url = {}, pdf = {}, keyword = {Incremental Verification, Regression Verification, Software Model Checking, CPAchecker}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#diffDP">paper</a> at iFM 2023.}, artifact = {10.5281/zenodo.8272913}, funding = {Software-Factory 4.0, DFG-ReVeriX}, institution = {arXiv/CoRR}, }
   Additional Infos

   This technical report is an extended version of our paper at iFM 2023.