Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction
Abstract elided by the publisher.
Related papers
- Automatic Abstraction in SMT-Based Unbounded Software Model Checking CAV 2013
- Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration SAS 2015
- Exploiting Adjoints in Property Directed Reachability Analysis CAV 2023
- The Lattice-Theoretic Essence of Property Directed Reachability Analysis CAV 2022
- Type-base flow analysis: from polymorphic subtyping to CFL-reachability POPL 2001
- Property Directed Reachability with Extended Resolution CAV 2025
- Property-directed reachability as abstract interpretation in the monotone theory POPL 2022
- Sampling-Based Verification of CTMCs with Uncertain Rates CAV 2022