Coverability for order-k nested reset counter systems is F_Ωk-complete.
In: Biere, A., Bloem, R
5 Pith papers cite this work, alongside 16 external citations. Polarity classification is still indexing.
5
Pith papers citing it
16
external citations · Crossref
representative citing papers
A novel decision procedure for arrays with constant arrays in SMT, supporting any index domain with an abstract calculus, soundness proofs, and implementation in Bitwuzla.
A verification technique for infinite-state systems learns transitive relations via recurrence analysis and projections to achieve finite diameter, enabling safety proofs through bounded-step reachability checks.
CSF is the first separation logic-based concolic testing engine for heap-manipulating programs that integrates specification-based testing to generate valid inputs with high coverage.
citing papers explorer
-
The Complexity of Nested Reset Counter Systems
Coverability for order-k nested reset counter systems is F_Ωk-complete.
-
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
A novel decision procedure for arrays with constant arrays in SMT, supporting any index domain with an abstract calculus, soundness proofs, and implementation in Bitwuzla.
-
Infinite State Model Checking by Learning Transitive Relations
A verification technique for infinite-state systems learns transitive relations via recurrence analysis and projections to achieve finite diameter, enabling safety proofs through bounded-step reachability checks.
-
Concolic Testing Heap-Manipulating Programs
CSF is the first separation logic-based concolic testing engine for heap-manipulating programs that integrates specification-based testing to generate valid inputs with high coverage.
- Verification of Configurable SRA Systems