A sound calculus for extensional arrays with constant default values works for finite and infinite index domains and is implemented in Bitwuzla.
In: Biere, A., Bloem, R
9 Pith papers cite this work, alongside 16 external citations. Polarity classification is still indexing.
9
Pith papers citing it
16
external citations · OpenAlex
representative citing papers
Coverability for order-k nested reset counter systems is F_Ωk-complete.
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 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.
ESBMC-LLB exposes function-block-hidden ladder logic bombs as safety violations, proves bomb-absence unboundedly, and synthesizes detonation triggers on public PLC benchmarks.
A parallel SMT framework using VSIDS-guided dynamic partitioning, core-guided backjumping, and online backbone detection reports the largest average solved-instance gain across six SMT-COMP 2025 logics.
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.
citing papers explorer
-
Satisfiability Modulo Extensional Constant Arrays (Extended Version)
A sound calculus for extensional arrays with constant default values works for finite and infinite index domains and is implemented in Bitwuzla.
-
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.
-
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.
-
Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
ESBMC-LLB exposes function-block-hidden ladder logic bombs as safety violations, proves bomb-absence unboundedly, and synthesizes detonation triggers on public PLC benchmarks.
-
Parallel SMT Solving via Dynamic Partitioning, Core-Guided Pruning, and Backbone Detection
A parallel SMT framework using VSIDS-guided dynamic partitioning, core-guided backjumping, and online backbone detection reports the largest average solved-instance gain across six SMT-COMP 2025 logics.
-
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.