Hoare-style logic for unstructured programs

DOI10.1007/978-3-030-58768-0_11zbMath1476.68064OpenAlexW3086076508MaRDI QIDQ2038040

Mads Dam, Roberto Guanciale, Andreas Lindner, Didrik Lundberg

Publication date: 8 July 2021

Full work available at URL: http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-281691

zbMATH Keywords

theorem provingformal verificationbinary analysisHoare logicprogram logics

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Loop verification with invariants and contracts ⋮ HolBA

Uses Software

• HOL
• CakeML
• seL4
• ARMor
• BoogiePL
• Cloc
• TrABin

This page was built for publication: Hoare-style logic for unstructured programs