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.
(eds.): Handbook of Model Checking
8 Pith papers cite this work. Polarity classification is still indexing.
8
Pith papers citing it
verdicts
UNVERDICTED 8representative citing papers
HOA non-emptiness is NP-complete for standard acceptance conditions; inclusion is PSPACE-complete except EXPSPACE-complete for Emerson-Lei; HOG games are Pi2-complete for parity/safety and PSPACE-complete for Muller/Emerson-Lei.
Nested sequent calculi for intuitionistic grammar logics admit uniform cut-elimination via a shift rule and validity is undecidable.
The authors introduce a three-part ontology-based verification system for AI agents that generates regulatory and adversarial test scenarios and issues machine-verifiable trust certificates, with pilot results indicating improved coverage over baselines in four industries.
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
Obligation properties in LTLf+ admit a direct symbolic translation to deterministic weak automata, enabling linear-time synthesis via DWA games with effectiveness comparable to LTLf.
Provides complexity results for the constrained existence problem of five equilibrium notions in multiplayer graph games.
This survey compiles the history, awards, funding, AI integrations, and open challenges of the ESBMC model checker from 2009 to 2026.
citing papers explorer
-
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.
-
A Theory of Hanoi Omega-Automata and Games
HOA non-emptiness is NP-complete for standard acceptance conditions; inclusion is PSPACE-complete except EXPSPACE-complete for Emerson-Lei; HOG games are Pi2-complete for parity/safety and PSPACE-complete for Muller/Emerson-Lei.
-
Nested Sequents for Intuitionistic Multi-Modal Logics: Modularity, Cut-Elimination, and Undecidability
Nested sequent calculi for intuitionistic grammar logics admit uniform cut-elimination via a shift rule and validity is undecidable.
-
Toward Pre-Deployment Assurance for Enterprise AI Agents: Ontology-Grounded Simulation and Trust Certification
The authors introduce a three-part ontology-based verification system for AI agents that generates regulatory and adversarial test scenarios and issues machine-verifiable trust certificates, with pilot results indicating improved coverage over baselines in four industries.
-
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.
-
Symbolic Synthesis for LTLf+ Obligations
Obligation properties in LTLf+ admit a direct symbolic translation to deterministic weak automata, enabling linear-time synthesis via DWA games with effectiveness comparable to LTLf.
-
Equilibria in Multiplayer Graph Games: An Algorithmic Study
Provides complexity results for the constrained existence problem of five equilibrium notions in multiplayer graph games.
-
ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification
This survey compiles the history, awards, funding, AI integrations, and open challenges of the ESBMC model checker from 2009 to 2026.