Recent advances in program verification through computer algebra
DOI10.1007/S11704-009-0074-7zbMATH Open1267.68099OpenAlexW2039205672MaRDI QIDQ351971FDOQ351971
Authors: Lu Yang, Chaochen Zhou, Naijun Zhan, Bican Xia 
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
Recommendations
computer algebrainvariantsembedded systemsprogram verificationterminationranking functionssemi-algebraic systems solving
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- A complete algorithm for automated discovering of a class of inequality-type theorems
- Partial cylindrical algebraic decomposition for quantifier elimination
- Constructive versions of Tarski's fixed point theorems
- Title not available (Why is that?)
- Title not available (Why is that?)
- The synthesis of loop predicates
- An axiomatic basis for computer programming
- Affine relationships among variables of a program
- Reachability analysis of rational eigenvalue linear systems
- The algorithmic analysis of hybrid systems
- Computer Aided Verification
- Non-linear loop invariant generation using Gröbner bases
- Precise interprocedural analysis through linear algebra
- Automatic Generation of Polynomial Loop Invariants
- Deciding stability and mortality of piecewise affine dynamical systems
- A complete discrimination system for polynomials
- Recent advances on determining the number of real roots of parametric polynomials
- Title not available (Why is that?)
- Real quantifier elimination is doubly exponential
- A calculus of durations
- Synthesis of ML programs in the system Coq
- 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
- Title not available (Why is that?)
- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
- Generating Polynomial Invariants with DISCOVERER and QEPCAD
- Logical analysis of programs
- Title not available (Why is that?)
- Symbolic decision procedure for termination of linear programs
- Static Analysis
- 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
- Termination of linear programs with nonlinear constraints
Cited In (17)
- Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
- A computer checked algebraic verification of a distributed summation algorithm
- Algebraic program analysis
- Formal modelling, analysis and verification of hybrid systems
- Discovering non-terminating inputs for multi-path polynomial programs
- Witness to non-termination of linear programs
- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
- Title not available (Why is that?)
- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- Verification, Model Checking, and Abstract Interpretation
- Title not available (Why is that?)
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
- Problem-oriented verification system and its application to linear algebra programs
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- Title not available (Why is that?)
- Algebraic implementations preserve program correctness
Uses Software
This page was built for publication: Recent advances in program verification through computer algebra
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q351971)
