Loop Analysis by Quantification over Iterations

DOI10.29007/269PMaRDI QIDQ5222968zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

automated reasoningfirst-order logicinvariant generationloopprogram verificationtermination

Mathematics Subject Classification ID

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

Recommendations

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

Cited in

(9)

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

Describes a project that uses

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)