Don't care words with an application to the automata-based approach for real addition
type: Item
instance of: scholarly article
title: Don't care words with an application to the automata-based approach for real addition
zbMATH Open document ID: 1165.68393
author: Jochen Eisinger
author: Felix Klaedtke
published in: Formal Methods in System Design
publication date: 2009-07-06T00:00:00Z
full work available at URL: http://hdl.handle.net/20.500.11850/1030
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5576072
zbMATH Keywords: decision procedure
zbMATH Keywords: mixed linear arithmetic over the integers and reals
zbMATH Keywords: automata theory
zbMATH Keywords: verification of infinite-state systems
describes a project that uses: SIMPLIFY
describes a project that uses: Yices
describes a project that uses: LASH
describes a project that uses: LIRA
describes a project that uses: PHAVer
describes a project that uses: FAST
describes a project that uses: cvc3
describes a project that uses: HyTech
describes a project that uses: MONA
MaRDI profile type: Publication
OpenAlex ID: W2094939885
cites work: Computer Aided Verification
cites work: Finite presentations of infinite structures: Automata and interpretations
cites work: The Power of Hybrid Acceleration
cites work: Counting the solutions of Presburger equations without enumerating them.
cites work: Q4518891
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Weak Second‐Order Arithmetic and Finite Automata
cites work: Verifying Mixed Real-Integer Quantifier Elimination
cites work: Introduction to algorithms
cites work: Implementation and Application of Automata
cites work: Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
cites work: Simplify: a theorem prover for program checking
cites work: A mathematical introduction to logic.
cites work: A Decision Procedure for the First Order Theory of Real Addition with Order
cites work: Hybrid Systems: Computation and Control
cites work: Presburger arithmetic with unary predicates is Π11 complete
cites work: Q4503930
cites work: HyTech: A model checker for hybrid systems
cites work: Q3862379
cites work: Symbolic model checking with rich assertional languages
cites work: MONA IMPLEMENTATION SECRETS
cites work: Weak alternating automata are not that weak
cites work: Efficient minimization of deterministic weak \(\omega\)-automata
cites work: Q3141897
cites work: Alternating finite automata on \(\omega\)-words
cites work: Rocket-Fast Proof Checking for SMT Solvers
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q4055589
cites work: Q4385530
cites work: Applying Linear Quantifier Elimination
DOI: 10.1007/S10703-008-0057-6
description: scientific article; zbMATH DE number 5576072