Engineering Hoare Logic-Based Program Verification in K Framework

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

Journal of Automated Reasoning ◽

10.1007/s10817-021-09610-2 ◽

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.

Download Full-text

KAT and PHL in Coq

Computer Science and Information Systems ◽

10.2298/csis0802137p ◽

2008 ◽

Vol 5 (2) ◽

pp. 137-160 ◽

Cited By ~ 3

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). .

Download Full-text

Java Program Verification via a Hoare Logic with Abrupt Termination

Fundamental Approaches to Software Engineering - Lecture Notes in Computer Science ◽

10.1007/3-540-46428-x_20 ◽

2000 ◽

pp. 284-303 ◽

Cited By ~ 59

Author(s):

Marieke Huisman ◽

Bart Jacobs

Keyword(s):

Program Verification ◽

Hoare Logic ◽

Java Program

Download Full-text

Synthesizing Conjunctive & Disjunctive Linear Invariants by K-means++ and SVM

The International Arab Journal of Information Technology ◽

10.34028/iajit/17/6/3 ◽

2020 ◽

Vol 17 (6) ◽

pp. 847-856

Author(s):

Shengbing Ren ◽

Xiang Zhang

Keyword(s):

Software Verification ◽

State Of The Art ◽

Positive Sample ◽

Machine Learning Algorithms ◽

Support Vector ◽

Hoare Logic ◽

Excellent Performance ◽

Automated Software ◽

Inductive Invariants ◽

Linear Invariants

The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically

Download Full-text