A sound and relatively complete translation of CTL* verification and synthesis problems for reactive programs into existential Horn clauses.
Modular primal-dual fixpoint logic solving for temporal verification
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
fields
cs.LO 2verdicts
UNVERDICTED 2representative citing papers
MoAT reduces LTL model checking of infinite state systems to fair termination via automata-based approach and calls KoAT/LoAT, matching state-of-the-art performance in experiments.
citing papers explorer
-
CTL* Verification and Synthesis using Existential Horn Clauses
A sound and relatively complete translation of CTL* verification and synthesis problems for reactive programs into existential Horn clauses.
-
Verifying LTL for Infinite State Systems via Termination Analysis
MoAT reduces LTL model checking of infinite state systems to fair termination via automata-based approach and calls KoAT/LoAT, matching state-of-the-art performance in experiments.