Endomorphisms for Non-trivial Non-linear Loop Invariant Generation

DOI10.1007/978-3-540-85762-4_29zbMath1161.68389OpenAlexW1532216203MaRDI QIDQ5505618

Nadir Matringe, Rachid Rebiha, Arnaldo Vieira Moura

Publication date: 27 January 2009

Published in: Theoretical Aspects of Computing - ICTAC 2008 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-85762-4_29

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Generating invariants for non-linear loops by linear algebraic methods ⋮ Morphisms for Non-trivial Non-linear Invariant Generation for Algebraic Hybrid Systems ⋮ Endomorphisms for Non-trivial Non-linear Loop Invariant Generation ⋮ Generating invariants for non-linear hybrid systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Generating all polynomial invariants in simple loops
• Non-linear loop invariant generation using Gröbner bases
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• Abstract interpretation and application to logic programs
• Reasoning Algebraically About P-Solvable Loops
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Verification, Model Checking, and Abstract Interpretation