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

CSim 2

2021 ◽  
Vol 43 (1) ◽  
pp. 1-46
Author(s):  
David Sanan ◽  
Yongwang Zhao ◽  
Shang-Wei Lin ◽  
Liu Yang
Keyword(s):  
Programming Languages ◽  
Concurrent Systems ◽  
Theorem Prover ◽  
Compositional Techniques ◽  
Machine Code ◽  
Top Down ◽  
Hol Theorem Prover ◽  
High Level ◽  
High Degree

To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is top-down verification where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present CSim 2 a (compositional) rely-guarantee-based framework for the top-down verification of complex concurrent systems in the Isabelle/HOL theorem prover. CSim 2 uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim 2 provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification, CSim 2 provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of CSim 2 by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use CSim 2 to preserve the property on lower abstraction layers.

scholarly journals Continuous Verification of Network Security Compliance

2021 ◽  
Author(s):  
Claas Lorenz ◽  
Vera Clemens ◽  
Max Schrötter ◽  
Bettina Schnor
Keyword(s):  
Network Security ◽  
Formal Language ◽  
Theorem Prover ◽  
Domain Specific ◽  
Rule Sets ◽  
Rule Set ◽  
Verification Tools ◽  
Data Structures And Algorithms ◽  
Security Compliance ◽  
High Level

Continuous verification of network security compliance is an accepted need. Especially, the analysis of stateful packet filters plays a central role for network security in practice. But the few existing tools which support the analysis of stateful packet filters are based on general applicable formal methods like Satifiability Modulo Theories (SMT) or theorem prover and show runtimes in the order of minutes to hours making them unsuitable for continuous compliance verification.<br>In this work, we address these challenges and present the concept of state shell interweaving to transform a stateful firewall rule set into a stateless rule set. This allows us to reuse any fast domain specific engine from the field of data plane verification tools leveraging smart, very fast, and domain specialized data structures and algorithms including Header Space Analysis (HSA). First, we introduce the formal language FPL that enables a high-level human-understandable specification of the desired state of network security. Second, we demonstrate the instantiation of a compliance process using a verification framework that analyzes the configuration of complex networks and devices - including stateful firewalls - for compliance with FPL policies. Our evaluation results show the scalability of the presented approach for the well known Internet2 and Stanford benchmarks as well as for large firewall rule sets where it outscales state-of-the-art tools by a factor of over 41.

scholarly journals The verified CakeML compiler backend

2019 ◽  
Vol 29 ◽  
Author(s):  
YONG KIAM TAN ◽  
MAGNUS O. MYREEN ◽  
RAMANA KUMAR ◽  
ANTHONY FOX ◽  
SCOTT OWENS ◽  
...  
Keyword(s):  
Functional Programming ◽  
Theorem Prover ◽  
Runtime System ◽  
Machine Code ◽  
Garbage Collector ◽  
Overall Design ◽  
Data Representations ◽  
Arbitrary Precision ◽  
High Level ◽  
Intermediate Languages

AbstractThe CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler’s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.

scholarly journals Implementing type theory in higher order constraint logic programming

2019 ◽  
Vol 29 (8) ◽  
pp. 1125-1150
Author(s):  
FERRUCCIO GUIDI ◽  
CLAUDIO SACERDOTI COEN ◽  
ENRICO TASSI
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Theorem Prover ◽  
Type Checking ◽  
Language Extension ◽  
Order Constraint ◽  
Simple Implementation ◽  
Calculus Of Inductive Constructions ◽  
High Level

In this paper, we are interested in high-level programming languages to implement the core components of an interactive theorem prover for a dependently typed language: the kernel – responsible for type-checking closed terms – and the elaborator – that manipulates open terms, that is terms containing unresolved unification variables.In this paper, we confirm that λProlog, the language developed by Miller and Nadathur since the 80s, is extremely suitable for implementing the kernel. Indeed, we easily obtain a type checker for the Calculus of Inductive Constructions (CIC). Even more, we do so in an incremental way by escalating a checker for a pure type system to the full CIC.We then turn our attention to the elaborator with the objective to obtain a simple implementation thanks to the features of the programming language. In particular, we want to use λProlog’s unification variables to model the object language ones. In this way, scope checking, carrying of assignments and occur checking are handled by the programming language.We observe that the eager generative semantics inherited from Prolog clashes with this plan. We propose an extension to λProlog that allows to control the generative semantics, suspend goals over flexible terms turning them into constraints, and finally manipulate these constraints at the meta-meta level via constraint handling rules.We implement the proposed language extension in the Embedded Lambda Prolog Interpreter system and we discuss how it can be used to extend the kernel into an elaborator for CIC.

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.

Computational Model

1995 ◽  
Author(s):  
Ronnie W. Smith ◽  
D. Richard Hipp
Keyword(s):  
Computational Model ◽  
Selection Process ◽  
Theorem Prover ◽  
Processing Algorithm ◽  
Process Step ◽  
Completion Process ◽  
High Level ◽  
Relationship Of ◽  
Task Step ◽  
Dialog Processing

This chapter describes the computational model that has evolved from the theory of integrated dialog processing presented in the previous chapter. The organization of this chapter follows. 1. A high-level description of the basic dialog processing algorithm. 2. A detailed discussion of the major steps of the algorithm. 3. A concluding critique that evaluates the model’s effectiveness at handling several fundamental problems in dialog processing. The system software that implements this model is available via anonymous FTP. Details on obtaining the software are given in appendix C. Figure 4.1 describes the basic steps of the overall dialog processing algorithm that is executed by the dialog controller. By necessity, this description is at a very high level, but specifics will be given in subsequent sections. The motivation for these steps is presented below. Since the computer is providing task assistance, an important part of the algorithm must be the selection of a task step to accomplish (steps 1 and 2). Because the characterization of task steps is a function of the domain processor, the dialog controller must receive recommendations from the domain processor during the selection process (step 1). However, since a dialog may have arbitrary suspensions and resumptions of subdialogs, the dialog controller cannot blindly select the domain processor’s recommendation. The relationship of the recommended task step to the dialog as well as the dialog status must be considered before the selection can be made (step 2). Once a task step is selected, the dialog controller must use the general reasoning facility (i.e. the interruptible theorem prover, IPSIM) in step 3 to determine when the task step is accomplished. Whenever the theorem prover cannot continue due to a missing axiom, the dialog controller uses available knowledge about linguistic realizations of utterances in order to communicate a contextually appropriate utterance as well as to compute expectations for the response. After the response is received and its relationship to the missing axiom determined, the dialog controller must decide how to continue the task step completion process.

scholarly journals VERIFICATION OF A STRING TO INTEGER CONVERSION PROGRAM

2020 ◽  
Author(s):  
Vladimir Ivanovich Shelekhov ◽  
Keyword(s):  
Program Verification ◽  
Deductive Verification ◽  
Program Specification

Deductive verification of a string to integer conversion program kstrtoul in Linux OS kernel library is described. The kstrtoul program calculates the integer value presented as a char sequence of digits. To simplify program verification the transformations of replacing pointer operators to equivalent actions without pointers are conducted. Model of inner program state are constructed to enhance program specification. Deductive verification was conducted in the tools Why3 and Coq.

Sign in / Sign up

Export Citation Format

Share Document