Verification and synthesis using real quantifier elimination
From MaRDI portal
Publication:5254190
DOI10.1145/1993886.1993935zbMath1323.68385OpenAlexW2131395649MaRDI QIDQ5254190
Thomas Sturm, Ashish Kumar Tiwari
Publication date: 9 June 2015
Published in: Proceedings of the 36th international symposium on Symbolic and algebraic computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1993886.1993935
Symbolic computation and algebraic computation (68W30) Application models in control theory (93C95) Specification and verification (program logics, model checking, etc.) (68Q60) Quantifier elimination, model completeness, and related topics (03C10)
Related Items (14)
Pegasus: sound continuous invariant generation ⋮ Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems ⋮ An efficient framework for barrier certificate generation of uncertain nonlinear hybrid systems ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Exact safety verification of hybrid systems using sums-of-squares representation ⋮ Synthesizing ReLU neural networks with two hidden layers as barrier certificates for hybrid systems ⋮ Better answers to real questions ⋮ A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications ⋮ Efficient solution of a class of quantified constraints with quantifier prefix exists-forall ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Automatic generation of bounds for polynomial systems with application to the Lorenz system ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ A Roadmap to Decidability
Uses Software
This page was built for publication: Verification and synthesis using real quantifier elimination
