A versatile concept for the analysis of loops

DOI10.1016/j.jlap.2012.04.001zbMath1246.68094OpenAlexW2029961359MaRDI QIDQ444373

Khaled Bsaies, Asma Louhichi, Lamia Labed Jilani, Olfa Mraihi, Wided Ghardallou, Ali Milli

Publication date: 14 August 2012

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2012.04.001

zbMATH Keywords

invariant functionweakest preconditioninvariant assertioninvariant relationloop functionsloop semanticsstrongest postconditiontermination conditionwhile loop

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Convergence: integrating termination and abort-freedom

Uses Software

• Mathematica
• FLATA
• Daikon
• LOOPUS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strongest invariant functions: Their use in the systematic analysis of while statements
• Mathematics for reasoning about loop functions
• On the lattice of specifications: Applications to a specification methodology
• The Daikon system for dynamic detection of likely invariants
• Computing Preconditions and Postconditions of While Loops
• Proving Conditional Termination
• Inferring Loop Invariants Using Postconditions
• Programming as a Discipline of Mathematical Nature
• The verified software initiative
• An axiomatic basis for computer programming
• Proof automation for functional correctness in separation logic

This page was built for publication: A versatile concept for the analysis of loops