Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

DOI10.1007/s11704-014-3150-6zbMath1425.68260OpenAlexW1982538489MaRDI QIDQ2418665

Yanyan Li

Publication date: 28 May 2019

Published in: Frontiers of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11704-014-3150-6

zbMATH Keywords

semidefinite programmingsymbolic computationsum-of-squares relaxationtotal correctnessprecondition generation

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Semidefinite programming (90C22) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Sharper and Simpler Nonlinear Interpolants for Program Verification

Uses Software

• Sostools
• SeDuMi
• YALMIP
• DISCOVERER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Recent advances in program verification through computer algebra
• Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
• Symbolic decision procedure for termination of linear programs
• Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients
• Efficient weakest preconditions
• Generating all polynomial invariants in simple loops
• Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients
• Generating Non-linear Interpolants by Semidefinite Programming
• Non-linear loop invariant generation using Gröbner bases
• Proving Conditional Termination
• Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• Using SeDuMi 1.02, A Matlab toolbox for optimization over symmetric cones
• Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars
• Static Analysis
• An axiomatic basis for computer programming
• Theoretical Aspects of Computing - ICTAC 2004
• Verification, Model Checking, and Abstract Interpretation
• Static Analysis
• CONCUR 2005 – Concurrency Theory
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Partial correctness for probabilistic demonic programs