Automatic generation of non-linear loop invariants

DOI10.3724/SP.J.1087.2008.01854MaRDI QIDQ3646570zbMATH OpenFDO

Authors Zhongqin Bi, Zhenbing Zeng, Yuan-Hua Guo

Publication date 22 November 2009

Published in Journal of Computer Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3724/SP.J.1087.2008.01854

zbMATH Keywords

constraint solving problemloop invariantprogram verificationtransition system

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Automated generation of non-linear loop invariants utilizing hypergeometric sequences
• Generating invariants for non-linear loops by linear algebraic methods
• Automatic generation of invariants and intermediate assertions
• An iterative method for generating loop invariants
• Automatically inferring loop invariants via algorithmic learning
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Automatic Generation of Polynomial Loop Invariants
• Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
• Ilinva: using abduction to generate loop invariants
• Non-linear loop invariant generation using Gröbner bases

Cited in

(16)

• scientific article; zbMATH DE number 1617317 (Why is no real title available?)
• SMT-based array invariant generation
• Finding positively invariant sets of a class of nonlinear loops via curve fitting
• An iterative method for generating loop invariants
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Non-linear loop invariant generation using Gröbner bases
• Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction
• Maximal and compositional pattern-based loop invariants
• The derivation and formal proof of binary tree sorting non-recursive algorithm
• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
• Automated generation of non-linear loop invariants utilizing hypergeometric sequences
• Programming Languages and Systems
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Automatically inferring loop invariants via algorithmic learning
• Computer Aided Verification
• Generating invariants for non-linear loops by linear algebraic methods

Describes a project that uses

Uses Software

• Maple

This page was built for publication: Automatic generation of non-linear loop invariants

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