Publications by year
2024
-
A Transferability Study of Interpolation-Based Hardware Model Checking for Software Verification.
Proc. ACM Softw. Eng., 1(FSE),
2024.
ACM.
doi:10.1145/3660797
Funding:
DFG-CONVEY
Publisher's Version
PDF
Presentation
Supplement
Artifact(s)
Abstract
Assuring the correctness of computing systems is fundamental to our society and economy, and formal verification is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, Craig interpolation has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1) Interpolation-Sequence-Based Model Checking (Vizel and Grumberg, 2009) and (2) Intertwined Forward-Backward Reachability Analysis Using Interpolants (Vizel, Grumberg, and Shoham, 2013), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.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 for Software Verification}, journal = {Proc. ACM Softw. Eng.}, volume = {1}, number = {FSE}, year = {2024}, publisher = {ACM}, doi = {10.1145/3660797}, url = {https://www.sosy-lab.org/research/dar-ismc-transferability/}, presentation = {https://www.sosy-lab.org/research/prs/2024-07-18_FSE_A_Transferability_Study_of_Interpolation-Based_HWMC_for_SV_Marek.pdf}, abstract = {Assuring the correctness of computing systems is fundamental to our society and economy, and <em>formal verification</em> is a class of techniques approaching this issue with mathematical rigor. Researchers have invented numerous algorithms to automatically prove whether a computational model, e.g., a software program or a hardware digital circuit, satisfies its specification. In the past two decades, <em>Craig interpolation</em> has been widely used in both hardware and software verification. Despite the similarities in the theoretical foundation between hardware and software verification, previous works usually evaluate interpolation-based algorithms on only one type of verification tasks (e.g., either circuits or programs), so the conclusions of these studies do not necessarily transfer to different types of verification tasks. To investigate the transferability of research conclusions from hardware to software, we adopt two performant approaches of interpolation-based hardware model checking, (1) <em>Interpolation-Sequence-Based Model Checking</em> (<a href="https://doi.org/10.1109/FMCAD.2009.5351148">Vizel and Grumberg, 2009</a>) and (2) <em>Intertwined Forward-Backward Reachability Analysis Using Interpolants</em> (<a href="https://doi.org/10.1007/978-3-642-36742-7_22">Vizel, Grumberg, and Shoham, 2013</a>), for software verification. We implement the algorithms proposed by the two publications in the software verifier CPAchecker because it has a software-verification adoption of the first interpolation-based algorithm for hardware model checking from 2003, which the two publications use as a comparison baseline. To assess whether the claims in the two publications transfer to software verification, we conduct an extensive experiment on the largest publicly available suite of safety-verification tasks for the programming language C. Our experimental results show that the important characteristics of the two approaches for hardware model checking are transferable to software verification, and that the cross-disciplinary algorithm adoption is beneficial, as the approaches adopted from hardware model checking were able to tackle tasks unsolvable by existing methods. This work consolidates the knowledge in hardware and software verification and provides open-source implementations to improve the understanding of the compared interpolation-based algorithms.}, _pdf = {https://www.sosy-lab.org/research/pub/2024-FSE.A_Transferability_Study_of_Interpolation-Based_Hardware_Model_Checking_for_Software_Verification.pdf}, annote = {This article received the "ACM SIGSOFT Distinguished Paper Award" and its reproduction artifact received the "ACM SIGSOFT Best Artifact Award" at <a href="https://2024.esec-fse.org/info/awards">FSE 2024</a>!}, articleno = {90}, artifact = {10.5281/zenodo.11070973}, funding = {DFG-CONVEY}, issue_date = {July 2024}, numpages = {23}, }Additional Infos
This article received the "ACM SIGSOFT Distinguished Paper Award" and its reproduction artifact received the "ACM SIGSOFT Best Artifact Award" at FSE 2024! -
Decomposing Software Verification using Distributed Summary Synthesis.
Proc. ACM Softw. Eng., 1(FSE),
2024.
ACM.
doi:10.1145/3660766
Funding:
DFG-CONVEY,
DFG-COOP
Publisher's Version
PDF
Supplement
Artifact(s)
Abstract
There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries are computed — based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (which program states reach this block) and verification conditions to check at the block exit (which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a precondition or verification condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach as an extension of the configurable-program-analysis algorithm and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.BibTeX Entry
@article{DSS-PACMSE, author = {Dirk Beyer and Matthias Kettl and Thomas Lemberger}, title = {Decomposing Software Verification using Distributed Summary Synthesis}, journal = {Proc. ACM Softw. Eng.}, volume = {1}, number = {FSE}, year = {2024}, publisher = {ACM}, doi = {10.1145/3660766}, url = {https://www.sosy-lab.org/research/distributed-summary-synthesis/}, presentation = {}, abstract = {There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries are computed — based on independent, distributed, continuous refinement by communication between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (which program states reach this block) and verification conditions to check at the block exit (which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a precondition or verification condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach as an extension of the configurable-program-analysis algorithm and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.}, _pdf = {https://www.sosy-lab.org/research/pub/2024-FSE.Decomposing_Software_Verification_using_Distributed_Summary_Synthesis.pdf}, articleno = {90}, artifact = {10.5281/zenodo.11095864}, funding = {DFG-CONVEY,DFG-COOP}, issue_date = {July 2024}, numpages = {23}, } -
Robust Feature Inference: A Test-time Defense Strategy using Spectral Projections.
Transactions on Machine Learning Research,
2024.
Funding:
DFG-CONVEY
Supplement
BibTeX Entry
@article{singh2024robust, author = {Anurag Singh and Mahalakshmi Sabanayagam and Krikamol Muandet and Debarghya Ghoshdastidar}, title = {Robust Feature Inference: A Test-time Defense Strategy using Spectral Projections}, journal = {Transactions on Machine Learning Research}, year = {2024}, url = {https://openreview.net/forum?id=9OHAtWdFWB}, funding = {DFG-CONVEY}, issn = {2835-8856}, note = {}, } -
Provable Robustness of (Graph) Neural Networks Against Data Poisoning and Backdoor Attacks.
arXiv preprint arXiv:2407.10867,
2024.
Funding:
DFG-CONVEY
BibTeX Entry
@article{gosch2024provable, author = {Gosch, Lukas and Sabanayagam, Mahalakshmi and Ghoshdastidar, Debarghya and G{\"u}nnemann, Stephan}, title = {Provable Robustness of (Graph) Neural Networks Against Data Poisoning and Backdoor Attacks}, journal = {arXiv preprint arXiv:2407.10867}, year = {2024}, funding = {DFG-CONVEY}, } -
BenchCloud: A Platform for Scalable Performance Benchmarking.
In Proc. ASE,
2024.
ACM.
doi:10.1145/3691620.3695358
Funding:
DFG-CONVEY,
DFG-COOP
Publisher's Version
PDF
Video
Supplement
Artifact(s)
Abstract
Performance evaluation is a crucial method for assessing automated-reasoning tools. Evaluating automated tools requires rigorous benchmarking to accurately measure resource consumption, including time and memory, which are essential for understanding the tools' capabilities. BenchExec, a widely used benchmarking framework, reliably measures resource usage for tools executed locally on a single node. This paper describes BenchCloud, a solution for elastic and scalable job distribution across hundreds of nodes, enabling large-scale experiments on distributed and heterogeneous computing environments. BenchCloud seamlessly integrates with BenchExec, allowing BenchExec to delegate the actual execution to BenchCloud. The system has been employed in several prominent international competitions in automated reasoning, including SMT-COMP, SV-COMP, and Test-Comp, underscoring its importance in rigorous tool evaluation across various research domains. It helps to ensure both internal and external validity of the experimental results. This paper presents an overview of BenchCloud's architecture and high- lights its primary use cases in facilitating scalable benchmarking.
Demonstration video: https://youtu.be/aBfQytqPm0U
Running system: https://benchcloud.sosy-lab.org/BibTeX Entry
@inproceedings{ASE24a, author = {Dirk Beyer and Po-Chun Chien and Marek Jankola}, title = {{BenchCloud}: {A} Platform for Scalable Performance Benchmarking}, booktitle = {Proc.\ ASE}, pages = {}, year = {2024}, series = {}, publisher = {ACM}, doi = {10.1145/3691620.3695358}, url = {https://benchcloud.sosy-lab.org/}, pdf = {https://www.sosy-lab.org/research/pub/2024-ASE24.BenchCloud_A_Platform_for_Scalable_Performance_Benchmarking.pdf}, presentation = {}, abstract = {Performance evaluation is a crucial method for assessing automated-reasoning tools. Evaluating automated tools requires rigorous benchmarking to accurately measure resource consumption, including time and memory, which are essential for understanding the tools' capabilities. BenchExec, a widely used benchmarking framework, reliably measures resource usage for tools executed locally on a single node. This paper describes BenchCloud, a solution for elastic and scalable job distribution across hundreds of nodes, enabling large-scale experiments on distributed and heterogeneous computing environments. BenchCloud seamlessly integrates with BenchExec, allowing BenchExec to delegate the actual execution to BenchCloud. The system has been employed in several prominent international competitions in automated reasoning, including SMT-COMP, SV-COMP, and Test-Comp, underscoring its importance in rigorous tool evaluation across various research domains. It helps to ensure both internal and external validity of the experimental results. This paper presents an overview of BenchCloud's architecture and high- lights its primary use cases in facilitating scalable benchmarking. <br> Demonstration video: <a href="https://youtu.be/aBfQytqPm0U">https://youtu.be/aBfQytqPm0U</a> <br> Running system: <a href="https://benchcloud.sosy-lab.org/">https://benchcloud.sosy-lab.org/</a>}, artifact = {10.5281/zenodo.13742756}, funding = {DFG-CONVEY, DFG-COOP}, video = {https://youtu.be/aBfQytqPm0U}, } -
CPA-Daemon: Mitigating Tool Restarts for Java-Based Verifiers.
In Proceedings of the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA 2024, Kyoto, Japan, October 21-24),
LNCS ,
2024.
Springer.
Funding:
DFG-CONVEY
PDF
Artifact(s)
BibTeX Entry
@inproceedings{ATVA24, author = {Dirk Beyer and Thomas Lemberger and Henrik Wachowitz}, title = {{CPA-Daemon}: Mitigating Tool Restarts for Java-Based Verifiers}, booktitle = {Proceedings of the 22nd International Symposium on Automated Technology for Verification and Analysis (ATVA~2024, Kyoto, Japan, October 21-24)}, pages = {}, year = {2024}, series = {LNCS~}, publisher = {Springer}, pdf = {https://www.sosy-lab.org/research/pub/2024-ATVA.CPA-Daemon_Mitigating_Tool_Restart_for_Java-Based_Verifiers.pdf}, abstract = {}, artifact = {https://doi.org/10.5281/zenodo.11147333}, doinone = {Unpublished: Last checked: 2024-10-01}, funding = {DFG-CONVEY}, } -
Software Verification with CPAchecker 3.0: Tutorial and User Guide.
In Proceedings of the 26th International Symposium on Formal Methods (FM 2024, Milan, Italy, September 9-13),
LNCS 14934,
pages 543-570,
2024.
Springer.
doi:10.1007/978-3-031-71177-0_30
Funding:
DFG-COOP,
DFG-CONVEY,
DFG-IDEFIX
Publisher's Version
PDF
Presentation
Supplement
Artifact(s)
Abstract
This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.BibTeX Entry
@inproceedings{FM24a, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marie-Christine Jakobs and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Henrik Wachowitz and Philipp Wendler}, title = {Software Verification with {CPAchecker} 3.0: {Tutorial} and User Guide}, booktitle = {Proceedings of the 26th International Symposium on Formal Methods (FM~2024, Milan, Italy, September 9-13)}, pages = {543-570}, year = {2024}, series = {LNCS~14934}, publisher = {Springer}, doi = {10.1007/978-3-031-71177-0_30}, url = {https://cpachecker.sosy-lab.org}, pdf = {https://www.sosy-lab.org/research/pub/2024-FM.Software_Verification_with_CPAchecker_3.0_Tutorial_and_User_Guide.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-09-10_FM24_CPAchecker_Tutorial.pdf}, abstract = {This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, <i>k</i>-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. An extended version also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at <a href="https://cpachecker.sosy-lab.org/doc.php">https://cpachecker.sosy-lab.org/doc.php</a>.}, annote = {An <a href="https://www.sosy-lab.org/research/bib/All/index.html#TechReport24c">extended version</a> of this article is available on <a href="https://doi.org/10.48550/arXiv.2409.02094">arXiv</a>.}, artifact = {10.5281/zenodo.13612338}, funding = {DFG-COOP, DFG-CONVEY, DFG-IDEFIX}, }Additional Infos
An extended version of this article is available on arXiv. -
Software Verification Witnesses 2.0.
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
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 = {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}, 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}, } -
Augmenting Interpolation-Based Model Checking with Auxiliary Invariants.
In Proceedings of the 30th International Symposium on Model Checking Software (SPIN 2024, Luxembourg City, Luxembourg, April 10-11),
LNCS 14624,
2024.
Springer.
doi:10.1007/978-3-031-66149-5_13
Funding:
DFG-CONVEY
Publisher's Version
PDF
Presentation
Supplement
Artifact(s)
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 = {Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11)}, pages = {}, year = {2024}, series = {LNCS~14624}, publisher = {Springer}, doi = {10.1007/978-3-031-66149-5_13}, 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}, 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. -
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)
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. -
CPAchecker 2.3 with Strategy Selection (Competition Contribution).
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 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)
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 = {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 = {359-364}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_21}, url = {https://cpachecker.sosy-lab.org/}, 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.}, _pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPAchecker_2.3_with_Strategy_Selection_Competition_Contribution.pdf}, artifact = {10.5281/zenodo.10203297}, funding = {DFG-CONVEY, DFG-IDEFIX}, } -
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}, } -
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)
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/}, 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.}, _pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.Btor2-Cert_A_Certifying_Hardware-Verification_Framework_Using_Software_Analyzers.pdf}, 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! -
CoVeriTeam GUI: A No-Code Approach to Cooperative Software Verification.
In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024, Sacramento, CA, USA, October 27-November 1),
2024.
Funding:
DFG-CONVEY
PDF
Artifact(s)
Abstract
We present CoVeriTeam GUI, a No-Code web frontend to compose new software-verification workflows from existing analysis techniques. Verification approaches stopped relying on single techniques years ago, and instead combine selections that complement each other well. So far, such combinations were-under high implementation and maintenance cost-glued together with proprietary code. Now, CoVeriTeam GUI enables users to build new verification workflows without programming. Verification techniques can be combined through various composition operators in a drag-and-drop fashion directly in the browser, and an integration with a remote service allows to execute the built workflows with the click of a button. CoVeriTeam GUI is available open source under Apache 2.0: https://gitlab.com/sosy-lab/software/coveriteam-gui
Demonstration video: https://youtu.be/oZoOARuIOuABibTeX Entry
@inproceedings{CoVeriTeamGUI-ASE24, author = {Thomas Lemberger and Henrik Wachowitz}, title = {CoVeriTeam GUI: A No-Code Approach to Cooperative Software Verification}, booktitle = {Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024, Sacramento, CA, USA, October 27-November 1)}, pages = {}, year = {2024}, doi = {}, pdf = {https://www.sosy-lab.org/research/pub/2024-ASE24.CoVeriTeam_GUI_A_No-Code_Approach_to_Cooperative_Software_Verification.pdf}, presentation = {}, abstract = {We present CoVeriTeam GUI, a No-Code web frontend to compose new software-verification workflows from existing analysis techniques. Verification approaches stopped relying on single techniques years ago, and instead combine selections that complement each other well. So far, such combinations were---under high implementation and maintenance cost---glued together with proprietary code. Now, CoVeriTeam GUI enables users to build new verification workflows without programming. Verification techniques can be combined through various composition operators in a drag-and-drop fashion directly in the browser, and an integration with a remote service allows to execute the built workflows with the click of a button. CoVeriTeam GUI is available open source under Apache 2.0: <a href="https://gitlab.com/sosy-lab/software/coveriteam-gui">https://gitlab.com/sosy-lab/software/coveriteam-gui</a><br> Demonstration video: <a href="https://youtu.be/oZoOARuIOuA">https://youtu.be/oZoOARuIOuA</a>}, artifact = {10.5281/zenodo.13757771}, funding = {DFG-CONVEY}, } -
CPV: A Circuit-Based Program Verifier (Competition Contribution).
In Proc. TACAS,
LNCS 14572,
pages 365-370,
2024.
Springer.
doi:10.1007/978-3-031-57256-2_22
Funding:
DFG-CONVEY
Publisher's Version
PDF
Presentation
Supplement
Artifact(s)
Abstract
We submit to SV-COMP 2024 CPV, a circuit-based software verifier for C programs. CPV utilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and k-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition, CPV achieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the category ReachSafety, it outperformed several mature software verifiers as a first-year participant. CPV manifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.BibTeX Entry
@inproceedings{CPV-TACAS24, author = {Po-Chun Chien and Nian-Ze Lee}, title = {CPV: A Circuit-Based Program Verifier (Competition Contribution)}, booktitle = {Proc.\ TACAS}, pages = {365-370}, year = {2024}, series = {LNCS~14572}, publisher = {Springer}, doi = {10.1007/978-3-031-57256-2_22}, url = {https://gitlab.com/sosy-lab/software/cpv}, pdf = {https://www.sosy-lab.org/research/pub/2024-TACAS.CPV_A_Circuit-Based_Program_Verifier_Competition_Contribution.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2024-04-08_SVCOMP_CPV_A_Circuit-Based_Program_Verifier_Po-Chun.pdf}, abstract = {We submit to SV-COMP 2024 CPV, a circuit-based software verifier for C programs. CPV utilizes sequential circuits as its intermediate representation and invokes hardware model checkers to analyze the reachability safety of C programs. As the frontend, it uses Kratos2, a recently proposed verification tool, to translate a C program to a sequential circuit. As the backend, state-of-the-art hardware model checkers ABC and AVR are employed to verify the translated circuits. We configure the hardware model checkers to run various analyses, including IC3/PDR, interpolation-based model checking, and <i>k</i>-induction. Information discovered by hardware model checkers is represented as verification witnesses. In the competition, CPV achieved comparable performance against participants whose intermediate representations are based on control-flow graphs. In the category <i>ReachSafety</i>, it outperformed several mature software verifiers as a first-year participant. CPV manifests the feasibility of sequential circuits as an alternative intermediate representation for program analysis and enables head-to-head algorithmic comparison between hardware and software verification.}, artifact = {10.5281/zenodo.10203472}, funding = {DFG-CONVEY}, } -
Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version).
Technical report 2409.02094, arXiv/CoRR,
September
2024.
doi:10.48550/arXiv.2409.02094
Funding:
DFG-COOP,
DFG-CONVEY,
DFG-IDEFIX
Publisher's Version
PDF
Presentation
Supplement
Artifact(s)
Abstract
This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php.BibTeX Entry
@techreport{TechReport24c, author = {Daniel Baier and Dirk Beyer and Po-Chun Chien and Marie-Christine Jakobs and Marek Jankola and Matthias Kettl and Nian-Ze Lee and Thomas Lemberger and Marian Lingsch-Rosenfeld and Henrik Wachowitz and Philipp Wendler}, title = {Software Verification with {CPAchecker} 3.0: {Tutorial} and User Guide (Extended Version)}, number = {2409.02094}, year = {2024}, doi = {10.48550/arXiv.2409.02094}, url = {https://cpachecker.sosy-lab.org}, presentation = {https://www.sosy-lab.org/research/prs/2024-09-10_FM24_CPAchecker_Tutorial.pdf}, abstract = {This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, <i>k</i>-induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at <a href="https://cpachecker.sosy-lab.org/doc.php">https://cpachecker.sosy-lab.org/doc.php</a>.}, annote = {This technical report is an extended version of our <a href="https://www.sosy-lab.org/research/bib/All/index.html#FM24a">paper</a> at FM 2024.}, artifact = {10.5281/zenodo.13612338}, funding = {DFG-COOP, DFG-CONVEY, DFG-IDEFIX}, institution = {arXiv/CoRR}, month = {September}, }Additional Infos
This technical report is an extended version of our paper at FM 2024. -
MoXIchecker: An Extensible Model Checker for MoXI.
Technical report 2407.15551, arXiv/CoRR,
March
2024.
doi:10.48550/arXiv.2407.15551
Funding:
DFG-CONVEY,
DFG-BRIDGE
Publisher's Version
PDF
Supplement
Artifact(s)
Abstract
MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.BibTeX Entry
@techreport{TechReport24b, author = {Salih Ates and Dirk Beyer and Po-Chun Chien and Nian-Ze Lee}, title = {{MoXIchecker}: {An} Extensible Model Checker for {MoXI}}, number = {2407.15551}, year = {2024}, doi = {10.48550/arXiv.2407.15551}, url = {https://gitlab.com/sosy-lab/software/moxichecker}, pdf = {https://arxiv.org/abs/2407.15551}, abstract = {MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.}, artifact = {10.5281/zenodo.12787654}, funding = {DFG-CONVEY,DFG-BRIDGE}, institution = {arXiv/CoRR}, month = {March}, } -
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)
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. -
Bridging Hardware and Software Formal Verification (Extended Abstract).
Technical report 2024-06, LMU Munich,
2024.
Funding:
DFG-CONVEY
PDF
Abstract
Modern technology relies heavily on the integration of hardware and software systems, from embedded devices in consumer electronics to safety-critical controllers. Despite their interdependence, the tools and methods used for verifying the correctness and reliability of these systems are often segregated, meaning that the advancement in one community cannot benefit another directly. Addressing this challenge, my dissertation aims at bridging the gap between hardware and software formal analysis. This involves translating representations of verification tasks, generating certificates for verification results, integrating state-of-the-art formal analysis tools into a cohesive framework, and adapting and combining model-checking algorithms across domains. By translating word-level hardware circuits into C programs, we found out that software analyzers were able to identify property violations that well-established hardware verifiers failed to detect. Moreover, by adopting interpolation-based hardware-verification algorithms for software analysis, we were able to tackle tasks unsolvable by existing methods. Our research consolidates knowledge from both hardware and software domains, paving a pathway for comprehensive system-level verification.BibTeX Entry
@techreport{chien:fm24-doc-symposium, author = {Po-Chun Chien}, title = {Bridging Hardware and Software Formal Verification (Extended Abstract)}, number = {2024-06}, year = {2024}, pdf = {https://www.sosy-lab.org/research/pub/2024-FM_Doctoral_Symposium.Bridging_Hardware_and_Software_Formal_Verification_Extended_Abstract.pdf}, abstract = {Modern technology relies heavily on the integration of hardware and software systems, from embedded devices in consumer electronics to safety-critical controllers. Despite their interdependence, the tools and methods used for verifying the correctness and reliability of these systems are often segregated, meaning that the advancement in one community cannot benefit another directly. Addressing this challenge, my dissertation aims at bridging the gap between hardware and software formal analysis. This involves translating representations of verification tasks, generating certificates for verification results, integrating state-of-the-art formal analysis tools into a cohesive framework, and adapting and combining model-checking algorithms across domains. By translating word-level hardware circuits into C programs, we found out that software analyzers were able to identify property violations that well-established hardware verifiers failed to detect. Moreover, by adopting interpolation-based hardware-verification algorithms for software analysis, we were able to tackle tasks unsolvable by existing methods. Our research consolidates knowledge from both hardware and software domains, paving a pathway for comprehensive system-level verification.}, annote = {An extended abstract of the dissertation project. Submitted to the Doctoral Symposium of FM 2024.}, funding = {DFG-CONVEY}, institution = {LMU Munich}, }Additional Infos
An extended abstract of the dissertation project. Submitted to the Doctoral Symposium of FM 2024.
2023
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
Analysis of Convolutions, Non-linearity and Depth in Graph Neural Networks using Neural Tangent Kernel.
Transactions on Machine Learning Research,
2023.
Funding:
DFG-CONVEY
Supplement
BibTeX Entry
@article{sabanayagam2023analysis, author = {Mahalakshmi Sabanayagam and Pascal Esser and Debarghya Ghoshdastidar}, title = {Analysis of Convolutions, Non-linearity and Depth in Graph Neural Networks using Neural Tangent Kernel}, journal = {Transactions on Machine Learning Research}, year = {2023}, url = {https://openreview.net/forum?id=xgYgDEof29}, funding = {DFG-CONVEY}, issn = {2835-8856}, note = {}, } -
Kernels, Data & Physics.
arXiv preprint arXiv:2307.02693,
2023.
Funding:
DFG-CONVEY
BibTeX Entry
@article{cagnetta2023kernels, author = {Cagnetta, Francesco and Oliveira, Deborah and Sabanayagam, Mahalakshmi and Tsilivis, Nikolaos and Kempe, Julia}, title = {Kernels, Data \& Physics}, journal = {arXiv preprint arXiv:2307.02693}, year = {2023}, funding = {DFG-CONVEY}, } -
Unveiling the Hessian's Connection to the Decision Boundary.
arXiv preprint arXiv:2306.07104,
2023.
Funding:
DFG-CONVEY
BibTeX Entry
@article{sabanayagam2023unveiling, author = {Sabanayagam, Mahalakshmi and Behrens, Freya and Adomaityte, Urte and Dawid, Anna}, title = {Unveiling the Hessian's Connection to the Decision Boundary}, journal = {arXiv preprint arXiv:2306.07104}, year = {2023}, funding = {DFG-CONVEY}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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)
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_4BibTeX 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%. <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}, } -
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)
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}, } -
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)
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}, } -
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)
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}, } -
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)
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}, } -
Improved Representation Learning Through Tensorized Autoencoders.
In International Conference on Artificial Intelligence and Statistics,
pages 8294-8307,
2023.
Funding:
DFG-CONVEY
BibTeX Entry
@inproceedings{esser2023improved, author = {Esser, Pascal and Mukherjee, Satyaki and Sabanayagam, Mahalakshmi and Ghoshdastidar, Debarghya}, title = {Improved Representation Learning Through Tensorized Autoencoders}, booktitle = {International Conference on Artificial Intelligence and Statistics}, pages = {8294--8307}, year = {2023}, funding = {DFG-CONVEY}, organization = {PMLR}, } -
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}, } -
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}, } -
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
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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)
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}, } -
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}, } -
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}, } -
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}, } -
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
-
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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}, } -
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)
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}, } -
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}, } -
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}, } -
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}, } -
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
-
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}, } -
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}, } -
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}, }
Disclaimer:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
