Synthesizing invariants by solving solvable loops

DOI10.1007/978-3-319-68167-2_22MaRDI QIDQ5096093zbMATH OpenOpenAlexFDO

Authors Steven de Oliveira, Saddek Bensalem, Virgile Prevosto

Publication date 12 August 2022

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1611.07753

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented in the open-source tool Pilat.

Recommendations

• Invariant Generation for P-Solvable Loops with Assignments
• Theoretical Aspects of Computing - ICTAC 2004
• A complete invariant generation approach for P-solvable loops
• Algebra-based synthesis of loops and their invariants (invited paper)
• Polynomial invariants by linear algebra

Cited in

(26)

• Loop invariant synthesis in a combined abstract domain
• Ilinva: using abduction to generate loop invariants
• Termination of polynomial loops
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Algebra-based synthesis of loops and their invariants (invited paper)
• Automatic proving or disproving equality loop invariants based on finite difference techniques
• scientific article; zbMATH DE number 1701754 (Why is no real title available?)
• Invariants synthesis over a combined domain for automated program verification
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Reasoning about loops using Vampire in KeY
• On invariant checking
• Maximal and compositional pattern-based loop invariants
• Finding polynomial loop invariants for probabilistic programs
• Loop Invariants from Counterexamples
• Automating Verification of Loops by Parallelization
• Invariant Synthesis for Combined Theories
• Valigator: A Verification Tool with Bound and Invariant Generation
• Mechanical inference of invariants for FOR-loops
• Solving invariant generation for unsolvable loops
• Algebra-Based Reasoning for Loop Synthesis
• Affine Loop Invariant Generation via Matrix Algebra
• Polynomial loops: beyond termination
• Algebraic tools for computing polynomial loop invariants
• Algebraic and algorithmic methods for computing polynomial loop invariants
• Porous invariants
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs

This page was built for publication: Synthesizing invariants by solving solvable loops

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5096093)