Generating invariants for non-linear loops by linear algebraic methods

DOI10.1007/S00165-015-0333-3MaRDI QIDQ903492zbMATH OpenOpenAlexFDO

Authors Rachid Rebiha, Arnaldo Vieira Moura, Nadir Matringe

Publication date 6 January 2016

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-015-0333-3

zbMATH Keywords

linear algebraformal methodsinvariant generation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• Non-linear loop invariant generation using Gröbner bases
• Automatic generation of non-linear loop invariants
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Automated generation of non-linear loop invariants utilizing hypergeometric sequences
• Polynomial invariants by linear algebra

Cites work

• scientific article; zbMATH DE number 1617317 (Why is no real title available?)
• scientific article; zbMATH DE number 1703931 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1140679 (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?)
• A new efficient algorithm for computing Gröbner bases \((F_4)\)
• Abstract interpretation and application to logic programs
• An axiomatic basis for computer programming
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Constraint-Based Approach for Analysis of Hybrid Systems
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Generating Box Invariants
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• Generating all polynomial invariants in simple loops
• Generating invariants for non-linear hybrid systems by linear algebraic methods
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Lagrange resolvents
• Non-linear loop invariant generation using Gröbner bases
• Programming Languages and Systems
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Reasoning Algebraically About P-Solvable Loops
• SAGE
• Temporal verification of reactive systems: response
• Verification, Model Checking, and Abstract Interpretation

Cited in

(10)

• Non-linear loop invariant generation using Gröbner bases
• Nonlinear invariants for linear loops and eigenpolynomials of linear operators
• Computer Aided Verification
• A deductive approach towards reasoning about algebraic transition systems
• Affine Loop Invariant Generation via Matrix Algebra
• Automatic generation of non-linear loop invariants
• scientific article; zbMATH DE number 1617317 (Why is no real title available?)
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Automated generation of non-linear loop invariants utilizing hypergeometric sequences
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)

Describes a project that uses

Uses Software

• SageMath

This page was built for publication: Generating invariants for non-linear loops by linear algebraic methods

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