Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure

DOI10.1007/978-3-030-29436-6_18OpenAlexW2969578428MaRDI QIDQ5919501

Lukáš Holík, Ondřej Lengál, Tomáš Vojnar, Vojtěch Havlena

Publication date: 10 March 2020

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1905.08697

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure

Uses Software

• FMona
• MONA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Array theory of bounded elements and its applications
• Forest automata for verification of heap manipulation
• MONA IMPLEMENTATION SECRETS
• Lazy Automata Techniques for WS1S
• Antichain Algorithms for Finite Automata
• When Simulation Meets Antichains
• New Algorithm for Weak Monadic Second-Order Logic on Inductive Structures
• Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Nested Antichains for WS1S
• An Efficient Decision Procedure for Imperative Tree Data Structures
• Minimization of symbolic automata
• Decidable logics combining heap structures and data
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Hybrid Systems: Computation and Control
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure

This page was built for publication: Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure