Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic
No abstract available.
Related papers
- Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results TOPLAS 1999
- Parikh's Theorem Made Symbolic POPL 2024
- Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic VMCAI 2019
- Weakly Acyclic Diagrams: A Data Structure for Infinite-State Symbolic Verification TACAS 2025
- Context-Free-Language Reachability for Almost-Commuting Transition Systems POPL 2026
- Fairness for Infinite-State Systems TACAS 2015
- FPL: fast Presburger arithmetic through transprecision OOPSLA 2021
- Verifying Infinite State Processes with Sequential and Parallel Composition POPL 1995