A sound calculus for extensional arrays with constant default values works for finite and infinite index domains and is implemented in Bitwuzla.
(eds.): Handbook of Model Checking
9 Pith papers cite this work, alongside 699 external citations. Polarity classification is still indexing.
9
Pith papers citing it
699
external citations · OpenAlex
representative 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.
Memoryless randomised subgame-perfect equilibria always exist for turn-based deterministic games with reachability, safety, and 0-2 Muller objectives, and can be constructed in polynomial time.
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 sound calculus for extensional arrays with constant default values works for finite and infinite index domains and is implemented 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.
-
Simple Nash Equilibria for Qualitative Multiplayer Games
Memoryless randomised subgame-perfect equilibria always exist for turn-based deterministic games with reachability, safety, and 0-2 Muller objectives, and can be constructed in polynomial time.
-
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.