Real World Verification
From MaRDI portal
Publication:5191121
DOI10.1007/978-3-642-02959-2_35zbMath1250.68197OpenAlexW1565786776MaRDI QIDQ5191121
Jan-David Quesel, André Platzer, Philipp Rümmer
Publication date: 28 July 2009
Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_35
Related Items
A heuristic prover for real inequalities, SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Sharper and Simpler Nonlinear Interpolants for Program Verification, Pegasus: sound continuous invariant generation, Bellerophon: tactical theorem proving for hybrid systems, Solving quantified linear arithmetic by counterexample-guided instantiation, Local Search For Satisfiability Modulo Integer Arithmetic Theories, Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition, Using machine learning to improve cylindrical algebraic decomposition, Real World Verification, $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation, Satisfiability checking and symbolic computation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Differential dynamic logic for hybrid systems
- Real quantifier elimination is doubly exponential
- Partial cylindrical algebraic decomposition for quantifier elimination
- A new approach for automatic theorem proving in real geometry
- Semidefinite programming relaxations for semialgebraic problems
- Cylindrical algebraic decomposition using validated numerics
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Computing Differential Invariants of Hybrid Systems as Fixedpoints
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Linear Quantifier Elimination
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Aligator: A Mathematica Package for Invariant Generation (System Description)
- CSDP, A C library for semidefinite programming
- QEPCAD B
- Real World Verification
- Efficient solving of quantified inequality constraints over the real numbers
- Computer Science Logic
- Automated Deduction – CADE-20
- Correct Hardware Design and Verification Methods
