From C to Infinity and Back: Unbounded Auto-active Verification with VCC
Abstract elided by the publisher.
Related papers
- AutoProof: Auto-Active Functional Verification of Object-Oriented Programs TACAS 2015
- Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification ECOOP 2023
- On the Impact of Formal Verification on Software Development OOPSLA 2025
- The WhyRel Prototype for Modular Relational Verification of Pointer Programs TACAS 2023
- Verification of Programs with ADTs Using Shallow Horn Clauses SAS 2024
- Android Stack Machine CAV 2018
- Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting TACAS 2020
- A Two-Phase Approach for Conditional Floating-Point Verification TACAS 2021