Coverability for order-k nested reset counter systems is F_Ωk-complete.
In: Biere, A., Bloem, R
8 Pith papers cite this work, alongside 16 external citations. Polarity classification is still indexing.
8
Pith papers citing it
16
external citations · Crossref
verdicts
UNVERDICTED 8representative citing papers
For fixed-dimensional continuous VASS with rational transition vectors, all eight variants of reachability and coverability are in AC^1 for dimension 1 and NP-complete for dimension at least 2.
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.
Contract-based approach with Dafny verifies correctness of every legal instantiation of configurable SRA systems.
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
Presents a dynamic partitioning parallel SMT framework with core-guided pruning and backbone detection that outperforms sequential Z3 and prior parallel solvers on SMT-COMP 2025 benchmarks across six logics.
citing papers explorer
-
The Complexity of Nested Reset Counter Systems
Coverability for order-k nested reset counter systems is F_Ωk-complete.
-
Reachability in Fixed-Dimensional Continuous VASS
For fixed-dimensional continuous VASS with rational transition vectors, all eight variants of reachability and coverability are in AC^1 for dimension 1 and NP-complete for dimension at least 2.
-
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
Contract-based approach with Dafny verifies correctness of every legal instantiation of configurable SRA systems.
-
Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
-
Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Online Backbone Detection
Presents a dynamic partitioning parallel SMT framework with core-guided pruning and backbone detection that outperforms sequential Z3 and prior parallel solvers on SMT-COMP 2025 benchmarks across six logics.