Recent advances in program verification through computer algebra (Q351971)

From MaRDI portal

Jump to:navigation, search

scientific article

In more languages

Language	Label	Description	Also known as
English	Recent advances in program verification through computer algebra	scientific article

Statements

scholarly article

Recent advances in program verification through computer algebra (English)

Frontiers of Computer Science in China

publication date

4 July 2013

zbMATH Keywords

program verification

computer algebra

semi-algebraic systems solving

embedded systems

invariants

ranking functions

termination

describes a project that uses

MaRDI profile type

MaRDI publication profile

full work available at URL

https://doi.org/10.1007/s11704-009-0074-7

Synthesis of ML programs in the system Coq

Constructive versions of Tarski's fixed point theorems

A calculus of durations

The algorithmic analysis of hybrid systems

Static Analysis

Automatic Generation of Polynomial Loop Invariants

Non-linear loop invariant generation using Gröbner bases

Partial cylindrical algebraic decomposition for quantifier elimination

Verification, Model Checking, and Abstract Interpretation

Computer Aided Verification

Recent advances on determining the number of real roots of parametric polynomials

A complete algorithm for automated discovering of a class of inequality-type theorems

A complete discrimination system for polynomials

An algorithm for isolating the real solutions of semi-algebraic systems

Real solution isolation using interval arithmetic

Reachability analysis of rational eigenvalue linear systems

An axiomatic basis for computer programming

Affine relationships among variables of a program

Logical analysis of programs

The synthesis of loop predicates

Verification, Model Checking, and Abstract Interpretation

Computer Aided Verification

Precise interprocedural analysis through linear algebra

Generating all polynomial invariants in simple loops

Real quantifier elimination is doubly exponential

Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems

Verification, Model Checking, and Abstract Interpretation

Termination of Integer Linear Programs

Generating Polynomial Invariants with DISCOVERER and QEPCAD

CONCUR 2005 – Concurrency Theory

Recent advances in automated theorem proving on inequalities

Symbolic decision procedure for termination of linear programs

Deciding stability and mortality of piecewise affine dynamical systems

Termination of linear programs with nonlinear constraints

Identifiers

zbMATH Open document ID

10.1007/s11704-009-0074-7

Mathematics Subject Classification ID

zbMATH DE Number

Sitelinks

Mathematics(1 entry)

mardi Publication:351971

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q351971&oldid=35339849"