euforia: Complete Software Model Checking with Uninterpreted Functions
Abstract elided by the publisher.
Related papers
- Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions ESOP 2006
- Decidable verification of uninterpreted programs POPL 2019
- Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory CAV 1998
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions CAV 2002
- Hyperproperty Verification as CHC Satisfiability ESOP 2024
- Relative Completeness of Abstraction Refinement for Software Model Checking TACAS 2002
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF TACAS 2017
- Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time POPL 2020