Deciding properties of affine loops

zbMATH Open1212.05264MaRDI QIDQ3590301FDOQ3590301

Authors: Adalbert Kovacs, Laura Kovács 

Publication date: 17 September 2010

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

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)

Cited In (8)

• Porous invariants
• Automata, Languages and Programming
• Title not available (Why is that?)
• 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

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)