Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification

DOI10.1007/978-3-031-16681-5_17OpenAlexW4296118746MaRDI QIDQ6160567

David E. Narváez, Edith Hemaspaandra

Publication date: 2 June 2023

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

Full work available at URL: https://doi.org/10.1007/978-3-031-16681-5_17

zbMATH Keywords

formal methodsfinite automataQBFIsabelle/HOLinteractive theorem provingQSAT

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The state complexities of some basic operations on regular languages
• Circuit-based search space pruning in QBF
• Dependency learning for QBF
• State complexity of some operations on binary regular languages
• Formally verifying the solution to the Boolean Pythagorean triples problem
• Relationships between nondeterministic and deterministic tape complexities
• Non-prenex QBF Solving Using Abstraction
• Compressing BMC Encodings with QBF
• Checking NFA equivalence with bisimulations up to congruence
• Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• A Unified Proof System for QBF Preprocessing
• A First Step Towards a Unified Proof Checker for QBF
• Decidability and Shortest Strings in Formal Languages
• Experimental Evaluation of Classical Automata Constructions
• On the Bounds for State-Set Size in the Proofs of Equivalence Between Deterministic, Nondeterministic, and Two-Way Finite Automata
• NONDETERMINISTIC DESCRIPTIONAL COMPLEXITY OF REGULAR LANGUAGES

This page was built for publication: Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification