scholarly journals KAT and PHL in Coq

2008 ◽  
Vol 5 (2) ◽  
pp. 137-160 ◽  
Author(s):  
David Pereira ◽  
Nelma Moreira
Keyword(s):  
Program Verification ◽  
Theorem Prover ◽  
Hoare Logic ◽  
Automatic Production ◽  
Kleene Algebra ◽  
Source Level ◽  
Deduction Rules

In this article we describe an implementation of Kleene algebra with tests (KAT) in the Coq theorem prover. KAT is an equational system that has been successfully applied in program verification and, in particular, it subsumes the propositional Hoare logic (PHL). We also present an PHL encoding in KAT, by deriving its deduction rules as theorems of KAT. Some examples of simple program's formal correctness are given. This work is part of a study of the feasibility of using KAT in the automatic production of certificates in the context of (source-level) Proof-Carrying-Code (PCC). .

scholarly journals Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL

2021 ◽  
Author(s):  
Sadegh Dalvandi ◽  
Brijesh Dongol ◽  
Simon Doherty ◽  
Heike Wehrheim
Keyword(s):  
Program Verification ◽  
Memory Models ◽  
Theorem Prover ◽  
Hoare Logic ◽  
Deductive Verification ◽  
High Level

AbstractWeak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki–Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g. reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by introducing the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto’s encoding of Owicki–Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson’s algorithm and a read–copy–update algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.

scholarly journals AN EMPIRICAL EVALUATION OF AUTOMATED THEOREM PROVERS IN SOFTWARE CERTIFICATION

2006 ◽  
Vol 15 (01) ◽  
pp. 81-107 ◽  
Author(s):  
EWEN DENNEY ◽  
BERND FISCHER ◽  
JOHANN SCHUMANN
Keyword(s):  
System Architecture ◽  
High Performance ◽  
Program Verification ◽  
Source Code ◽  
Empirical Evaluation ◽  
Theorem Prover ◽  
Safety Properties ◽  
Proof Checking ◽  
First Order ◽  
The Individual

We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, traceability, and usability, and describe the resulting system architecture, including a certification browser that maintains and displays links between obligations and source code locations. For full automation, the obligations must be aggressively preprocessed and simplified, and we demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATPs to solve the proof tasks. Our results are based on 13 comprehensive certification experiments that lead to 366 top-level safety obligations and ultimately to more than 25,000 proof tasks which have been used to determine the suitability of the high-performance provers DCTP, E-Setheo, E, Gandalf, Otter, Setheo, Spass, and Vampire, and our associated infrastructure. The proofs found by Otter have been checked by Ivy.

scholarly journals On incorrectness logic and Kleene algebra with top and tests

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-30
Author(s):  
Cheng Zhang ◽  
Arthur Azevedo de Amorim ◽  
Marco Gaboardi
Keyword(s):  
Equational Theory ◽  
Program Transformations ◽  
Hoare Logic ◽  
Compiler Optimizations ◽  
Partial Correctness ◽  
Seminal Work ◽  
Kleene Algebra

Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O'Hearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.

KAT-ML: an interactive theorem prover for Kleene algebra with tests

2006 ◽  
Vol 16 (1-2) ◽  
pp. 9-33 ◽  
Author(s):  
Kamal Aboul-Hosn ◽  
Dexter Kozen
Keyword(s):  
Theorem Prover ◽  
Kleene Algebra

scholarly journals Formal Replay of Translation Validation for Highly Optimised C

10.29007/dw2m ◽  
2018 ◽  
Author(s):  
Thomas Sewell
Keyword(s):  
Gold Standard ◽  
Program Verification ◽  
Theorem Prover ◽  
Worked Example ◽  
Translation Validation ◽  
Smt Solvers ◽  
Ongoing Effort ◽  
Formal Rule ◽  
Standard Level ◽  
Rule Set

In previous work [Sewell, Myreen and Klein, 2013] we have implemented atranslation validation mechanism for checking that a C compiler is adheringto the expected semantics of a verified program. We used this apparatus tocheck the compilation of the seL4 verified operating systemkernel [Klein et.al. 2009] by GCC 4.5.1. To get this result, wecarefully chose a problem representation that worked well with certain highlyoptimised SMT solvers. This raises a question of correctness. While we areconfident the result is correct, we still aim to replay this result with themost dependable tools available.In this work we present a formalisation of the proof rules needed to replaythe translation check within the theorem prover Isabelle/HOL. This is part ofan ongoing effort to bring the entire translation validation result within asingle trusted proof engine and derive a single correctness theorem, thusreaching the gold standard level of trustworthiness for program verification.We had hoped to present the formal rule set in action through a worked example.Unfortunately while we have all the theory we need, the mechanisms forselecting and applying the rules and discharging certain side conditions remaina work in progress, and our example proof is incomplete.

scholarly journals Hoare Semigroups

2017 ◽  
Vol 28 (6) ◽  
pp. 775-799 ◽  
Author(s):  
GEORG STRUTH
Keyword(s):  
Theorem Prover ◽  
Hoare Logic

A semigroup-based setting for developing Hoare logics and refinement calculi is introduced together with procedures for translating between verification and refinement proofs. A new Hoare logic for multirelations and two minimalist generic verification and refinement components, implemented in an interactive theorem prover, are presented as applications that benefit from this generalisation.

Sign in / Sign up

Export Citation Format

Share Document