Publications by year

2024

1. Dirk Beyer, Po-Chun Chien, Marek Jankola, and Nian-Ze Lee. A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification. Proc. ACM Softw. Eng.(FSE), 2024. Funding: DFG-CONVEY
   BibTeX Entry

   @article{ItpTransfer-PACMSE, author = {Dirk Beyer and Po-Chun Chien and Marek Jankola and Nian-Ze Lee}, title = {A Transferability Study of Interpolation-Based Hardware Model Checking to Software Verification}, journal = {Proc. ACM Softw. Eng.}, volume = {}, number = {FSE}, pages = {}, year = {2024}, doi = {}, url = {}, pdf = {}, presentation = {}, abstract = {}, artifact = {}, funding = {DFG-CONVEY}, }
2. 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. Funding: DFG-CONVEY, DFG-IDEFIX PDF Presentation 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}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-11_SPIN24_Software-Verification-Witnesses-2.0.pdf}, abstract = {}, annote = {}, artifact = {}, doinone = {Unpublished: Last checked: 2024-03-25}, funding = {DFG-CONVEY,DFG-IDEFIX}, }
3. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants. In Proc. SPIN, 2024. Springer. Funding: DFG-CONVEY PDF Presentation Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10548594
   Abstract

   Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
   BibTeX Entry

   @inproceedings{SPIN24b, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants}, booktitle = {Proc.\ SPIN}, pages = {}, year = {2024}, series = {}, publisher = {Springer}, url = {https://www.sosy-lab.org/research/imc-df/}, pdf = {https://www.sosy-lab.org/research/pub/2024-SPIN.Augmenting_Interpolation-Based_Model_Checking_with_Auxiliary_Invariants.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-10_SPIN_Augmenting_IMC_with_Auxiliary_Invariants_Po-Chun.pdf}, abstract = {Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including <i>k</i>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.}, annote = {This article received the "Best Paper Award" at SPIN 2024! An <a href="https://www.sosy-lab.org/research/bib/All/index.html#TechReport24a">extended version</a> of this article is available on <a href="https://doi.org/10.48550/arXiv.2403.07821">arXiv</a>.}, artifact = {10.5281/zenodo.10548594}, doinone = {Unpublished: Last checked: 2024-03-16}, funding = {DFG-CONVEY}, }
   Additional Infos

   This article received the "Best Paper Award" at SPIN 2024! An extended version of this article is available on arXiv.
4. Dirk Beyer, Matthias Kettl, and Thomas Lemberger. Fault Localization on Verification Witnesses. In Proceedings of the 30th International Symposium on Model Checking Software (SPIN 2024, Luxembourg City, Luxembourg, April 10-11), LNCS, 2024. Springer. Funding: DFG-CONVEY, DFG-IDEFIX, DFG-COOP PDF
   Artifact(s)

   1. doi:10.5281/zenodo.10794627
   Abstract

   When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.
   BibTeX Entry

   @inproceedings{SPIN24a, author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger}, title = {Fault Localization on Verification Witnesses}, booktitle = {Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11)}, pages = {}, year = {2024}, series = {LNCS}, publisher = {Springer}, pdf = {https://sosy-lab.org/research/pub/2024-SPIN.Fault_Localization_on_Verification_Witnesses.pdf}, abstract = {When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.}, annote = {Nominated for best paper.<br> This work was also presented with a poster at the 46th International Conference on Software Engineering (ICSE 2024, Lisbon, Portugal, April 14-20): <a href="https://sosy-lab.org/research/pst/2024-03-05_ICSE24_Fault_Localization_on_Verification_Witnesses_Poster.pdf">Extended Abstract</a>.}, artifact = {10.5281/zenodo.10794627}, doinone = {TBD}, funding = {DFG-CONVEY,DFG-IDEFIX,DFG-COOP}, }
   Additional Infos

   Nominated for best paper.
   This work was also presented with a poster at the 46th International Conference on Software Engineering (ICSE 2024, Lisbon, Portugal, April 14-20): Extended Abstract.
5. 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 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.}, artifact = {10.5281/zenodo.10203297}, funding = {DFG-CONVEY, DFG-IDEFIX}, }
6. Dirk Beyer. State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024, Luxembourg, Luxembourg, April 6-11), part 3, LNCS 14572, pages 299-329, 2024. Springer. doi:10.1007/978-3-031-57256-2_15 Funding: DFG-CONVEY Publisher's Version PDF Supplement
   BibTeX Entry

   @inproceedings{TACAS24b, author = {Dirk Beyer}, title = {State of the Art in Software Verification and Witness Validation: {SV-COMP 2024}}, booktitle = {Proceedings of the 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2024, Luxembourg, Luxembourg, April 6-11), part~3}, pages = {299-329}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_15}, sha256 = {}, url = {https://sv-comp.sosy-lab.org/2024/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.State_of_the_Art_in_Software_Verification_and_Witness_Validation_SV-COMP_2024.pdf}, funding = {DFG-CONVEY}, }
7. Zsófia Ádám, Dirk Beyer, Po-Chun Chien, Nian-Ze Lee, and Nils Sirrenberg. Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers. In Proc. TACAS (3), LNCS 14572, pages 129-149, 2024. Springer. doi:10.1007/978-3-031-57256-2_7 Funding: DFG-CONVEY Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10548597
   Abstract

   Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier CBMC on translated programs, it uniquely solved, with confirmed witnesses, 8% of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.
   BibTeX Entry

   @inproceedings{TACAS24a, author = {Zsófia Ádám and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee and Nils Sirrenberg}, title = {{Btor2-Cert}: {A} Certifying Hardware-Verification Framework Using Software Analyzers}, booktitle = {Proc.\ TACAS~(3)}, pages = {129-149}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_7}, url = {https://www.sosy-lab.org/research/btor2-cert/}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.Btor2-Cert_A_Certifying_Hardware-Verification_Framework_Using_Software_Analyzers.pdf}, abstract = {Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the confidence in verification results by generating a witness for other tools to validate the verdict independently. Recently, translating the hardware-modeling language Btor2 to software, such as the programming language C or LLVM intermediate representation, has been actively studied and facilitated verifying hardware designs by software analyzers. However, it remained unknown whether witnesses produced by software verifiers contain helpful information about the original circuits and how such information can aid hardware analysis. We propose a certifying and validating framework Btor2-Cert to verify safety properties of Btor2 circuits, combining Btor2-to-C translation, software verifiers, and a new witness validator Btor2-Val, to answer the above open questions. Btor2-Cert translates a software violation witness to a Btor2 violation witness; As the Btor2 language lacks a format for correctness witnesses, we encode invariants in software correctness witnesses as Btor2 circuits. The validator Btor2-Val checks violation witnesses by circuit simulation and correctness witnesses by validation via verification. In our evaluation, Btor2-Cert successfully utilized software witnesses to improve quality assurance of hardware. By invoking the software verifier CBMC on translated programs, it uniquely solved, with confirmed witnesses, 8&percnt; of the unsafe tasks for which the hardware verifier ABC failed to detect bugs.}, annote = {The reproduction package of this article received the "Distinguished Artifact Award" at TACAS 2024!}, artifact = {10.5281/zenodo.10548597}, funding = {DFG-CONVEY}, }
   Additional Infos

   The reproduction package of this article received the "Distinguished Artifact Award" at TACAS 2024!
8. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version). Technical report 2403.07821, arXiv/CoRR, March 2024. doi:10.48550/arXiv.2403.07821 Funding: DFG-CONVEY Publisher's Version PDF Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.10548594
   Abstract

   Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
   BibTeX Entry

   @techreport{TechReport24a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)}, number = {2403.07821}, year = {2024}, doi = {10.48550/arXiv.2403.07821}, url = {https://www.sosy-lab.org/research/imc-df/}, pdf = {https://arxiv.org/abs/2403.07821}, abstract = {Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including <i>k</i>-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#SPIN24b">paper</a> at SPIN 2024.}, artifact = {10.5281/zenodo.10548594}, funding = {DFG-CONVEY}, institution = {arXiv/CoRR}, month = {March}, }
   Additional Infos

   This technical report is an extended version of our paper at SPIN 2024.

2023

9. Sabanayagam, Mahalakshmi, Behrens, Freya, Adomaityte, Urte, and Dawid, Anna. Unveiling the Hessian's Connection to the Decision Boundary. CoRR, June 2023. doi:10.48550/ARXIV.2306.07104 Funding: DFG-CONVEY Publisher's Version PDF
   BibTeX Entry

   @article{SabanayagamBAD23, author = {Sabanayagam, Mahalakshmi and Behrens, Freya and Adomaityte, Urte and Dawid, Anna}, title = {Unveiling the Hessian's Connection to the Decision Boundary}, journal = {CoRR}, year = {2023}, doi = {10.48550/ARXIV.2306.07104}, dblp_id = {journals/corr/abs-2306-07104}, funding = {DFG-CONVEY}, month = {June}, type = {preprint}, }
10. Czerner, Philipp, Esparza, Javier, and Leroux, Jérôme. Lower Bounds on the State Complexity of Population Protocols. Distributed Comput., 2023. doi:10.1007/s00446-023-00450-4 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @article{CzernerEL23, author = {Czerner, Philipp and Esparza, Javier and Leroux, Jérôme}, title = {Lower Bounds on the State Complexity of Population Protocols}, journal = {Distributed Comput.}, year = {2023}, doi = {10.1007/s00446-023-00450-4}, url = {https://arxiv.org/abs/2102.11619}, dblp_id = {none}, funding = {DFG-CONVEY}, }
11. Kochdumper, Niklas, Krasowski, Hanna, Wang, Xiao, Bak, Stanley, and Althoff, Matthias. Provably Safe Reinforcement Learning via Action Projection using Reachability Analysis and Polynomial Zonotopes. IEEE Open Journal of Control Systems, 2:79-92, 2023. doi:10.1109/OJCSYS.2023.3256305 Funding: DFG-CONVEY Publisher's Version PDF Video
    BibTeX Entry

    @article{KochdumperKWBA22, author = {Kochdumper, Niklas and Krasowski, Hanna and Wang, Xiao and Bak, Stanley and Althoff, Matthias}, title = {Provably Safe Reinforcement Learning via Action Projection using Reachability Analysis and Polynomial Zonotopes}, journal = {IEEE Open Journal of Control Systems}, volume = {2}, pages = {79-92}, year = {2023}, doi = {10.1109/OJCSYS.2023.3256305}, pdf = {https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=10068193}, dblp_id = {none}, funding = {DFG-CONVEY}, video = {https://www.youtube.com/watch?v=6ISKxO4DDWA}, }
12. Singh, Anurag, Sabanayagam, Mahalakshmi, Ghoshdastidar, Debarghya, and Muandet, Kirkamol. Fast Adaptive Test-Time Defense with Robust Features. 2023. Funding: DFG-CONVEY
    BibTeX Entry

    @article{sabanayagam2023fast, author = {Singh, Anurag and Sabanayagam, Mahalakshmi and Ghoshdastidar, Debarghya and Muandet, Kirkamol}, title = {Fast Adaptive Test-Time Defense with Robust Features}, year = {2023}, dblp_id = {none}, funding = {DFG-CONVEY}, type = {preprint}, }
13. Jahanshahi, Niloofar and Zamani, Majid. Synthesis of Controllers for Partially-Observable Systems: A Data-Driven Approach. IFAC-PapersOnLine, 2023. Elsevier. Funding: DFG-CONVEY
    BibTeX Entry

    @article{jahanshahi2023data, author = {Jahanshahi, Niloofar and Zamani, Majid}, title = {Synthesis of Controllers for Partially-Observable Systems: A Data-Driven Approach}, journal = {IFAC-PapersOnLine}, year = {2023}, publisher = {Elsevier}, dblp_id = {none}, funding = {DFG-CONVEY}, }
14. Anand, Mahathi and Zamani, Majid. Formally Verified Neural Network Control Barrier Certificates . 22nd IFAC World Congress, 2023. Funding: DFG-CONVEY
    BibTeX Entry

    @article{ANANDNN, author = {Anand, Mahathi and Zamani, Majid}, title = {Formally Verified Neural Network Control Barrier Certificates}, journal = {22nd IFAC World Congress}, year = {2023}, dblp_id = {none}, funding = {DFG-CONVEY}, }
15. Tilscher, Sarah, Stade, Yannick, Schwarz, Michael, Vogler, Ralf, and Seidl, Helmut. The Top-Down-Solver — An Exercise in A²I. In Challenges of Software Verification, 2023. Springer Nature Singapore. Funding: DFG-CONVEY
    BibTeX Entry

    @incollection{Tilscher2023, author = {Tilscher, Sarah and Stade, Yannick and Schwarz, Michael and Vogler, Ralf and Seidl, Helmut}, title = {The Top-Down-Solver — An Exercise in A²I}, booktitle = {Challenges of Software Verification}, year = {2023}, publisher = {Springer Nature Singapore}, dblp_id = {none}, funding = {DFG-CONVEY}, }
16. Maximilian Schäffeler and Mohammad Abdulaziz. Formally Verified Solution Methods for Markov Decision Processes. In Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 15073-15081, February 2023. AAAI Press. doi:10.1609/aaai.v37i12.26759 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{SchaffelerA23, author = {Maximilian Sch{\"{a}}ffeler and Mohammad Abdulaziz}, title = {Formally Verified Solution Methods for Markov Decision Processes}, booktitle = {Thirty-Seventh {AAAI} Conference on Artificial Intelligence, {AAAI} 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, {IAAI} 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, {EAAI} 2023, Washington, DC, USA, February 7-14, 2023}, pages = {15073--15081}, year = {2023}, publisher = {{AAAI} Press}, doi = {10.1609/aaai.v37i12.26759}, url = {https://doi.org/10.1609/aaai.v37i12.26759}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/aaai/SchaffelerA23.bib}, dblp_id = {conf/aaai/SchaffelerA23}, funding = {DFG-CONVEY}, month = {February}, timestamp = {Mon, 04 Sep 2023 16:50:27 +0200}, }
17. Michael Schwarz, Simmo Saan, Helmut Seidl, Julian Erhard, and Vesal Vojdani. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. In Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, LNCS, pages 28-58, April 2023. Springer. doi:10.1007/978-3-031-30044-8_2 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SchwarzSSEV23, author = {Michael Schwarz and Simmo Saan and Helmut Seidl and Julian Erhard and Vesal Vojdani}, title = {Clustered Relational Thread-Modular Abstract Interpretation with Local Traces}, booktitle = {Programming Languages and Systems - 32nd European Symposium on Programming, {ESOP} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2023, Paris, France, April 22-27, 2023, Proceedings}, volume = {13990}, pages = {28--58}, year = {2023}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-031-30044-8_2}, dblp_id = {conf/esop/SchwarzSSEV23}, funding = {DFG-CONVEY}, month = {April}, }
18. Simmo Saan, Michael Schwarz, Julian Erhard, Manuel Pietsch, Helmut Seidl, Sarah Tilscher, and Vesal Vojdani. Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, LNCS, pages 547-552, April 2023. Springer. doi:10.1007/978-3-031-30820-8_34 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{SaanSEPSTV23, author = {Simmo Saan and Michael Schwarz and Julian Erhard and Manuel Pietsch and Helmut Seidl and Sarah Tilscher and Vesal Vojdani}, title = {Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution)}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, {TACAS} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Paris, France, April 22-27, 2023, Proceedings, Part {II}}, volume = {13994}, pages = {547--552}, year = {2023}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_34}, url = {https://doi.org/10.1007/978-3-031-30820-8\_34}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/tacas/SaanSEPSTV23.bib}, dblp_id = {conf/tacas/SaanSEPSTV23}, funding = {DFG-CONVEY}, month = {April}, timestamp = {Sat, 13 May 2023 01:07:18 +0200}, }
19. Pascal Mattia Esser, Satyaki Mukherjee, Mahalakshmi Sabanayagam, and Debarghya Ghoshdastidar. Improved Representation Learning Through Tensorized Autoencoders. In International Conference on Artificial Intelligence and Statistics, 25-27 April 2023, Palau de Congressos, Valencia, Spain, Proceedings of Machine Learning Research, pages 8294-8307, April 2023. PMLR. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @inproceedings{EsserMSG23, author = {Pascal Mattia Esser and Satyaki Mukherjee and Mahalakshmi Sabanayagam and Debarghya Ghoshdastidar}, title = {Improved Representation Learning Through Tensorized Autoencoders}, booktitle = {International Conference on Artificial Intelligence and Statistics, 25-27 April 2023, Palau de Congressos, Valencia, Spain}, volume = {206}, pages = {8294--8307}, year = {2023}, series = {Proceedings of Machine Learning Research}, publisher = {{PMLR}}, url = {https://proceedings.mlr.press/v206/esser23a.html}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/aistats/EsserMSG23.bib}, dblp_id = {conf/aistats/EsserMSG23}, funding = {DFG-CONVEY}, month = {April}, timestamp = {Mon, 19 Jun 2023 16:44:26 +0200}, }
20. M. Wetzlinger, N. Kochdumper, S. Bak, and M. Althoff. Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions. In Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2023, San Antonio, TX, USA, May 9-12, 2023, May 2023. ACM. doi:10.1145/3575870.3587121 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{WetzlingerKBA23, author = {M. Wetzlinger and N. Kochdumper and S. Bak and M. Althoff}, title = {Fully-Automated Verification of Linear Systems Using Reachability Analysis with Support Functions}, booktitle = {Proceedings of the 26th {ACM} International Conference on Hybrid Systems: Computation and Control, {HSCC} 2023, San Antonio, TX, USA, May 9-12, 2023}, year = {2023}, publisher = {ACM}, doi = {10.1145/3575870.3587121}, url = {https://doi.org/10.1145/3575870.3587121}, articleno = {5}, dblp_id = {conf/hybrid/WetzlingerKBA23}, funding = {DFG-CONVEY}, keywords = {high-dimensional systems, automated parameter tuning, iterative refinement, Formal verification, set-based computing, counterexample.}, month = {May}, numpages = {12}, }
21. Philipp Czerner. Brief Announcement: Population Protocols Decide Double-exponential Thresholds. In Proceedings of the 2023 ACM Symposium on Principles of Distributed Computing, PODC 2023, Orlando, FL, USA, June 19-23, 2023, pages 28-31, June 2023. ACM. doi:10.1145/3583668.3594571 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{Czerner23, author = {Philipp Czerner}, title = {Brief Announcement: Population Protocols Decide Double-exponential Thresholds}, booktitle = {Proceedings of the 2023 {ACM} Symposium on Principles of Distributed Computing, {PODC} 2023, Orlando, FL, USA, June 19-23, 2023}, pages = {28--31}, year = {2023}, publisher = {{ACM}}, doi = {10.1145/3583668.3594571}, url = {https://doi.org/10.1145/3583668.3594571}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/podc/Czerner23.bib}, dblp_id = {conf/podc/Czerner23}, funding = {DFG-CONVEY}, month = {June}, timestamp = {Mon, 19 Jun 2023 08:58:36 +0200}, }
22. Michael Schwarz, Julian Erhard, Vesal Vojdani, Simmo Saan, and Helmut Seidl. When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2023, Orlando, FL, USA, 17 June 2023, pages 20-26, June 2023. ACM. doi:10.1145/3589250.3596140 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{SchwarzEVSS23, author = {Michael Schwarz and Julian Erhard and Vesal Vojdani and Simmo Saan and Helmut Seidl}, title = {When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in {C}}, booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} International Workshop on the State Of the Art in Program Analysis, {SOAP} 2023, Orlando, FL, USA, 17 June 2023}, pages = {20--26}, year = {2023}, publisher = {{ACM}}, doi = {10.1145/3589250.3596140}, url = {https://doi.org/10.1145/3589250.3596140}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/pldi/0007EVSS23.bib}, dblp_id = {conf/pldi/0007EVSS23}, funding = {DFG-CONVEY}, month = {June}, timestamp = {Wed, 14 Jun 2023 15:33:02 +0200}, }
23. Katharina Kreuzer and Tobias Nipkow. Verification of NP-Hardness Reduction Functions for Exact Lattice Problems. In Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, LNCS, pages 365-381, July 2023. Springer. doi:10.1007/978-3-031-38499-8_21 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{KreuzerN23, author = {Katharina Kreuzer and Tobias Nipkow}, title = {Verification of NP-Hardness Reduction Functions for Exact Lattice Problems}, booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings}, volume = {14132}, pages = {365--381}, year = {2023}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-031-38499-8_21}, url = {https://doi.org/10.1007/978-3-031-38499-8\_21}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/cade/KreuzerN23.bib}, dblp_id = {conf/cade/KreuzerN23}, funding = {DFG-CONVEY}, month = {July}, timestamp = {Thu, 14 Sep 2023 20:25:50 +0200}, }
24. Eszter Couillard, Philipp Czerner, Javier Esparza, and Rupak Majumdar. Making Practical: Efficient Interactive Protocols for BDD Algorithms. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, LNCS, pages 437-458, July 2023. Springer. doi:10.1007/978-3-031-37709-9_21 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{CouillardCEM23, author = {Eszter Couillard and Philipp Czerner and Javier Esparza and Rupak Majumdar}, title = {Making $\textsf{IP}=\textsf{PSPACE}$ Practical: Efficient Interactive Protocols for {BDD} Algorithms}, booktitle = {Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {III}}, volume = {13966}, pages = {437--458}, year = {2023}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-031-37709-9_21}, url = {https://doi.org/10.1007/978-3-031-37709-9\_21}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/cav/CouillardCEM23.bib}, dblp_id = {conf/cav/CouillardCEM23}, funding = {DFG-CONVEY}, month = {July}, timestamp = {Tue, 12 Sep 2023 07:57:21 +0200}, }
25. Marvin Brieger, Stefan Mitsch, and André Platzer. Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs. In Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, LNCS, pages 96-115, July 2023. Springer. doi:10.1007/978-3-031-38499-8_6 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{BriegerMP23, author = {Marvin Brieger and Stefan Mitsch and Andr{\'{e}} Platzer}, title = {Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs}, booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings}, volume = {14132}, pages = {96--115}, year = {2023}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-031-38499-8_6}, url = {https://doi.org/10.1007/978-3-031-38499-8\_6}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/cade/BriegerMP23.bib}, dblp_id = {conf/cade/BriegerMP23}, funding = {DFG-CONVEY}, month = {July}, timestamp = {Sun, 24 Sep 2023 15:46:42 +0200}, }
26. Kiesbye, Jonis, Grover, Kush, and Křetínský, Jan. Model Checking for Proving and Improving Fault Tolerance of Satellites. In 2023 IEEE Aerospace Conference, pages 1-9, 2023. doi:10.1109/AERO55745.2023.10115801 Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @inproceedings{KiesbyeGK23, author = {Kiesbye, Jonis and Grover, Kush and Křetínský, Jan}, title = {Model Checking for Proving and Improving Fault Tolerance of Satellites}, booktitle = {2023 IEEE Aerospace Conference}, volume = {}, number = {}, pages = {1-9}, year = {2023}, doi = {10.1109/AERO55745.2023.10115801}, dblp_id = {none}, funding = {DFG-CONVEY}, }
27. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification. In Proc. ASE, pages 2050-2053, 2023. IEEE. doi:10.1109/ASE56229.2023.00213 Funding: DFG-CONVEY Publisher's Version PDF Presentation Video Supplement
    Artifact(s)

    1. doi:10.5281/zenodo.8245821
    Abstract

    Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the k-induction implementation in CPAchecker, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on SV-Benchmarks, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain k-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain k-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized k-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use CoVeriTeam, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20%.
    Demonstration video: https://youtu.be/l7UG-vhTL_4
    BibTeX Entry

    @inproceedings{ASE23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{CPA-DF}: {A} Tool for Configurable Interval Analysis to Boost Program Verification}, booktitle = {Proc.\ ASE}, pages = {2050-2053}, year = {2023}, series = {}, publisher = {IEEE}, doi = {10.1109/ASE56229.2023.00213}, url = {https://www.sosy-lab.org/research/cpa-df/}, pdf = {https://www.sosy-lab.org/research/pub/2023-ASE.CPA-DF_A_Tool_for_Configurable_Interval_Analysis_to_Boost_Program_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2023-09-13_ASE_CPA-DF_Po-Chun.pdf}, abstract = {Software verification is challenging, and auxiliary program invariants are used to improve the effectiveness of verification approaches. For instance, the <i>k</i>-induction implementation in <a href="https://cpachecker.sosy-lab.org/">CPAchecker</a>, an award-winning framework for program analysis, uses invariants produced by a configurable data-flow analysis to strengthen induction hypotheses. This invariant generator, CPA-DF, uses arithmetic expressions over intervals as its abstract domain and is able to prove some safe verification tasks alone. After extensively evaluating CPA-DF on <a href="https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks">SV-Benchmarks</a>, the largest publicly available suite of C safety-verification tasks, we discover that its potential as a stand-alone analysis or a sub-analysis in a parallel portfolio for combined verification approaches has been significantly underestimated: (1) As a stand-alone analysis, CPA-DF finds almost as many proofs as the plain <i>k</i>-induction implementation without auxiliary invariants. (2) As a sub-analysis running in parallel to the plain <i>k</i>-induction implementation, CPA-DF boosts the portfolio verifier to solve a comparable amount of tasks as the heavily-optimized <i>k</i>-induction implementation with invariant injection. Our detailed analysis reveals that dynamic precision adjustment is crucial to the efficiency and effectiveness of CPA-DF. To generalize our results beyond CPAchecker, we use <a href="https://gitlab.com/sosy-lab/software/coveriteam">CoVeriTeam</a>, a platform for cooperative verification, to compose three portfolio verifiers that execute CPA-DF and three other software verifiers in parallel, respectively. Surprisingly, running CPA-DF merely in parallel to these state-of-the-art tools further boosts the number of correct results up to more than 20&percnt;. <br> Demonstration video: <a href="https://youtu.be/l7UG-vhTL_4">https://youtu.be/l7UG-vhTL_4</a>}, artifact = {10.5281/zenodo.8245821}, funding = {DFG-CONVEY}, video = {https://youtu.be/l7UG-vhTL_4}, }
28. 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 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.}, artifact = {10.5281/zenodo.8289101}, funding = {DFG-CONVEY}, video = {https://youtu.be/mZhoGAa08Rk}, }
29. 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 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).}, artifact = {10.5281/zenodo.8287183}, funding = {DFG-CONVEY}, video = {https://youtu.be/ASZ6hoq8asE}, }
30. 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 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.}, _sha256 = {604dd391b6a49e46e97b6faafbb3cc331ccf5c04e3d364cf1e76a2c99c1c267f}, artifact = {10.5281/zenodo.7276532}, funding = {DFG-CONVEY,DFG-COOP}, }
31. Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee. Bridging Hardware and Software Analysis with Btor2C: A Word-Level-Circuit-to-C Translator. In Proc. TACAS, LNCS 13994, pages 152-172, 2023. Springer. doi:10.1007/978-3-031-30820-8_12 Funding: DFG-CONVEY Publisher's Version PDF Presentation Supplement
    Artifact(s)

    1. doi:10.5281/zenodo.7551707
    Abstract

    Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose the Btor2 language as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.
    BibTeX Entry

    @inproceedings{TACAS23a, author = {Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {Bridging Hardware and Software Analysis with {Btor2C}: {A} Word-Level-Circuit-to-{C} Translator}, booktitle = {Proc.\ TACAS}, pages = {152-172}, year = {2023}, series = {LNCS~13994}, publisher = {Springer}, doi = {10.1007/978-3-031-30820-8_12}, url = {https://www.sosy-lab.org/research/btor2c/}, presentation = {https://www.sosy-lab.org/research/prs/2023-04-26_TACAS23_Bridging_Hardware_and_Software_Analysis_with_Btor2C_Po-Chun.pdf}, abstract = {Across the broad field for the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to similar problems originating from other computational systems. A prominent example of such situation is the studies on formal verification and testing for hardware and software systems. The two research communities share common theoretical foundations and solving methods, including satisfiability, interpolation, and abstraction refinement. Nevertheless, it is often demanding for one community to benefit from the advancements of the other, as analyzers typically assume a particular input format. To bridge the gap between the hardware and software analysis, we propose Btor2C, a converter from word-level sequential circuits to C programs. We choose <a href="https://doi.org/10.1007/978-3-319-96145-3_32">the Btor2 language</a> as the input format for its simplicity and bit-precise semantics. It can be deemed as an intermediate representation tailored for analysis. Given a Btor2 circuit, Btor2C generates a behaviorally equivalent program in the C language, supported by most static program analyzers. We demonstrate the use cases of Btor2C by translating the benchmark set from the Hardware Model Checking Competitions into C programs and analyze them by tools from the Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware verifiers for enhanced quality assurance.}, _pdf = {https://www.sosy-lab.org/research/pub/2023-TACAS.Bridging_Hardware_and_Software_Analysis_with_Btor2C_A_Word-Level-Circuit-to-C_Translator.pdf}, artifact = {10.5281/zenodo.7551707}, funding = {DFG-CONVEY}, }
32. Katharina Kreuzer. Verification of Correctness and Security Properties for CRYSTALS-KYBER. IACR Cryptol. ePrint Arch., Cryptology ePrint Archive, Paper 2023/087, January 2023. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @misc{Kreuzer23a, author = {Katharina Kreuzer}, title = {Verification of Correctness and Security Properties for CRYSTALS-KYBER}, journal = {{IACR} Cryptol. ePrint Arch.}, year = {2023}, url = {https://eprint.iacr.org/2023/087}, dblp_id = {journals/iacr/Kreuzer23a}, funding = {DFG-CONVEY}, howpublished = {Cryptology ePrint Archive, Paper 2023/087}, month = {January}, type = {preprint}, }
33. Krasowski, Hanna, Thumm, Jakob, Müller, Marlon, Schäfer, Lukas, Wang, Xiao, and Althoff, Matthias. Provably Safe Reinforcement Learning: A Theoretical and Experimental Comparison. CoRR, abs/2205.06750, May 2023. Funding: DFG-CONVEY
    BibTeX Entry

    @misc{KrasowskiTMSWA23, author = {Krasowski, Hanna and Thumm, Jakob and Müller, Marlon and Schäfer, Lukas and Wang, Xiao and Althoff, Matthias}, title = {Provably Safe Reinforcement Learning: {A} Theoretical and Experimental Comparison}, journal = {CoRR}, volume = {abs/2205.06750}, year = {2023}, archiveprefix = {arXiv}, dblp_id = {journals/corr/abs-2205-06750}, eprint = {2205.06750}, funding = {DFG-CONVEY}, month = {May}, preprint = {https://arxiv.org/abs/2205.06750}, primaryclass = {cs.LG}, type = {preprint}, }
34. Katharina Kreuzer. Verification of the (1–)-Correctness Proof of CRYSTALS-KYBER with Number Theoretic Transform. Cryptology ePrint Archive, Paper 2023/027, 2023. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @misc{KreuzerePrintArXive, author = {Katharina Kreuzer}, title = {Verification of the (1–$\delta$)-{C}orrectness {P}roof of {CRYSTALS-KYBER} with {N}umber {T}heoretic {T}ransform}, year = {2023}, url = {https://eprint.iacr.org/2023/027}, dblp_id = {none}, funding = {DFG-CONVEY}, howpublished = {Cryptology ePrint Archive, Paper 2023/027}, type = {preprint}, }

2022

35. Julian Erhard, Simmo Saan, Sarah Tilscher, Michael Schwarz, Karoliine Holter, Vesal Vojdani, and Helmut Seidl. Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap. CoRR, abs/2209.10445, sept 2022. doi:10.48550/arXiv.2209.10445 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @article{ErhardSTSHVS22, author = {Julian Erhard and Simmo Saan and Sarah Tilscher and Michael Schwarz and Karoliine Holter and Vesal Vojdani and Helmut Seidl}, title = {Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap}, journal = {CoRR}, volume = {abs/2209.10445}, year = {2022}, doi = {10.48550/arXiv.2209.10445}, url = {https://doi.org/10.48550/arXiv.2209.10445}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/corr/abs-2209-10445.bib}, dblp_id = {journals/corr/abs-2209-10445}, eprint = {2209.10445}, eprinttype = {arXiv}, funding = {DFG-CONVEY}, month = {sept}, timestamp = {Wed, 28 Sep 2022 15:17:28 +0200}, type = {preprint}, }
36. Roßkopf, Simon and Nipkow, Tobias. A Formalization and Proof Checker for Isabelle's Metalogic. J. Autom. Reason., 67, 12. Dec 2022. doi:10.1007/s10817-022-09648-w Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @article{RosskopfN23, author = {Ro{\ss}kopf, Simon and Nipkow, Tobias}, title = {A Formalization and Proof Checker for Isabelle's Metalogic}, journal = {J. Autom. Reason.}, volume = {67}, year = {2022}, doi = {10.1007/s10817-022-09648-w}, url = {https://doi.org/10.1007/s10817-022-09648-w}, day = {12}, dblp_id = {journals/jar/RosskopfN23}, funding = {DFG-CONVEY}, issn = {1573-0670}, month = {Dec}, }
37. Jahanshahi, Niloofar, Lavaei, Abolfazl, and Zamani, Majid. Compositional Construction of Safety Controllers for Networks of Continuous-Space POMDPs. IEEE Transactions on Control of Network Systems:1-12, June 2022. doi:10.1109/TCNS.2022.3186649 Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @article{DBLPjournalscorrabs210305906, author = {Jahanshahi, Niloofar and Lavaei, Abolfazl and Zamani, Majid}, title = {Compositional Construction of Safety Controllers for Networks of Continuous-Space POMDPs}, journal = {IEEE Transactions on Control of Network Systems}, volume = {}, number = {}, pages = {1-12}, year = {2022}, doi = {10.1109/TCNS.2022.3186649}, dblp_id = {none}, funding = {DFG-CONVEY}, month = {June}, preprint = {https://arxiv.org/abs/2103.05906}, }
38. Anand, Mahathi, Lavaei, Abolfazl, and Zamani, Majid. From Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems. IEEE Transactions on Automatic Control:1-8, June 2022. doi:10.1109/TAC.2022.3183032 Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @article{9796643, author = {Anand, Mahathi and Lavaei, Abolfazl and Zamani, Majid}, title = {From Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems}, journal = {IEEE Transactions on Automatic Control}, volume = {}, number = {}, pages = {1-8}, year = {2022}, doi = {10.1109/TAC.2022.3183032}, dblp_id = {none}, funding = {DFG-CONVEY}, month = {June}, preprint = {https://arxiv.org/abs/2101.06916}, }
39. Sabanayagam, Mahalakshmi, Esser, Pascal, and Ghoshdastidar, Debarghya. Analysis of Graph Convolutional Networks using Neural Tangent Kernels. International Workshop on Mining and Learning with Graphs, June 2022. Funding: DFG-CONVEY
    BibTeX Entry

    @article{SabanayagamEG22a, author = {Sabanayagam, Mahalakshmi and Esser, Pascal and Ghoshdastidar, Debarghya}, title = {Analysis of Graph Convolutional Networks using Neural Tangent Kernels}, journal = {International Workshop on Mining and Learning with Graphs}, year = {2022}, dblp_id = {none}, funding = {DFG-CONVEY}, month = {June}, }
40. Thomas Ammer and Katharina Kreuzer. Number Theoretic Transform. Archive of Formal Proofs, August 2022. Funding: DFG-CONVEY
    BibTeX Entry

    @article{NumberTheoreticTransformAFP, author = {Thomas Ammer and Katharina Kreuzer}, title = {Number {T}heoretic {T}ransform}, journal = {Archive of Formal Proofs}, year = {2022}, dblp_id = {none}, funding = {DFG-CONVEY}, issn = {2150-914x}, month = {August}, }
41. Ujkan Sulejmani, Manuel Eberl, and Katharina Kreuzer. The Hales–Jewett Theorem. Archive of Formal Proofs, September 2022. Funding: DFG-CONVEY
    BibTeX Entry

    @article{HalesJewettAFP, author = {Ujkan Sulejmani and Manuel Eberl and Katharina Kreuzer}, title = {The {H}ales–{J}ewett {T}heorem}, journal = {Archive of Formal Proofs}, year = {2022}, dblp_id = {none}, funding = {DFG-CONVEY}, issn = {2150-914x}, month = {September}, }
42. Katharina Kreuzer. CRYSTALS-Kyber. Archive of Formal Proofs, September 2022. Funding: DFG-CONVEY
    BibTeX Entry

    @article{CRYSTALSKyberAFP, author = {Katharina Kreuzer}, title = {{CRYSTALS}-{K}yber}, journal = {Archive of Formal Proofs}, year = {2022}, dblp_id = {none}, funding = {DFG-CONVEY}, issn = {2150-914x}, month = {September}, }
43. Sabanayagam, Mahalakshmi, Esser, Pascal, and Ghoshdastidar, Debarghya. Representation Power of Graph Convolutions : Neural Tangent Kernel Analysis. CoRR, abs/2210-09809, October 2022. doi:10.48550/ARXIV.2210.09809 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @article{SabanayagamEG22, author = {Sabanayagam, Mahalakshmi and Esser, Pascal and Ghoshdastidar, Debarghya}, title = {Representation Power of Graph Convolutions : Neural Tangent Kernel Analysis}, journal = {CoRR}, volume = {abs/2210-09809}, year = {2022}, doi = {10.48550/ARXIV.2210.09809}, pdf = {https://www.cs.cit.tum.de/fileadmin/w00cfj/tfai/preprints/sabanayagam2022.pdf}, dblp_id = {journals/corr/abs-2210-09809}, funding = {DFG-CONVEY}, month = {October}, type = {preprint}, }
44. Esser, Pascal Mattia, Mukherjee, Satyaki, Sabanayagam, Mahalakshmi, and Ghoshdastidar, Debarghya. Improved Representation Learning Through Tensorized Autoencoders. CoRR, December 2022. doi:10.48550/ARXIV.2212.01046 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @article{EsserMSG22, author = {Esser, Pascal Mattia and Mukherjee, Satyaki and Sabanayagam, Mahalakshmi and Ghoshdastidar, Debarghya}, title = {Improved Representation Learning Through Tensorized Autoencoders}, journal = {CoRR}, year = {2022}, doi = {10.48550/ARXIV.2212.01046}, dblp_id = {journals/corr/abs-2212-01046}, funding = {DFG-CONVEY}, month = {December}, type = {preprint}, }
45. Maximilian Schäffeler and Mohammad Abdulaziz. Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes. CoRR, abs/2206.02169, 2022. doi:10.48550/arXiv.2206.02169 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @article{SchaffelerA22, author = {Maximilian Sch\"affeler and Mohammad Abdulaziz}, title = {Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes}, journal = {CoRR}, volume = {abs/2206.02169}, year = {2022}, doi = {10.48550/arXiv.2206.02169}, url = {https://doi.org/10.48550/arXiv.2206.02169}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/corr/abs-2206-02169.bib}, dblp_id = {journals/corr/abs-2206-02169}, eprint = {2206.02169}, eprinttype = {arXiv}, funding = {DFG-CONVEY}, no_month = {true}, timestamp = {Mon, 13 Jun 2022 15:31:50 +0200}, type = {preprint}, }
46. Mark Wetzlinger, Adrian Kulmburg, Alexis Le Penven, and Matthias Althoff. Adaptive reachability algorithms for nonlinear systems using abstraction error analysis. Nonlinear Analysis: Hybrid Systems, 46:101252, 2022. doi:10.1016/j.nahs.2022.101252 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @article{WetzlingerKLA22, author = {Mark Wetzlinger and Adrian Kulmburg and Alexis {Le Penven} and Matthias Althoff}, title = {Adaptive reachability algorithms for nonlinear systems using abstraction error analysis}, journal = {Nonlinear Analysis: Hybrid Systems}, volume = {46}, pages = {101252}, year = {2022}, doi = {10.1016/j.nahs.2022.101252}, url = {https://www.sciencedirect.com/science/article/pii/S1751570X22000607}, dblp_id = {none}, funding = {DFG-CONVEY}, issn = {1751-570X}, keywords = {Convergence order, Gain order, Parameter tuning, Zonotope order reduction, Hausdorff distance, reachability analysis, Nonlinear systems, Differential-algebraic equations}, }
47. Matthias Kettl and Thomas Lemberger. The Static Analyzer Infer in SV-COMP (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, LNCS, pages 451-456, March 2022. Springer. doi:10.1007/978-3-030-99527-0_30 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{KettlL22, author = {Matthias Kettl and Thomas Lemberger}, title = {The Static Analyzer Infer in {SV-COMP} (Competition Contribution)}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, {TACAS} 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {II}}, volume = {13244}, pages = {451--456}, year = {2022}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_30}, url = {https://doi.org/10.1007/978-3-030-99527-0\_30}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/tacas/KettlL22.bib}, dblp_id = {conf/tacas/KettlL22}, funding = {DFG-CONVEY}, month = {March}, timestamp = {Fri, 29 Apr 2022 14:50:33 +0200}, }
48. Mahalakshmi Sabanayagam, Leena Chennuru Vankadara, and Debarghya Ghoshdastidar. Graphon based Clustering and Testing of Networks: Algorithms and Theory. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022, April 2022. OpenReview.net. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @inproceedings{SabanayagamVG22, author = {Mahalakshmi Sabanayagam and Leena Chennuru Vankadara and Debarghya Ghoshdastidar}, title = {Graphon based Clustering and Testing of Networks: Algorithms and Theory}, booktitle = {The Tenth International Conference on Learning Representations, {ICLR} 2022, Virtual Event, April 25-29, 2022}, year = {2022}, publisher = {OpenReview.net}, url = {https://openreview.net/forum?id=sTNHCrIKDQc}, dblp_id = {conf/iclr/SabanayagamVG22}, funding = {DFG-CONVEY}, month = {April}, }
49. Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza. Fast and Succinct Population Protocols for Presburger Arithmetic. In 1st Symposium on Algorithmic Foundations of Dynamic Networks, SAND 2022, March 28-30, 2022, Virtual Conference, LIPIcs, pages 11:1-11:17, April 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.SAND.2022.11 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{CzernerGHE22, author = {Philipp Czerner and Roland Guttenberg and Martin Helfrich and Javier Esparza}, title = {Fast and Succinct Population Protocols for Presburger Arithmetic}, booktitle = {1st Symposium on Algorithmic Foundations of Dynamic Networks, {SAND} 2022, March 28-30, 2022, Virtual Conference}, volume = {221}, pages = {11:1--11:17}, year = {2022}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, doi = {10.4230/LIPIcs.SAND.2022.11}, url = {https://doi.org/10.4230/LIPIcs.SAND.2022.11}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/sand/CzernerGHE22.bib}, dblp_id = {conf/sand/CzernerGHE22}, funding = {DFG-CONVEY}, month = {April}, timestamp = {Fri, 29 Apr 2022 14:20:08 +0200}, }
50. Jonis Kiesbye, Kush Grover, Pranav Ashok, and Jan Kretínský. Planning via model checking with decision-tree controllers. In 2022 International Conference on Robotics and Automation, ICRA 2022, Philadelphia, PA, USA, May 23-27, 2022, pages 4347-4354, May 2022. IEEE. doi:10.1109/ICRA46639.2022.9811980 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{KiesbyeGAK22, author = {Jonis Kiesbye and Kush Grover and Pranav Ashok and Jan Kret{\'{\i}}nsk{\'{y}}}, title = {Planning via model checking with decision-tree controllers}, booktitle = {2022 International Conference on Robotics and Automation, {ICRA} 2022, Philadelphia, PA, USA, May 23-27, 2022}, pages = {4347--4354}, year = {2022}, publisher = {{IEEE}}, doi = {10.1109/ICRA46639.2022.9811980}, url = {https://doi.org/10.1109/ICRA46639.2022.9811980}, dblp_id = {conf/icra/KiesbyeGAK22}, funding = {DFG-CONVEY}, month = {May}, }
51. Anand, Mahathi, Murali, Vishnu, Trivedi, Ashutosh, and Zamani, Majid. K-Inductive Barrier Certificates for Stochastic Systems. In HSCC '22: 25th ACM International Conference on Hybrid Systems: Computation and Control, Milan, Italy, May 4 - 6, 2022, HSCC '22, May 2022. Association for Computing Machinery. doi:10.1145/3501710.3519532 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{AnandM0Z22, author = {Anand, Mahathi and Murali, Vishnu and Trivedi, Ashutosh and Zamani, Majid}, title = {K-Inductive Barrier Certificates for Stochastic Systems}, booktitle = {{HSCC} '22: 25th {ACM} International Conference on Hybrid Systems: Computation and Control, Milan, Italy, May 4 - 6, 2022}, year = {2022}, series = {HSCC '22}, publisher = {Association for Computing Machinery}, doi = {10.1145/3501710.3519532}, url = {https://doi.org/10.1145/3501710.3519532}, address = {New York, NY, USA}, articleno = {12}, dblp_id = {conf/hybrid/AnandM0Z22}, funding = {DFG-CONVEY}, keywords = {Stochastic dynamical systems, Barrier certificates, Safety specification, Reachability specification, k-Induction}, location = {Milan, Italy}, month = {May}, numpages = {11}, }
52. Kush Grover, Jan Kretínský, Tobias Meggendorfer, and Maximilian Weininger. Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. In 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, pages 11:1-11:20, September 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2022.11 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{GroverKMW22, author = {Kush Grover and Jan Kret{\'{\i}}nsk{\'{y}} and Tobias Meggendorfer and Maximilian Weininger}, title = {Anytime Guarantees for Reachability in Uncountable Markov Decision Processes}, booktitle = {33rd International Conference on Concurrency Theory, {CONCUR} 2022, September 12-16, 2022, Warsaw, Poland}, pages = {11:1--11:20}, year = {2022}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, doi = {10.4230/LIPIcs.CONCUR.2022.11}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2022/17074/pdf/LIPIcs-CONCUR-2022-11.pdf}, dblp_id = {conf/concur/GroverKMW22}, funding = {DFG-CONVEY}, month = {September}, }
53. Martin Helfrich, Milan Ceska, Jan Kretínský, and Stefan Marticek. Abstraction-Based Segmental Simulation of Chemical Reaction Networks. In Computational Methods in Systems Biology - 20th International Conference, CMSB 2022, Bucharest, Romania, September 14-16, 2022, Proceedings, LNCS, pages 41-60, September 2022. Springer. doi:10.1007/978-3-031-15034-0_3 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{HelfrichCKM22, author = {Martin Helfrich and Milan Ceska and Jan Kret{\'{\i}}nsk{\'{y}} and Stefan Marticek}, title = {Abstraction-Based Segmental Simulation of Chemical Reaction Networks}, booktitle = {Computational Methods in Systems Biology - 20th International Conference, {CMSB} 2022, Bucharest, Romania, September 14-16, 2022, Proceedings}, volume = {13447}, pages = {41--60}, year = {2022}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-031-15034-0_3}, url = {https://doi.org/10.1007/978-3-031-15034-0\_3}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/cmsb/HelfrichCKM22.bib}, dblp_id = {conf/cmsb/HelfrichCKM22}, funding = {DFG-CONVEY}, month = {September}, timestamp = {Sat, 10 Sep 2022 20:58:38 +0200}, }
54. Hanna Krasowski and Matthias Althoff. CommonOcean: Composable Benchmarks for Motion Planning on Oceans. In 25th IEEE International Conference on Intelligent Transportation Systems, ITSC 2022, Macau, China, October 8-12, 2022, pages 1676-1682, October 2022. doi:10.1109/ITSC55140.2022.9921925 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{KrasowskiA22, author = {Hanna Krasowski and Matthias Althoff}, title = {CommonOcean: Composable Benchmarks for Motion Planning on Oceans}, booktitle = {25th {IEEE} International Conference on Intelligent Transportation Systems, {ITSC} 2022, Macau, China, October 8-12, 2022}, pages = {1676-1682}, year = {2022}, doi = {10.1109/ITSC55140.2022.9921925}, pdf = {https://mediatum.ub.tum.de/doc/1687691/ltbbjgwihiht96fqfeblxdyj7.ITSC22_CommonOcean.pdf}, code = {https://commonocean.cps.cit.tum.de/}, dblp_id = {conf/itsc/KrasowskiA22}, funding = {DFG-CONVEY}, month = {October}, }
55. Hanna Krasowski, Yinqiang Zhang, and Matthias Althoff. Safe Reinforcement Learning for Urban Driving using Invariably Safe Braking Sets. In 25th IEEE International Conference on Intelligent Transportation Systems, ITSC 2022, Macau, China, October 8-12, 2022, pages 2407-2414, October 2022. doi:10.1109/ITSC55140.2022.9922166 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{KrasowskiZA22, author = {Hanna Krasowski and Yinqiang Zhang and Matthias Althoff}, title = {Safe Reinforcement Learning for Urban Driving using Invariably Safe Braking Sets}, booktitle = {25th {IEEE} International Conference on Intelligent Transportation Systems, {ITSC} 2022, Macau, China, October 8-12, 2022}, pages = {2407-2414}, year = {2022}, doi = {10.1109/ITSC55140.2022.9922166}, pdf = {https://mediatum.ub.tum.de/doc/1687692/q8nz0sgpht6oh7j66y4jpyhnv.ITSC22_Safe_RL_Urban.pdf}, dblp_id = {conf/itsc/KrasowskiZA22}, funding = {DFG-CONVEY}, month = {October}, }
56. Dirk Beyer, Martin Spiessl, and Sven Umbricht. Cooperation between Automatic and Interactive Software Verifiers. In 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 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}, pages = {111–128}, year = {2022}, series = {LNCS~13550}, publisher = {Springer}, doi = {10.1007/978-3-031-17108-6_7}, sha256 = {a310ff0ac97f37ee817c6f05a4cc9a635cbacd09ad301b483095f133040e8e48}, url = {}, abstract = {}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.Cooperation_between_Automatic_and_Interactive_Software_Verifiers.pdf}, funding = {DFG-CONVEY}, }
57. Dirk Beyer, Marian Lingsch Rosenfeld, and Martin Spiessl. A Unifying Approach for Control-Flow-Based Loop Abstraction. In 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 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}, pages = {3-19}, year = {2022}, series = {LNCS~13550}, publisher = {Springer}, doi = {10.1007/978-3-031-17108-6_1}, sha256 = {047a8a9062e143741623320cf80ec963ce5f7200a5a75d263fa6615c12f2199e}, url = {}, abstract = {}, _pdf = {https://www.sosy-lab.org/research/pub/2022-SEFM.A_Unifying_Approach_for_Control-Flow-Based_Loop_Abstraction.pdf}, funding = {DFG-CONVEY}, }
58. Dirk Beyer and Martin Spiessl. The Static Analyzer Frama-C in SV-COMP (Competition Contribution). In 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 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}, pages = {429--434}, year = {2022}, series = {LNCS~13244}, publisher = {Springer}, doi = {10.1007/978-3-030-99527-0_26}, sha256 = {77ed425c2b30a4f9424ed46c9cb5a846f5c21677ececdbf098e30f37aca67a3d}, url = {}, abstract = {}, _pdf = {https://www.sosy-lab.org/research/pub/2022-TACAS.The_Static_Analyzer_Frama-C_in_SV-COMP_Competition_Contribution.pdf}, funding = {DFG-CONVEY}, }
59. Mark Wetzlinger, Niklas Kochdumper, Stanley Bak, and Matthias Althoff. Fully Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets. CoRR, abs/2209-09321, September 2022. Funding: DFG-CONVEY
    BibTeX Entry

    @misc{WetzlingerKBA22, author = {Mark Wetzlinger and Niklas Kochdumper and Stanley Bak and Matthias Althoff}, title = {Fully Automated Verification of Linear Systems Using Inner- and Outer-Approximations of Reachable Sets}, journal = {CoRR}, volume = {abs/2209-09321}, year = {2022}, archiveprefix = {arXiv}, dblp_id = {journals/corr/abs-2209-09321}, eprint = {2209.09321}, funding = {DFG-CONVEY}, month = {September}, preprint = {http://arxiv.org/abs/2209.09321}, primaryclass = {math.NA}, type = {preprint}, }
60. Krasowski, Hanna, Akella, Prithvi, Ames, Aaron D., and Althoff, Matthias. Probabilistic Guarantees for Safe Reinforcement Learning in Continuous Action Spaces via Temporal Logic. CoRR, abs/2212.06129, December 2022. Funding: DFG-CONVEY
    BibTeX Entry

    @misc{KrasowskiAAA22, author = {Krasowski, Hanna and Akella, Prithvi and Ames, Aaron D. and Althoff, Matthias}, title = {Probabilistic Guarantees for Safe Reinforcement Learning in Continuous Action Spaces via Temporal Logic}, journal = {CoRR}, volume = {abs/2212.06129}, year = {2022}, archiveprefix = {arXiv}, dblp_id = {journals/corr/abs-2212-06129}, eprint = {2212.06129}, funding = {DFG-CONVEY}, month = {December}, preprint = {https://arxiv.org/abs/2212.06129}, type = {preprint}, }

2021

61. Tobias Nipkow and Simon Roßkopf. Isabelle's Metalogic: Formalization and Proof Checker. Arch. Formal Proofs, April 2021. Funding: DFG-CONVEY
    BibTeX Entry

    @article{NipkowR21, author = {Tobias Nipkow and Simon Roßkopf}, title = {Isabelle's Metalogic: Formalization and Proof Checker}, journal = {Arch. Formal Proofs}, year = {2021}, dblp_id = {journals/afp/NipkowR21}, funding = {DFG-CONVEY}, issn = {2150-914x}, month = {April}, }
62. Niloofar Jahanshahi, Pushpak Jagtap, and Majid Zamani. Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier Functions. IEEE Control. Syst. Lett., 5(1):253-258, June 2021. doi:10.1109/LCSYS.2020.3001562 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @article{JahanshahiJZ21, author = {Niloofar Jahanshahi and Pushpak Jagtap and Majid Zamani}, title = {Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier Functions}, journal = {{IEEE} Control. Syst. Lett.}, volume = {5}, number = {1}, pages = {253--258}, year = {2021}, doi = {10.1109/LCSYS.2020.3001562}, url = {https://www.researchgate.net/profile/Pushpak-Jagtap/publication/342112784_Synthesis_of_Partially_Observed_Jump-Diffusion_Systems_via_Control_Barrier_Functions/links/5efe440f92851c52d61361f7/Synthesis-of-Partially-Observed-Jump-Diffusion-Systems-via-Control-Barrier-Functions.pdf}, dblp_id = {journals/csysl/JahanshahiJZ21}, funding = {DFG-CONVEY}, month = {June}, }
63. Katharina Kreuzer and Manuel Eberl. Van der Waerden's Theorem. Archive of Formal Proofs, June 2021. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @article{VanderWaerdenAFP, author = {Katharina Kreuzer and Manuel Eberl}, title = {Van der {W}aerden's {T}heorem}, journal = {Archive of Formal Proofs}, year = {2021}, url = {https://isa-afp.org/entries/Van_der_Waerden.html}, dblp_id = {none}, funding = {DFG-CONVEY}, issn = {2150-914x}, month = {June}, }
64. Helmut Seidl and Ralf Vogler. Three improvements to the top-down solver. Math. Struct. Comput. Sci., 31(9):1090-1134, August 2021. doi:10.1017/S0960129521000499 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @article{SeidlV21, author = {Helmut Seidl and Ralf Vogler}, title = {Three improvements to the top-down solver}, journal = {Math. Struct. Comput. Sci.}, volume = {31}, number = {9}, pages = {1090--1134}, year = {2021}, doi = {10.1017/S0960129521000499}, url = {https://doi.org/10.1017/S0960129521000499}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/mscs/SeidlV21.bib}, dblp_id = {journals/mscs/SeidlV21}, funding = {DFG-CONVEY}, month = {August}, timestamp = {Mon, 08 Aug 2022 21:23:41 +0200}, }
65. Maximilian Schäffeler and Mohammad Abdulaziz. Verified Algorithms for Solving Markov Decision Processes. Archive of Formal Proofs, 2021, 2021. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @article{SchaffelerA21, author = {Maximilian Sch\"affeler and Mohammad Abdulaziz}, title = {Verified Algorithms for Solving Markov Decision Processes}, journal = {Archive of Formal Proofs}, volume = {2021}, year = {2021}, url = {https://www.isa-afp.org/entries/MDP-Algorithms.html}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/afp/SchaffelerA21.bib}, dblp_id = {none}, funding = {DFG-CONVEY}, timestamp = {Fri, 21 Jan 2022 16:48:15 +0100}, }
66. Maximilian Schäffeler and Mohammad Abdulaziz. Markov Decision Processes with Rewards. Archive of Formal Proofs, 2021, 2021. Funding: DFG-CONVEY Supplement
    BibTeX Entry

    @article{SchaffelerA21a, author = {Maximilian Sch\"affeler and Mohammad Abdulaziz}, title = {Markov Decision Processes with Rewards}, journal = {Archive of Formal Proofs}, volume = {2021}, year = {2021}, url = {https://www.isa-afp.org/entries/MDP-Rewards.html}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/journals/afp/SchaffelerA21a.bib}, dblp_id = {none}, funding = {DFG-CONVEY}, timestamp = {Fri, 21 Jan 2022 16:48:15 +0100}, }
67. Philipp Czerner and Stefan Jaax. Running Time Analysis of Broadcast Consensus Protocols. In Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, LNCS, pages 164-183, March 2021. Springer. doi:10.1007/978-3-030-71995-1_9 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CzernerJ21, author = {Philipp Czerner and Stefan Jaax}, title = {Running Time Analysis of Broadcast Consensus Protocols}, booktitle = {Foundations of Software Science and Computation Structures - 24th International Conference, {FOSSACS} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings}, volume = {12650}, pages = {164--183}, year = {2021}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-71995-1_9}, pdf = {https://nicze.de/philipp/running.pdf}, dblp_id = {conf/fossacs/CzernerJ21}, funding = {DFG-CONVEY}, month = {March}, preprint = {https://arxiv.org/abs/2101.03780}, slides = {https://nicze.de/philipp/fossacs2021.pdf}, }
68. Simmo Saan, Michael Schwarz, Kalmer Apinis, Julian Erhard, Helmut Seidl, Ralf Vogler, and Vesal Vojdani. Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, LNCS, pages 438-442, March 2021. Springer. doi:10.1007/978-3-030-72013-1_28 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SaanSAESVV21, author = {Simmo Saan and Michael Schwarz and Kalmer Apinis and Julian Erhard and Helmut Seidl and Ralf Vogler and Vesal Vojdani}, title = {Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints - (Competition Contribution)}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, {TACAS} 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part {II}}, volume = {12652}, pages = {438--442}, year = {2021}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-72013-1_28}, dblp_id = {conf/tacas/SaanSAESVV21}, funding = {DFG-CONVEY}, month = {March}, }
69. M. Khaled and M. Zamani. OmegaThreads: Symbolic controller design for omega-regular objectives. In HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021, May 2021. doi:10.1145/3447928.3456652 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{KhaledZ21, author = {M. Khaled and M. Zamani}, title = {{OmegaThreads}: {Symbolic} controller design for omega-regular objectives}, booktitle = {{HSCC} '21: 24th {ACM} International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021}, year = {2021}, doi = {10.1145/3447928.3456652}, date-added = {2021-03-15 22:20:10 -0600}, date-modified = {2021-06-14 20:36:19 -0600}, dblp_id = {conf/hybrid/KhaledZ21}, funding = {DFG-CONVEY}, month = {May}, }
70. Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. Formal Verification of Hyperproperties for Control Systems. In CAADCPS '21: Proceedings of the Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems, Nashville, TN, USA, May 19-21, 2021, CAADCPS '21, pages 29-30, May 2021. ACM. doi:10.1145/3457335.3461715 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{AnandM0Z21, author = {Mahathi Anand and Vishnu Murali and Ashutosh Trivedi and Majid Zamani}, title = {Formal Verification of Hyperproperties for Control Systems}, booktitle = {{CAADCPS} '21: Proceedings of the Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems, Nashville, TN, USA, May 19-21, 2021}, pages = {29--30}, year = {2021}, series = {CAADCPS '21}, publisher = {ACM}, doi = {10.1145/3457335.3461715}, dblp_id = {conf/cpsweek/AnandM0Z21}, funding = {DFG-CONVEY}, keywords = {barrier certificates, cyber-physical systems, hyperproperties}, location = {Nashville, Tennessee}, month = {May}, numpages = {2}, }
71. Mark Wetzlinger, Adrian Kulmburg, and Matthias Althoff. Adaptive Parameter Tuning for Reachability Analysis of Nonlinear Systems. In HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021, pages 16:1-16:11, May 2021. ACM. doi:10.1145/3447928.3456643 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{WetzlingerKA21, author = {Mark Wetzlinger and Adrian Kulmburg and Matthias Althoff}, title = {Adaptive Parameter Tuning for Reachability Analysis of Nonlinear Systems}, booktitle = {{HSCC} '21: 24th {ACM} International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021}, pages = {16:1--16:11}, year = {2021}, publisher = {ACM}, doi = {10.1145/3447928.3456643}, url = {https://dl.acm.org/doi/10.1145/3447928.3456643}, pdf = {https://mediatum.ub.tum.de/doc/1615814/1615814.pdf}, articleno = {16}, code = {https://codeocean.com/capsule/1174390/tree/v1}, dblp_id = {conf/hybrid/WetzlingerKA21}, funding = {DFG-CONVEY}, keywords = {parameter tuning, nonlinear systems, reachability analysis}, month = {May}, numpages = {11}, }
72. Susanne Albers and Jens Quedenfeld. Algorithms for Right-Sizing Heterogeneous Data Centers. In SPAA '21: 33rd ACM Symposium on Parallelism in Algorithms and Architectures, Virtual Event, USA, 6-8 July, 2021, pages 48-58, July 2021. ACM. doi:10.1145/3409964.3461789 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{AlbersQ21, author = {Susanne Albers and Jens Quedenfeld}, title = {Algorithms for Right-Sizing Heterogeneous Data Centers}, booktitle = {{SPAA} '21: 33rd {ACM} Symposium on Parallelism in Algorithms and Architectures, Virtual Event, USA, 6-8 July, 2021}, pages = {48--58}, year = {2021}, publisher = {{ACM}}, doi = {10.1145/3409964.3461789}, url = {https://doi.org/10.1145/3409964.3461789}, dblp_id = {conf/spaa/AlbersQ21}, funding = {DFG-CONVEY}, month = {July}, }
73. Hanna Krasowski and Matthias Althoff. Temporal Logic Formalization of Marine Traffic Rules. In IEEE Intelligent Vehicles Symposium, IV 2021, Nagoya, Japan, July 11-17, 2021, pages 186-192, July 2021. IEEE. doi:10.1109/IV48863.2021.9575685 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{KrasowskiA21, author = {Hanna Krasowski and Matthias Althoff}, title = {Temporal Logic Formalization of Marine Traffic Rules}, booktitle = {{IEEE} Intelligent Vehicles Symposium, {IV} 2021, Nagoya, Japan, July 11-17, 2021}, pages = {186-192}, year = {2021}, publisher = {IEEE}, doi = {10.1109/IV48863.2021.9575685}, pdf = {http://mediatum.ub.tum.de/doc/1613345/1es8mip5k7waoasv97t18tlvc.IV_final_submission.pdf}, code = {https://doi.org/10.24433/CO.8258454.v2}, dblp_id = {conf/ivs/KrasowskiA21}, funding = {DFG-CONVEY}, month = {July}, }
74. Philipp Czerner and Javier Esparza. Lower Bounds on the State Complexity of Population Protocols. In PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021, pages 45-54, July 2021. ACM. doi:10.1145/3465084.3467912 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CzernerE21, author = {Philipp Czerner and Javier Esparza}, title = {Lower Bounds on the State Complexity of Population Protocols}, booktitle = {{PODC} '21: {ACM} Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021}, pages = {45--54}, year = {2021}, publisher = {{ACM}}, doi = {10.1145/3465084.3467912}, pdf = {https://nicze.de/philipp/logloglog.pdf}, dblp_id = {conf/podc/CzernerE21}, funding = {DFG-CONVEY}, month = {July}, }
75. Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza. Decision Power of Weak Asynchronous Models of Distributed Computing. In PODC '21: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021, pages 115-125, July 2021. ACM. doi:10.1145/3465084.3467918 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{CzernerGHE21, author = {Philipp Czerner and Roland Guttenberg and Martin Helfrich and Javier Esparza}, title = {Decision Power of Weak Asynchronous Models of Distributed Computing}, booktitle = {{PODC} '21: {ACM} Symposium on Principles of Distributed Computing, Virtual Event, Italy, July 26-30, 2021}, pages = {115--125}, year = {2021}, publisher = {{ACM}}, doi = {10.1145/3465084.3467918}, pdf = {https://nicze.de/philipp/decisionpower.pdf}, dblp_id = {conf/podc/CzernerGHE21}, funding = {DFG-CONVEY}, month = {July}, }
76. Grover, Kush, Barbosa, Fernando S, Tumova, Jana, and Kretínský, Jan. Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments. In Robotics: Science and Systems XVII, Virtual Event, July 12-16, 2021, July 2021. doi:10.15607/RSS.2021.XVII.090 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{GroverBTK21, author = {Grover, Kush and Barbosa, Fernando S and Tumova, Jana and Kret{\'{\i}}nsk{\'{y}}, Jan}, title = {Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments}, booktitle = {Robotics: Science and Systems XVII, Virtual Event, July 12-16, 2021}, year = {2021}, doi = {10.15607/RSS.2021.XVII.090}, url = {https://roboticsconference.org/2021/program/papers/090/index.html}, pdf = {http://www.roboticsproceedings.org/rss17/p090.pdf}, address = {Virtual}, dblp_id = {conf/rss/GroverBTK21}, funding = {DFG-CONVEY}, month = {July}, organization = {RSS Foundation-Robotics Science \& Systems Foundation}, }
77. Nipkow, Tobias and Roßkopf, Simon. Isabelle's Metalogic: Formalization and Proof Checker. Arch. Formal Proofs:93-110, July 2021. Springer International Publishing. Funding: DFG-CONVEY
    Abstract

    Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.
    BibTeX Entry

    @inproceedings{NipkowR21a, author = {Nipkow, Tobias and Ro{\ss}kopf, Simon}, title = {Isabelle's Metalogic: Formalization and Proof Checker}, journal = {Arch. Formal Proofs}, booktitle = {Automated Deduction -- CADE 28}, pages = {93--110}, year = {2021}, publisher = {Springer International Publishing}, abstract = {Isabelle is a generic theorem prover with a fragment of higher-order logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.}, address = {Cham}, dblp_id = {journals/afp/NipkowR21}, funding = {DFG-CONVEY}, month = {July}, }
78. Javier Esparza, Stefan Kiefer, Jan Kretínský, and Maximilian Weininger. Enforcing ømega-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, LIPIcs, pages 5:1-5:22, August 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2021.5 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{EsparzaKKW21, author = {Javier Esparza and Stefan Kiefer and Jan Kret{\'{\i}}nsk{\'{y}} and Maximilian Weininger}, title = {Enforcing {\(\omega\)}-Regular Properties in Markov Chains by Restarting}, booktitle = {32nd International Conference on Concurrency Theory, {CONCUR} 2021, August 24-27, 2021, Virtual Conference}, volume = {203}, pages = {5:1--5:22}, year = {2021}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, doi = {10.4230/LIPIcs.CONCUR.2021.5}, url = {https://doi.org/10.4230/LIPIcs.CONCUR.2021.5}, pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/14382/pdf/LIPIcs-CONCUR-2021-5.pdf}, dblp_id = {conf/concur/EsparzaKKW21}, funding = {DFG-CONVEY}, month = {August}, }
79. Xiao Wang, Hanna Krasowski, and Matthias Althoff. CommonRoad-RL: A Configurable Reinforcement Learning Environment for Motion Planning of Autonomous Vehicles. In 24th IEEE International Intelligent Transportation Systems Conference, ITSC 2021, Indianapolis, IN, USA, September 19-22, 2021, pages 466-472, September 2021. IEEE. doi:10.1109/ITSC48978.2021.9564898 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{WangKA21, author = {Xiao Wang and Hanna Krasowski and Matthias Althoff}, title = {CommonRoad-RL: A Configurable Reinforcement Learning Environment for Motion Planning of Autonomous Vehicles}, booktitle = {24th {IEEE} International Intelligent Transportation Systems Conference, {ITSC} 2021, Indianapolis, IN, USA, September 19-22, 2021}, pages = {466-472}, year = {2021}, publisher = {IEEE}, doi = {10.1109/ITSC48978.2021.9564898}, url = {https://commonroad.in.tum.de/commonroad-rl}, pdf = {http://mediatum.ub.tum.de/doc/1616584/pbazfbwsvmisz7qko1odv8d8f.pdf}, code = {https://gitlab.lrz.de/tum-cps/commonroad-rl}, dblp_id = {conf/itsc/WangKA21}, funding = {DFG-CONVEY}, month = {September}, }
80. Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, and Vesal Vojdani. Improving Thread-Modular Abstract Interpretation. In Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, LNCS, pages 359-383, October 2021. Springer. doi:10.1007/978-3-030-88806-0_18 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SchwarzSSAEV21, author = {Michael Schwarz and Simmo Saan and Helmut Seidl and Kalmer Apinis and Julian Erhard and Vesal Vojdani}, title = {Improving Thread-Modular Abstract Interpretation}, booktitle = {Static Analysis - 28th International Symposium, {SAS} 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings}, volume = {12913}, pages = {359--383}, year = {2021}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-88806-0_18}, code = {https://zenodo.org/record/5148608}, dblp_id = {conf/sas/SchwarzSSAEV21}, funding = {DFG-CONVEY}, month = {October}, preprint = {https://arxiv.org/abs/2108.07613}, }
81. Hashemi, Vahid, Křetínský, Jan, Mohr, Stefanie, and Seferis, Emmanouil. Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks. In Runtime Verification - 21st International Conference, RV 2021, Virtual Event, October 11-14, 2021, Proceedings, pages 254-264, October 2021. Springer International Publishing. doi:10.1007/978-3-030-88494-9_14 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{HashemiKMS21, author = {Hashemi, Vahid and K{\v{r}}et{\'i}nsk{\'y}, Jan and Mohr, Stefanie and Seferis, Emmanouil}, title = {Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks}, booktitle = {Runtime Verification - 21st International Conference, {RV} 2021, Virtual Event, October 11-14, 2021, Proceedings}, pages = {254--264}, year = {2021}, publisher = {Springer International Publishing}, doi = {10.1007/978-3-030-88494-9_14}, pdf = {https://www7.in.tum.de/~mohr/files/RVpaper.pdf}, address = {Cham}, dblp_id = {conf/rv/HashemiKMS21}, funding = {DFG-CONVEY}, month = {October}, }
82. Maximilian Weininger, Kush Grover, Shruti Misra, and Jan Kretínský. Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games. In 2021 60th IEEE Conference on Decision and Control (CDC), Austin, TX, USA, December 14-17, 2021, pages 3786-3793, December 2021. IEEE. doi:10.1109/CDC45484.2021.9683447 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{WeiningerGMK21, author = {Maximilian Weininger and Kush Grover and Shruti Misra and Jan Kret{\'{\i}}nsk{\'{y}}}, title = {Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games}, booktitle = {2021 60th {IEEE} Conference on Decision and Control (CDC), Austin, TX, USA, December 14-17, 2021}, pages = {3786--3793}, year = {2021}, publisher = {{IEEE}}, doi = {10.1109/CDC45484.2021.9683447}, url = {https://doi.org/10.1109/CDC45484.2021.9683447}, dblp_id = {conf/cdc/WeiningerGMK21}, funding = {DFG-CONVEY}, month = {December}, }
83. L. Geretti, J. Alexandre Dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, P. Collins, P.S. Duggirala, M. Forets, E. Kim, U. Linares, D.P. Sanders, C. Schilling, and M. Wetzlinger. ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. In 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021, pages 32-54, December 2021. doi:10.29007/2jw8 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{GerettiSABCCDFK21, author = {L. Geretti and J. {Alexandre Dit Sandretto} and M. Althoff and L. Benet and A. Chapoutot and P. Collins and P.S. Duggirala and M. Forets and E. Kim and U. Linares and D.P. Sanders and C. Schilling and M. Wetzlinger}, title = {{ARCH-COMP}21 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics}, booktitle = {8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021}, pages = {32--54}, year = {2021}, doi = {10.29007/2jw8}, url = {https://easychair.org/publications/paper/GWwz}, dblp_id = {conf/arch/GerettiSABCCDFK21}, funding = {DFG-CONVEY}, month = {December}, organization = {EasyChair}, }
84. M. Althoff, E. Ábrahám, M. Forets, G. Frehse, D. Freire, C. Schilling, S. Schupp, and M. Wetzlinger. ARCH-COMP21 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics. In 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021, pages 1-31, December 2021. doi:10.29007/lhbw Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @inproceedings{AlthoffAFFF0SW21, author = {M. Althoff and E. \'{A}brah\'{a}m and M. Forets and G. Frehse and D. Freire and C. Schilling and S. Schupp and M. Wetzlinger}, title = {{ARCH-COMP21} Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics}, booktitle = {8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021}, pages = {1--31}, year = {2021}, doi = {10.29007/lhbw}, dblp_id = {conf/arch/AlthoffAFFF0SW21}, funding = {DFG-CONVEY}, month = {December}, organization = {EasyChair}, }
85. Anand, Mahathi, Murali, Vishnu, Trivedi, Ashutosh, and Zamani, Majid. Safety Verification of Dynamical Systems via k-Inductive Barrier Certificates. In 2021 60th IEEE Conference on Decision and Control (CDC), Austin, TX, USA, December 14-17, 2021, pages 1314-1320, December 2021. doi:10.1109/CDC45484.2021.9682889 Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @inproceedings{AnandM0Z21a, author = {Anand, Mahathi and Murali, Vishnu and Trivedi, Ashutosh and Zamani, Majid}, title = {Safety Verification of Dynamical Systems via k-Inductive Barrier Certificates}, booktitle = {2021 60th {IEEE} Conference on Decision and Control (CDC), Austin, TX, USA, December 14-17, 2021}, volume = {}, number = {}, pages = {1314-1320}, year = {2021}, doi = {10.1109/CDC45484.2021.9682889}, dblp_id = {conf/cdc/AnandM0Z21}, funding = {DFG-CONVEY}, month = {December}, }
86. Stefanie Mohr, Konstantina Drainas, and Jürgen Geist. Assessment of Neural Networks for Stream-Water-Temperature Prediction. In 20th IEEE International Conference on Machine Learning and Applications, ICMLA 2021, Pasadena, CA, USA, December 13-16, 2021, pages 891-896, December 2021. IEEE. doi:10.1109/ICMLA52953.2021.00147 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{MohrDG21, author = {Stefanie Mohr and Konstantina Drainas and J{\"{u}}rgen Geist}, title = {Assessment of Neural Networks for Stream-Water-Temperature Prediction}, booktitle = {20th {IEEE} International Conference on Machine Learning and Applications, {ICMLA} 2021, Pasadena, CA, USA, December 13-16, 2021}, pages = {891--896}, year = {2021}, publisher = {{IEEE}}, doi = {10.1109/ICMLA52953.2021.00147}, url = {https://doi.org/10.1109/ICMLA52953.2021.00147}, dblp_id = {conf/icmla/MohrDG21}, funding = {DFG-CONVEY}, month = {December}, preprint = {https://arxiv.org/abs/2110.04254}, }
87. 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 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.}, artifact = {10.5281/zenodo.5070156}, funding = {DFG-CONVEY}, }
88. Daniel Baier, Dirk Beyer, and Karlheinz Friedberger. JavaSMT 3: Interacting with SMT Solvers in Java. In 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 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)}, 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 = {}, _pdf = {https://www.sosy-lab.org/research/pub/2021-CAV.JavaSMT_3_Interacting_with_SMT_Solvers_in_Java.pdf}, funding = {DFG-CONVEY}, }
89. Dirk Beyer. Software Verification: 10th Comparative Evaluation (SV-COMP 2021). In 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 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}, 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 = {}, funding = {DFG-CONVEY}, }
90. Mahathi Anand, Abolfazl Lavaei, and Majid Zamani. Compositional Synthesis of Control Barrier Certificates for Networks of Stochastic Systems against -Regular Specifications. CoRR, abs/2103.02226, March 2021. Funding: DFG-CONVEY
    BibTeX Entry

    @misc{AnandLZ21, author = {Mahathi Anand and Abolfazl Lavaei and Majid Zamani}, title = {Compositional Synthesis of Control Barrier Certificates for Networks of Stochastic Systems against $\omega$-Regular Specifications}, journal = {CoRR}, volume = {abs/2103.02226}, year = {2021}, archiveprefix = {arXiv}, dblp_id = {journals/corr/abs-2103-02226}, eprint = {2103.02226}, funding = {DFG-CONVEY}, month = {March}, preprint = {https://arxiv.org/abs/2103.02226}, primaryclass = {eess.SY}, type = {preprint}, }
91. Mahathi Anand, Vishnu Murali, Ashutosh Trivedi, and Majid Zamani. Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates. May 2021. Funding: DFG-CONVEY
    BibTeX Entry

    @misc{anand2021formal, author = {Mahathi Anand and Vishnu Murali and Ashutosh Trivedi and Majid Zamani}, title = {Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates}, volume = {abs/2105.05493}, year = {2021}, archiveprefix = {arXiv}, dblp_id = {none}, eprint = {2105.05493}, eprinttype = {arXiv}, funding = {DFG-CONVEY}, month = {May}, preprint = {https://arxiv.org/abs/2105.05493}, primaryclass = {eess.SY}, type = {preprint}, }

2020

92. Christian Müller and Helmut Seidl. Stratified Guarded First-Order Transition Systems. In Static Analysis - 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020, Proceedings, LNCS, pages 113-133, January 2020. Springer. doi:10.1007/978-3-030-65474-0_6 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{MullerS20, author = {Christian M{\"{u}}ller and Helmut Seidl}, title = {Stratified Guarded First-Order Transition Systems}, booktitle = {Static Analysis - 27th International Symposium, {SAS} 2020, Virtual Event, November 18-20, 2020, Proceedings}, volume = {12389}, pages = {113--133}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-65474-0_6}, url = {https://doi.org/10.1007/978-3-030-65474-0\_6}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/sas/MullerS20.bib}, dblp_id = {conf/sas/MullerS20}, funding = {DFG-CONVEY}, month = {January}, timestamp = {Fri, 29 Jan 2021 16:47:04 +0100}, }
93. Helmut Seidl, Christian Müller, and Bernd Finkbeiner. How to Win First-Order Safety Games. In Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings, LNCS, pages 426-448, January 2020. Springer. doi:10.1007/978-3-030-39322-9_20 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{SeidlMF20, author = {Helmut Seidl and Christian M{\"{u}}ller and Bernd Finkbeiner}, title = {How to Win First-Order Safety Games}, booktitle = {Verification, Model Checking, and Abstract Interpretation - 21st International Conference, {VMCAI} 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings}, volume = {11990}, pages = {426--448}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-39322-9_20}, url = {https://doi.org/10.1007/978-3-030-39322-9\_20}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/vmcai/SeidlMF20.bib}, dblp_id = {conf/vmcai/SeidlMF20}, funding = {DFG-CONVEY}, month = {January}, timestamp = {Thu, 16 Jan 2020 17:28:31 +0100}, }
94. Helmut Seidl, Julian Erhard, and Ralf Vogler. Incremental Abstract Interpretation. In From Lambda Calculus to Cybersecurity Through Program Analysis - Essays Dedicated to Chris Hankin on the Occasion of His Retirement, LNCS, pages 132-148, March 2020. Springer. doi:10.1007/978-3-030-41103-9_5 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{SeidlEV15, author = {Helmut Seidl and Julian Erhard and Ralf Vogler}, title = {Incremental Abstract Interpretation}, booktitle = {From Lambda Calculus to Cybersecurity Through Program Analysis - Essays Dedicated to Chris Hankin on the Occasion of His Retirement}, volume = {12065}, pages = {132--148}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-41103-9_5}, dblp_id = {conf/birthday/SeidlEV15}, funding = {DFG-CONVEY}, month = {March}, }
95. Blondin, Michael, Esparza, Javier, Genest, Blaise, Helfrich, Martin, and Jaax, Stefan. Succinct Population Protocols for Presburger Arithmetic. In 37th International Symposium on Theoretical Aspects of Computer Science, STACS 2020, March 10-13, 2020, Montpellier, France, LIPIcs, pages 40:1-40:15, March 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.STACS.2020.40 Funding: DFG-CONVEY Publisher's Version Supplement
    BibTeX Entry

    @inproceedings{BlondinEGHJ20, author = {Blondin, Michael and Esparza, Javier and Genest, Blaise and Helfrich, Martin and Jaax, Stefan}, title = {Succinct Population Protocols for Presburger Arithmetic}, booktitle = {37th International Symposium on Theoretical Aspects of Computer Science, {STACS} 2020, March 10-13, 2020, Montpellier, France}, volume = {154}, pages = {40:1-40:15}, year = {2020}, series = {LIPIcs}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, doi = {10.4230/LIPIcs.STACS.2020.40}, url = {https://drops.dagstuhl.de/opus/volltexte/2020/11901/}, dblp_id = {conf/stacs/BlondinEGHJ20}, ee = {https://doi.org/10.4230/LIPIcs.STACS.2020.40}, funding = {DFG-CONVEY}, interhash = {230c644b131b1ac85ebfc76b18c8d8b5}, intrahash = {bebbfaec40c7c65fe3824d447690f9db}, keywords = {myown populationprotocols succinct synthesis}, month = {March}, preprint = {https://arxiv.org/abs/1910.04600}, timestamp = {2020-10-01T19:12:36.000+0200}, }
96. Anastasiia Izycheva, Eva Darulova, and Helmut Seidl. Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis. In Static Analysis - 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020, Proceedings, LNCS, pages 156-177, April 2020. Springer. doi:10.1007/978-3-030-65474-0_8 Funding: DFG-CONVEY Publisher's Version PDF Supplement
    BibTeX Entry

    @inproceedings{IzychevaDS20, author = {Anastasiia Izycheva and Eva Darulova and Helmut Seidl}, title = {Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis}, booktitle = {Static Analysis - 27th International Symposium, {SAS} 2020, Virtual Event, November 18-20, 2020, Proceedings}, volume = {12389}, pages = {156--177}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-65474-0_8}, url = {https://doi.org/10.1007/978-3-030-65474-0\_8}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/sas/IzychevaDS20.bib}, dblp_id = {conf/sas/IzychevaDS20}, funding = {DFG-CONVEY}, month = {April}, timestamp = {Sat, 09 Apr 2022 12:38:54 +0200}, }
97. Niloofar Jahanshahi, Pushpak Jagtap, and Majid Zamani. Synthesis of Stochastic Systems with Partial Information via Control Barrier Functions. In 21st IFAC World Congress (IFAC-V 2020), July 2020. doi:10.1016/j.ifacol.2020.12.187 Funding: DFG-CONVEY Publisher's Version PDF
    BibTeX Entry

    @inproceedings{JahanshahiJZ21b, author = {Niloofar Jahanshahi and Pushpak Jagtap and Majid Zamani}, title = {Synthesis of Stochastic Systems with Partial Information via Control Barrier Functions}, booktitle = {21st IFAC World Congress (IFAC-V 2020)}, year = {2020}, doi = {10.1016/j.ifacol.2020.12.187}, pdf = {https://www.sciencedirect.com/science/article/pii/S2405896320304523/pdf?md5=76fdfacc74fb7ee5195b2d89cebe253a&pid=1-s2.0-S2405896320304523-main.pdf}, dblp_id = {none}, funding = {DFG-CONVEY}, month = {July}, }
98. Mahathi Anand, Abolfazl Lavaei, and Majid Zamani. Compositional Construction of Control Barrier Certificates for Large-Scale Interconnected Stochastic Systems. In Proceedings of the 21st IFAC World Congress, July 2020. doi:10.1016/j.ifacol.2020.12.2355 Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @inproceedings{AnandLZ20, author = {Mahathi Anand and Abolfazl Lavaei and Majid Zamani}, title = {Compositional Construction of Control Barrier Certificates for Large-Scale Interconnected Stochastic Systems}, booktitle = {Proceedings of the 21st IFAC World Congress}, year = {2020}, doi = {10.1016/j.ifacol.2020.12.2355}, dblp_id = {none}, funding = {DFG-CONVEY}, month = {July}, }
99. M. Althoff, S. Bak, Z. Bao, M. Forets, G. Frehse, D. Freire, N. Kochdumper, Y. Li, S. Mitra, R. Ray, C. Schilling, S. Schupp, and M. Wetzlinger. ARCH-COMP20 category report: Continuous and hybrid systems with linear continuous dynamics. In ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), Berlin, Germany, July 12, 2020, pages 16-48, September 2020. doi:10.29007/7dt2 Funding: DFG-CONVEY Publisher's Version
    BibTeX Entry

    @inproceedings{AlthoffBBFFFKLM20, author = {M. Althoff and S. Bak and Z. Bao and M. Forets and G. Frehse and D. Freire and N. Kochdumper and Y. Li and S. Mitra and R. Ray and C. Schilling and S. Schupp and M. Wetzlinger}, title = {{ARCH-COMP}20 category report: Continuous and hybrid systems with linear continuous dynamics}, booktitle = {{ARCH20.} 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), Berlin, Germany, July 12, 2020}, pages = {16--48}, year = {2020}, doi = {10.29007/7dt2}, dblp_id = {conf/arch/AlthoffBBFFFKLM20}, funding = {DFG-CONVEY}, month = {September}, organization = {EasyChair}, }
100. L. Geretti, J. Alexandre dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, P. Collins, P.S. Duggirala, M. Forets, E. Kim, U. Linares, D.P. Sanders, C. Schilling, and M. Wetzlinger. ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics. In ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), Berlin, Germany, July 12, 2020, pages 49-75, September 2020. doi:10.29007/zkf6 Funding: DFG-CONVEY Publisher's Version
     BibTeX Entry

     @inproceedings{GerettiSABCCCFF20, author = {L. Geretti and J. {Alexandre dit Sandretto} and M. Althoff and L. Benet and A. Chapoutot and P. Collins and P.S. Duggirala and M. Forets and E. Kim and U. Linares and D.P. Sanders and C. Schilling and M. Wetzlinger}, title = {{ARCH-COMP}20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics}, booktitle = {{ARCH20.} 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), Berlin, Germany, July 12, 2020}, pages = {49--75}, year = {2020}, doi = {10.29007/zkf6}, dblp_id = {conf/arch/GerettiSABCCCFF20}, funding = {DFG-CONVEY}, month = {September}, organization = {EasyChair}, }
101. Krasowski, Hanna, Wang, Xiao, and Althoff, Matthias. Safe Reinforcement Learning for Autonomous Lane Changing Using Set-Based Prediction. In 23rd IEEE International Conference on Intelligent Transportation Systems, ITSC 2020, Rhodes, Greece, September 20-23, 2020, pages 1-7, September 2020. doi:10.1109/ITSC45102.2020.9294259 Funding: DFG-CONVEY Publisher's Version PDF
     BibTeX Entry

     @inproceedings{KrasowskiWA20, author = {Krasowski, Hanna and Wang, Xiao and Althoff, Matthias}, title = {Safe Reinforcement Learning for Autonomous Lane Changing Using Set-Based Prediction}, booktitle = {23rd {IEEE} International Conference on Intelligent Transportation Systems, {ITSC} 2020, Rhodes, Greece, September 20-23, 2020}, pages = {1-7}, year = {2020}, doi = {10.1109/ITSC45102.2020.9294259}, pdf = {https://mediatum.ub.tum.de/doc/1548735/256213.pdf}, dblp_id = {conf/itsc/KrasowskiWA20}, funding = {DFG-CONVEY}, month = {September}, }
102. Pranav Ashok, Vahid Hashemi, Jan Kretínský, and Stefanie Mohr. DeepAbstract: Neural Network Abstraction for Accelerating Verification. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, LNCS, pages 92-107, October 2020. Springer. doi:10.1007/978-3-030-59152-6_5 Funding: DFG-CONVEY Publisher's Version PDF
     BibTeX Entry

     @inproceedings{AshokHKM20, author = {Pranav Ashok and Vahid Hashemi and Jan Kret{\'{\i}}nsk{\'{y}} and Stefanie Mohr}, title = {DeepAbstract: Neural Network Abstraction for Accelerating Verification}, booktitle = {Automated Technology for Verification and Analysis - 18th International Symposium, {ATVA} 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings}, volume = {12302}, pages = {92--107}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-59152-6_5}, dblp_id = {conf/atva/AshokHKM20}, funding = {DFG-CONVEY}, month = {October}, preprint = {https://arxiv.org/pdf/2006.13735}, }
103. D'Antoni, Loris, Helfrich, Martin, Kretínský, Jan, Ramneantu, Emanuel, and Weininger, Maximilian. Automata Tutor v3. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, LNCS, pages 3-14, October 2020. Springer. doi:10.1007/978-3-030-53291-8_1 Funding: DFG-CONVEY Publisher's Version PDF Supplement
     BibTeX Entry

     @inproceedings{DAntoniHKRW20, author = {D'Antoni, Loris and Helfrich, Martin and Kret{\'{\i}}nsk{\'{y}}, Jan and Ramneantu, Emanuel and Weininger, Maximilian}, title = {Automata Tutor v3}, booktitle = {Computer Aided Verification - 32nd International Conference, {CAV} 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}}, volume = {12225}, pages = {3-14}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-53291-8_1}, url = {https://link.springer.com/chapter/10.1007/978-3-030-53291-8_1}, pdf = {https://link.springer.com/content/pdf/10.1007/978-3-030-53291-8_1.pdf}, dblp_id = {conf/cav/DAntoniHKRW20}, ee = {https://doi.org/10.1007/978-3-030-53291-8_1}, funding = {DFG-CONVEY}, interhash = {41bb208bad84e6141ca1aad7256c86aa}, intrahash = {6aef6725bb29fe9ba9192404ef70e8c1}, keywords = {tool}, month = {October}, preprint = {https://arxiv.org/abs/2005.01419}, timestamp = {2020-10-01T19:10:55.000+0200}, }
104. Blondin, Michael, Esparza, Javier, Helfrich, Martin, Kucera, Antoní­n, and Meyer, Philipp J.. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, LNCS, pages 372-397, October 2020. Springer. doi:10.1007/978-3-030-53291-8_20 Funding: DFG-CONVEY Publisher's Version PDF Supplement
     BibTeX Entry

     @inproceedings{BlondinEH0M20, author = {Blondin, Michael and Esparza, Javier and Helfrich, Martin and Kucera, Antoní­n and Meyer, Philipp J.}, title = {Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling}, booktitle = {Computer Aided Verification - 32nd International Conference, {CAV} 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}}, volume = {12225}, pages = {372-397}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-53291-8_20}, url = {https://link.springer.com/chapter/10.1007/978-3-030-53291-8_20}, dblp_id = {conf/cav/BlondinEH0M20}, ee = {https://doi.org/10.1007/978-3-030-53291-8_20}, funding = {DFG-CONVEY}, interhash = {306ccad2c5a9d4368e4e684e1d91815a}, intrahash = {24d25cf103539a6a5b6f3e08de94cef0}, keywords = {liveness parametrizedverification populationprotocols replicated systems verification}, month = {October}, preprint = {https://arxiv.org/abs/2005.03555}, timestamp = {2020-10-01T19:10:23.000+0200}, }
105. Javier Esparza, Martin Helfrich, Stefan Jaax, and Philipp J. Meyer. Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, LNCS, pages 550-556, October 2020. Springer. doi:10.1007/978-3-030-59152-6_32 Funding: DFG-CONVEY Publisher's Version PDF Supplement
     BibTeX Entry

     @inproceedings{EsparzaHJM20, author = {Javier Esparza and Martin Helfrich and Stefan Jaax and Philipp J. Meyer}, title = {Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs}, booktitle = {Automated Technology for Verification and Analysis - 18th International Symposium, {ATVA} 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings}, volume = {12302}, pages = {550--556}, year = {2020}, series = {LNCS}, publisher = {Springer}, doi = {10.1007/978-3-030-59152-6_32}, url = {https://doi.org/10.1007/978-3-030-59152-6\_32}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/atva/EsparzaHJM20.bib}, dblp_id = {conf/atva/EsparzaHJM20}, funding = {DFG-CONVEY}, month = {October}, preprint = {https://arxiv.org/abs/2007.07638}, timestamp = {Tue, 20 Oct 2020 18:27:30 +0200}, }
106. Mark Wetzlinger, Niklas Kochdumper, and Matthias Althoff. Adaptive Parameter Tuning for Reachability Analysis of Linear Systems. In 59th IEEE Conference on Decision and Control, CDC 2020, Jeju Island, South Korea, December 14-18, 2020, pages 5145-5152, December 2020. doi:10.1109/CDC42340.2020.9304431 Funding: DFG-CONVEY Publisher's Version PDF
     Abstract

     Despite the possibility to quickly compute reachable sets of large-scale linear systems, current methods are not yet widely applied by practitioners. The main reason for this is probably that current approaches are not push-button-capable and still require to manually set crucial parameters, such as time step sizes and the accuracy of the used set representation—€these settings require expert knowledge. We present a generic framework to automatically find near-optimal parameters for reachability analysis of linear systems given a user-defined accuracy. To limit the computational overhead as much as possible, our methods tune all relevant parameters during runtime. We evaluate our approach on benchmarks from the ARCH competition as well as on random examples. The results show that our new framework verifies the selected benchmarks faster than manually-tuned parameters and is an order of magnitude faster compared to genetic algorithms.
     BibTeX Entry

     @inproceedings{WetzlingerKA20, author = {Mark {Wetzlinger} and Niklas {Kochdumper} and Matthias {Althoff}}, title = {Adaptive Parameter Tuning for Reachability Analysis of Linear Systems}, booktitle = {59th {IEEE} Conference on Decision and Control, {CDC} 2020, Jeju Island, South Korea, December 14-18, 2020}, volume = {}, number = {}, pages = {5145-5152}, year = {2020}, doi = {10.1109/CDC42340.2020.9304431}, pdf = {http://mediatum.ub.tum.de/doc/1591476/fym5w7280kyl4yazcsxhhbv68.pdf}, abstract = {Despite the possibility to quickly compute reachable sets of large-scale linear systems, current methods are not yet widely applied by practitioners. The main reason for this is probably that current approaches are not push-button-capable and still require to manually set crucial parameters, such as time step sizes and the accuracy of the used set representation—€these settings require expert knowledge. We present a generic framework to automatically find near-optimal parameters for reachability analysis of linear systems given a user-defined accuracy. To limit the computational overhead as much as possible, our methods tune all relevant parameters during runtime. We evaluate our approach on benchmarks from the ARCH competition as well as on random examples. The results show that our new framework verifies the selected benchmarks faster than manually-tuned parameters and is an order of magnitude faster compared to genetic algorithms.}, dblp_id = {conf/cdc/WetzlingerKA20}, funding = {DFG-CONVEY}, issn = {2576-2370}, keywords = {Reachability analysis;Tuning;Linear systems;Measurement uncertainty;Trajectory;Tools;Time measurement}, month = {December}, preprint = {https://arxiv.org/pdf/2006.12091.pdf}, }
107. Dirk Beyer and Karlheinz Friedberger. Domain-Independent Interprocedural Program Analysis using Block-Abstraction Memoization. In 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 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)}, pages = {50-62}, year = {2020}, publisher = {ACM}, doi = {10.1145/3368089.3409718}, url = {https://cpachecker.sosy-lab.org}, _sha256 = {36dc2a423425ee8bec03f0f4073e04f9121d299cc475e27190828e8276e00cb8}, artifact = {10.5281/zenodo.4024268}, funding = {DFG-CONVEY}, fundingid = {378803395}, }
108. Dirk Beyer and Karlheinz Friedberger. Violation Witnesses and Result Validation for Multi-Threaded Programs. In 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 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}, 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 = {}, funding = {DFG-CONVEY}, }
109. Dirk Beyer and Sudeep Kanav. An Interface Theory for Program Verification. In 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 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}, 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 = {}, funding = {DFG-CONVEY}, }
110. Dirk Beyer, Marie-Christine Jakobs, and Thomas Lemberger. Difference Verification with Conditions. In 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 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)}, 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.}, funding = {DFG-COOP,DFG-CONVEY}, isbnnote = {}, video = {https://youtu.be/dG02602c9oo}, }
111. Dirk Beyer and Martin Spiessl. MetaVal: Witness Validation via Verification. In 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 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}, 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 = {}, funding = {DFG-CONVEY}, isbnnote = {978-3-030-53290-1}, }

2019

112. Susanne Albers. On Energy Conservation in Data Centers. ACM Trans. Parallel Comput., 6(3):13:1-13:26, September 2019. doi:10.1145/3364210 Funding: DFG-CONVEY Publisher's Version PDF Supplement
     BibTeX Entry

     @article{Albers19, author = {Susanne Albers}, title = {On Energy Conservation in Data Centers}, journal = {{ACM} Trans. Parallel Comput.}, volume = {6}, number = {3}, pages = {13:1--13:26}, year = {2019}, doi = {10.1145/3364210}, url = {https://doi.org/10.1145/3364210}, dblp_id = {journals/topc/Albers19}, funding = {DFG-CONVEY}, month = {September}, }
113. Mahmoud Khaled and Majid Zamani. pFaces: an acceleration ecosystem for symbolic control. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 252-257, April 2019. ACM. doi:10.1145/3302504.3311798 Funding: DFG-CONVEY Publisher's Version PDF Supplement
     BibTeX Entry

     @inproceedings{KhaledZ19, author = {Mahmoud Khaled and Majid Zamani}, title = {pFaces: an acceleration ecosystem for symbolic control}, booktitle = {Proceedings of the 22nd {ACM} International Conference on Hybrid Systems: Computation and Control, {HSCC} 2019, Montreal, QC, Canada, April 16-18, 2019}, pages = {252--257}, year = {2019}, publisher = {{ACM}}, doi = {10.1145/3302504.3311798}, url = {https://doi.org/10.1145/3302504.3311798}, bibsource = {dblp computer science bibliography, https://dblp.org}, biburl = {https://dblp.org/rec/conf/hybrid/KhaledZ19.bib}, dblp_id = {conf/hybrid/KhaledZ19}, funding = {DFG-CONVEY}, month = {April}, timestamp = {Tue, 20 Dec 2022 14:49:49 +0100}, }
114. Mahathi Anand, Pushpak Jagtap, and Majid Zamani. Verification of Switched Stochastic Systems via Barrier Certificates. In 58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019, pages 4373-4378, December 2019. IEEE. doi:10.1109/CDC40024.2019.9028862 Funding: DFG-CONVEY Publisher's Version
     BibTeX Entry

     @inproceedings{AnandJZ19, author = {Mahathi Anand and Pushpak Jagtap and Majid Zamani}, title = {Verification of Switched Stochastic Systems via Barrier Certificates}, booktitle = {58th {IEEE} Conference on Decision and Control, {CDC} 2019, Nice, France, December 11-13, 2019}, pages = {4373--4378}, year = {2019}, publisher = {{IEEE}}, doi = {10.1109/CDC40024.2019.9028862}, dblp_id = {conf/cdc/AnandJZ19}, funding = {DFG-CONVEY}, month = {December}, }