Generating Polynomial Invariants with DISCOVERER and QEPCAD

DOI10.1007/978-3-540-75221-9_4zbMath1151.68366OpenAlexW2135633055MaRDI QIDQ3526926

Bican Xia, Naijun Zhan, Yinghua Chen, Lu Yang

Publication date: 25 September 2008

Published in: Formal Methods and Hybrid Real-Time Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-75221-9_4

zbMATH Keywords

quantifier eliminationprogram verificationinvariant generationpolynomial programssemi-algebraic systemsDISCOVERERQEPCAD

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Recent advances in program verification through computer algebra ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ On invariant checking ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems ⋮ An Iterative Method for Generating Loop Invariants ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation

Uses Software

• QEPCAD
• REDLOG
• DISCOVERER

This page was built for publication: Generating Polynomial Invariants with DISCOVERER and QEPCAD