Recent advances in program verification through computer algebra
From MaRDI portal
(Redirected from Publication:351971)
Recommendations
Cites work
- A calculus of durations
- A complete algorithm for automated discovering of a class of inequality-type theorems
- A complete discrimination system for polynomials
- Affine relationships among variables of a program
- An algorithm for isolating the real solutions of semi-algebraic systems
- An axiomatic basis for computer programming
- Automatic Generation of Polynomial Loop Invariants
- Computer Aided Verification
- Computer Aided Verification
- CONCUR 2005 – Concurrency Theory
- Constructive versions of Tarski's fixed point theorems
- Deciding stability and mortality of piecewise affine dynamical systems
- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
- Generating all polynomial invariants in simple loops
- Generating Polynomial Invariants with DISCOVERER and QEPCAD
- scientific article; zbMATH DE number 1701751 (Why is no real title available?)
- scientific article; zbMATH DE number 3930354 (Why is no real title available?)
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 1948385 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- Logical analysis of programs
- Non-linear loop invariant generation using Gröbner bases
- Partial cylindrical algebraic decomposition for quantifier elimination
- Precise interprocedural analysis through linear algebra
- Reachability analysis of rational eigenvalue linear systems
- Real quantifier elimination is doubly exponential
- Real solution isolation using interval arithmetic
- Recent advances in automated theorem proving on inequalities
- Recent advances on determining the number of real roots of parametric polynomials
- Static Analysis
- Symbolic decision procedure for termination of linear programs
- Synthesis of ML programs in the system Coq
- Termination of Integer Linear Programs
- Termination of linear programs with nonlinear constraints
- The algorithmic analysis of hybrid systems
- The synthesis of loop predicates
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
Cited in
(18)- Using computer algebra techniques for the specification, verification and synthesis of recursive programs
- Algebraic implementations preserve program correctness
- Problem-oriented verification system and its application to linear algebra programs
- Discovering non-terminating inputs for multi-path polynomial programs
- Witness to non-termination of linear programs
- Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
- A computer checked algebraic verification of a distributed summation algorithm
- Formal modelling, analysis and verification of hybrid systems
- Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
- Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
- scientific article; zbMATH DE number 524110 (Why is no real title available?)
- scientific article; zbMATH DE number 1497749 (Why is no real title available?)
- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
- scientific article; zbMATH DE number 2217740 (Why is no real title available?)
- Verification, Model Checking, and Abstract Interpretation
- Proving an execution of an algorithm correct?
- Algebraic program analysis
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)
