Recent advances in program verification through computer algebra
From MaRDI portal
Publication:351971
DOI10.1007/s11704-009-0074-7zbMath1267.68099OpenAlexW2039205672MaRDI QIDQ351971
Naijun Zhan, Chaochen Zhou, Bican Xia, Lu Yang
Publication date: 4 July 2013
Published in: Frontiers of Computer Science in China (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11704-009-0074-7
invariantscomputer algebraembedded systemsterminationprogram verificationranking functionssemi-algebraic systems solving
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Generating exact nonlinear ranking functions by symbolic-numeric hybrid method ⋮ Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ Witness to non-termination of linear programs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Symbolic decision procedure for termination of linear programs
- Termination of linear programs with nonlinear constraints
- The algorithmic analysis of hybrid systems
- A complete discrimination system for polynomials
- A complete algorithm for automated discovering of a class of inequality-type theorems
- Real quantifier elimination is doubly exponential
- A calculus of durations
- Partial cylindrical algebraic decomposition for quantifier elimination
- Affine relationships among variables of a program
- Constructive versions of Tarski's fixed point theorems
- Synthesis of ML programs in the system Coq
- Recent advances on determining the number of real roots of parametric polynomials
- An algorithm for isolating the real solutions of semi-algebraic systems
- Recent advances in automated theorem proving on inequalities
- Generating all polynomial invariants in simple loops
- Real solution isolation using interval arithmetic
- Reachability analysis of rational eigenvalue linear systems
- Non-linear loop invariant generation using Gröbner bases
- Precise interprocedural analysis through linear algebra
- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
- Generating Polynomial Invariants with DISCOVERER and QEPCAD
- Logical analysis of programs
- Automatic Generation of Polynomial Loop Invariants
- The synthesis of loop predicates
- Computer Aided Verification
- Static Analysis
- An axiomatic basis for computer programming
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Termination of Integer Linear Programs
- CONCUR 2005 – Concurrency Theory
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Deciding stability and mortality of piecewise affine dynamical systems
