Affine Loop Invariant Generation via Matrix Algebra

DOI10.1007/978-3-031-13185-1_13MaRDI QIDQ6487319zbMATH OpenFDO

Authors Yucheng Ji, Hongfei Fu, Bin Fang, Haibo Chen

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-13185-1_13

Mathematics Subject Classification ID

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

Recommendations

• Automatic Generation of Polynomial Loop Invariants
• Synthesizing invariants by solving solvable loops
• Deciding properties of affine loops
• Generating invariants for non-linear loops by linear algebraic methods
• Invariant generation for multi-path loops with polynomial assignments

Cites work

• A data driven approach for algebraic loop invariants
• Affine Loop Invariant Generation via Matrix Algebra
• Algebra-based synthesis of loops and their invariants (invited paper)
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Computer Aided Verification
• Computing real roots of real polynomials
• Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
• From invariant checking to invariant inference using randomized search
• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Non-polynomial worst-case analysis of recursive programs
• Nonlinear Craig interpolant generation
• Refining and compressing abstract domains
• Solving systems of linear equations over polynomials
• Static Analysis
• Static Analysis
• Synthesis of circular compositional program proofs via abduction
• Synthesizing invariants by solving solvable loops
• Temporal verification of reactive systems: response
• The polyhedron-hitting problem

Cited in

(3)

• Invariant and type inference for matrices
• Affine Loop Invariant Generation via Matrix Algebra
• Invariant relations for affine loops

Describes a project that uses

Uses Software

• SageMath

This page was built for publication: Affine Loop Invariant Generation via Matrix Algebra

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