Loop Analysis by Quantification over Iterations

DOI10.29007/269PzbMATH Open1415.68146OpenAlexW2906781832MaRDI QIDQ5222968FDOQ5222968

Authors: Bernhard Gleiss, Laura Kovács, Simon Robillard 

Publication date: 4 July 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL: https://research.chalmers.se/en/publication/a5609e61-7728-48ee-a104-7cd16ec1fe40

Recommendations

• Automated Technology for Verification and Analysis
• Loop Summarization and Termination Analysis
• Algebra-Based Loop Analysis
• An iterative method for generating loop invariants

zbMATH Keywords

first-order logicprogram verificationautomated reasoningterminationloopinvariant generation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (9)

• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
• On invariant synthesis for parametric systems
• Analysis of Knoop indentation
• Loop Summarization and Termination Analysis
• QuIt
• A New Algorithm for Identifying Loops in Decompilation
• Algebra-Based Loop Analysis
• Automated Technology for Verification and Analysis
• A Lightweight Approach for Loop Summarization

Uses Software

• VAMPIRE
• SMT-LIB
• TPTP
• z3
• CVC4
• InvGen

This page was built for publication: Loop Analysis by Quantification over Iterations

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