Loop Analysis by Quantification over Iterations

DOI10.29007/269pzbMath1415.68146OpenAlexW2906781832MaRDI QIDQ5222968

Simon Robillard, Laura Kovács, Bernhard Gleiss

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

first-order logicautomated reasoningloopterminationprogram verificationinvariant generation

Mathematics Subject Classification ID

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

Related Items (2)

On invariant synthesis for parametric systems ⋮ QuIt

Uses Software

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

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