Deciding properties of affine loops

MaRDI QIDQ3590301zbMATH OpenFDO

Authors Adalbert Kovacs, Laura Kovács

Publication date 17 September 2010

zbMATH Keywords

program verificationloop invariantssymbolic summationpolynomial relations\texttt{Aligator}

Mathematics Subject Classification ID

Algebraic combinatorics (05E99) Computational aspects in algebraic geometry (14Q99) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Aligator: A Mathematica Package for Invariant Generation (System Description)
• Automatic Generation of Polynomial Loop Invariants
• Invariant Generation for P-Solvable Loops with Assignments
• Generating all polynomial invariants in simple loops
• Polynomial invariants by linear algebra

Cited in

(8)

• Porous invariants
• Automata, Languages and Programming
• scientific article; zbMATH DE number 5183795 (Why is no real title available?)
• Aligator: A Mathematica Package for Invariant Generation (System Description)
• Algebra-Based Loop Synthesis
• Aligator.jl -- a Julia package for loop invariant generation
• Affine Loop Invariant Generation via Matrix Algebra
• Decidability of affine solution problems

Describes a project that uses

Uses Software

• Aligator

This page was built for publication: Deciding properties of affine loops

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