A versatile concept for the analysis of loops

DOI10.1016/j.jlap.2012.04.001zbMath1246.68094MaRDI 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 function; weakest precondition; invariant assertion; invariant relation; loop functions; loop semantics; strongest postcondition; termination condition; while loop

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

03B70: Logic in computer science

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

Related Items

Convergence: integrating termination and abort-freedom

Uses Software

• Mathematica
• FLATA
• Daikon
• LOOPUS

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item