Recent advances in program verification through computer algebra
type: Item
instance of: scholarly article
title: Recent advances in program verification through computer algebra
zbMATH Open document ID: 1267.68099
author: Lu Yang
author: Chaochen Zhou
author: Naijun Zhan
author: Bican Xia
published in: Frontiers of Computer Science in China
publication date: 2013-07-04T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6183802
zbMATH Keywords: program verification
zbMATH Keywords: computer algebra
zbMATH Keywords: semi-algebraic systems solving
zbMATH Keywords: embedded systems
zbMATH Keywords: invariants
zbMATH Keywords: ranking functions
zbMATH Keywords: termination
describes a project that uses: QEPCAD
describes a project that uses: Isabelle/HOL
describes a project that uses: PVS
describes a project that uses: DISCOVERER
MaRDI profile type: Publication
full work available at URL: s11704-009-0074-7
OpenAlex ID: W2039205672
cites work: Q3703299
cites work: Q3940830
cites work: Synthesis of ML programs in the system Coq
cites work: Constructive versions of Tarski's fixed point theorems
cites work: A calculus of durations
cites work: The algorithmic analysis of hybrid systems
cites work: Static Analysis
cites work: Automatic Generation of Polynomial Loop Invariants
cites work: Non-linear loop invariant generation using Gröbner bases
cites work: Partial cylindrical algebraic decomposition for quantifier elimination
cites work: Verification, Model Checking, and Abstract Interpretation
cites work: Computer Aided Verification
cites work: Recent advances on determining the number of real roots of parametric polynomials
cites work: A complete algorithm for automated discovering of a class of inequality-type theorems
cites work: A complete discrimination system for polynomials
cites work: An algorithm for isolating the real solutions of semi-algebraic systems
cites work: Real solution isolation using interval arithmetic
cites work: Reachability analysis of rational eigenvalue linear systems
cites work: Q5584402
cites work: An axiomatic basis for computer programming
cites work: Affine relationships among variables of a program
cites work: Logical analysis of programs
cites work: The synthesis of loop predicates
cites work: Q4411947
cites work: Precise interprocedural analysis through linear algebra
cites work: Generating all polynomial invariants in simple loops
cites work: Real quantifier elimination is doubly exponential
cites work: Q2769578
cites work: Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
cites work: Termination of Integer Linear Programs
cites work: Generating Polynomial Invariants with DISCOVERER and QEPCAD
cites work: CONCUR 2005 – Concurrency Theory
cites work: Recent advances in automated theorem proving on inequalities
cites work: Symbolic decision procedure for termination of linear programs
cites work: Deciding stability and mortality of piecewise affine dynamical systems
cites work: Termination of linear programs with nonlinear constraints
DOI: 10.1007/S11704-009-0074-7
description: scientific article; zbMATH DE number 6183802