Don't care words with an application to the automata-based approach for real addition
From MaRDI portal
Publication:1028730
DOI10.1007/s10703-008-0057-6zbMath1165.68393OpenAlexW2094939885MaRDI QIDQ1028730
Jochen Eisinger, Felix Klaedtke
Publication date: 6 July 2009
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/20.500.11850/1030
automata theoryverification of infinite-state systemsdecision proceduremixed linear arithmetic over the integers and reals
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Uses Software
Cites Work
- Alternating finite automata on \(\omega\)-words
- Counting the solutions of Presburger equations without enumerating them.
- Isabelle/HOL. A proof assistant for higher-order logic
- Efficient minimization of deterministic weak \(\omega\)-automata
- Finite presentations of infinite structures: Automata and interpretations
- HyTech: A model checker for hybrid systems
- MONA IMPLEMENTATION SECRETS
- Applying Linear Quantifier Elimination
- Weak Second‐Order Arithmetic and Finite Automata
- Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
- Simplify: a theorem prover for program checking
- Weak alternating automata are not that weak
- Verifying Mixed Real-Integer Quantifier Elimination
- Presburger arithmetic with unary predicates is Π11 complete
- A Decision Procedure for the First Order Theory of Real Addition with Order
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Rocket-Fast Proof Checking for SMT Solvers
- Implementation and Application of Automata
- Hybrid Systems: Computation and Control
- Computer Aided Verification
- The Power of Hybrid Acceleration
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Symbolic model checking with rich assertional languages
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
