Generating Polynomial Invariants with DISCOVERER and QEPCAD

DOI10.1007/978-3-540-75221-9_4MaRDI QIDQ3526926zbMATH OpenOpenAlexFDO

Authors Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan

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

program verificationquantifier eliminationinvariant generationpolynomial programssemi-algebraic systemsDISCOVERERQEPCAD

Mathematics Subject Classification ID

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

Recommendations

• Static Analysis
• Polynomial invariants generation of programs
• Theoretical Aspects of Computing - ICTAC 2004
• Generating all polynomial invariants in simple loops
• Polynomial invariants by linear algebra

Cited in

(11)

• On invariant checking
• Static Analysis
• Formal modelling, analysis and verification of hybrid systems
• Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
• An iterative method for generating loop invariants
• Static Analysis
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Generating invariants for non-linear loops by linear algebraic methods
• Recent advances in program verification through computer algebra
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

Describes a project that uses

Uses Software

• DISCOVERER
• REDLOG
• QEPCAD

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3526926)