Checking System Properties via Integer Programming
Abstract elided by the publisher.
Related papers
- Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results TOPLAS 1999
- Higher-Order Property-Directed Reachability ICFP 2023
- Fairness for Infinite-State Systems TACAS 2015
- HFL(Z) Validity Checking for Automated Program Verification POPL 2023
- Space-Efficient Manifest Contracts POPL 2015
- The Golem Horn Solver CAV 2023
- Predicate abstraction and CEGAR for higher-order model checking PLDI 2011
- Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking) TACAS 2026