TY - JOUR AU - Martini, Alfio Ricardo PY - 2020/06/18 Y2 - 2024/03/28 TI - Reasoning about Partial Correctness Assertions in Isabelle/HOL JF - Revista de Informática Teórica e Aplicada JA - RITA VL - 27 IS - 3 SE - Selected Papers - WEIT 2019 DO - 10.22456/2175-2745.98483 UR - https://seer.ufrgs.br/index.php/rita/article/view/Vol27_nr3_84 SP - 84-101 AB - <p>Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented and concurrent programs. The purpose of this work is to provide a detailed and accessible exposition of the several ways the user can conduct, explore and write proofs of correctness of sequential imperative programs with Hoare logic and the ISABELLE proof assistant. With the proof language Isar, it is possible to write structured, readable proofs that are suitable for human understanding and communication.</p> ER -