Loop verification with invariants and contracts

DOI10.1007/978-3-030-94583-1_4zbMath1498.68074arXiv2010.05812MaRDI QIDQ2152642

Gidon Ernst

Publication date: 8 July 2022

Full work available at URL: https://arxiv.org/abs/2010.05812

zbMATH Keywords

invariants; loops; contracts; program verification

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

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

Uses Software

• Dafny
• Isabelle/HOL
• CIRC
• CPAchecker
• Leon
• RGITL
• GNATprove
• SeaHorn
• HolBA