MONA IMPLEMENTATION SECRETS
From MaRDI portal
Publication:3021971
DOI10.1142/S012905410200128XzbMath1066.68079OpenAlexW1987469449MaRDI QIDQ3021971
Anders Møller, Nils Klarlund, Michael I. Schwartzbach
Publication date: 22 June 2005
Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1142/s012905410200128x
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
A symbolic decision procedure for symbolic alternating finite automata ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Logic programming approach to automata-based decision procedures ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ Symbolic tree automata ⋮ Nested antichains for WS1S ⋮ Certifying proofs in the first-order theory of rewriting ⋮ Lazy Automata Techniques for WS1S ⋮ Minimization of Visibly Pushdown Automata Using Partial Max-SAT ⋮ Automata-based symbolic string analysis for vulnerability detection ⋮ Bounded treewidth as a key to tractability of knowledge representation and reasoning ⋮ Ehrenfeucht-Fraïssé goes automatic for real addition ⋮ Monitoring Metric First-Order Temporal Properties ⋮ Language-Based Abstraction Refinement for Hybrid System Verification ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ An Evaluation of Automata Algorithms for String Analysis ⋮ Deciding Monadic Second Order Logic over $$\omega $$ ω -Words by Specialized Finite Automata ⋮ MONA ⋮ PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ Turning decision procedures into disprovers ⋮ Relativizations for the logic-automata connection
Cites Work
