Proving Reflex Program Verification Conditions in Coq Proof Assistant

2021 ◽  
Author(s):  
Ivan Chernenko ◽  
Igor Anureev ◽  
Natalia Garanina
Keyword(s):  
Program Verification ◽  
Proof Assistant ◽  
Verification Conditions ◽  
Coq Proof Assistant

scholarly journals Modular development of certified program verifiers with a proof assistant,

2008 ◽  
Vol 18 (5-6) ◽  
pp. 599-647 ◽  
Author(s):  
ADAM CHLIPALA
Keyword(s):  
Program Verification ◽  
Type System ◽  
Minimal Amount ◽  
Dependent Types ◽  
Proof Assistant ◽  
Machine Code ◽  
The Coq Proof Assistant ◽  
Verification Tool ◽  
Coq Proof Assistant ◽  
New Type

AbstractWe report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checked proof of full correctness. The verifier is able to prove memory safety of x86 machine code programs compiled from code that uses algebraic datatypes. The tool's soundness theorem is expressed in terms of the bit-level semantics of x86 programs, so its correctness depends on very few assumptions. We take advantage of Coq's support for programming with dependent types and modules in the structure of the development. The approach is based on developing a library of reusable functors for transforming a verifier at one level of abstraction into a verifier at a lower level. Using this library, it is possible to prototype a verifier based on a new type system with a minimal amount of work, while obtaining a very strong soundness theorem about the final product.

scholarly journals Homotopy limits in type theory

2015 ◽  
Vol 25 (5) ◽  
pp. 1040-1070 ◽  
Author(s):  
JEREMY AVIGAD ◽  
KRZYSZTOF KAPULKIN ◽  
PETER LEFANU LUMSDAINE
Keyword(s):  
Homotopy Type ◽  
Systematic Study ◽  
Type Theory ◽  
Proof Assistant ◽  
Classical Approach ◽  
Homotopy Type Theory ◽  
The Coq Proof Assistant ◽  
Homotopy Limits ◽  
Coq Proof Assistant

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

Every bit counts: The binary representation of typed data and programs

2012 ◽  
Vol 22 (4-5) ◽  
pp. 529-573 ◽  
Author(s):  
ANDREW J. KENNEDY ◽  
DIMITRIOS VYTINIOTIS
Keyword(s):  
Binary Data ◽  
General Framework ◽  
Binary Representation ◽  
Proof Assistant ◽  
A Value ◽  
The Coq Proof Assistant ◽  
Binary Encoding ◽  
Coq Proof Assistant ◽  
Definition Of ◽  
Formal Properties

AbstractWe show how the binary encoding and decoding of typed data and typed programs can be understood, programmed and verified with the help of question–answer games. The encoding of a value is determined by the yes/no answers to a sequence of questions about that value; conversely, decoding is the interpretation of binary data as answers to the same question scheme. We introduce a general framework for writing and verifying game-based codecs. We present games in Haskell for structured, recursive, polymorphic and indexed types, building up to a representation of well-typed terms in the simply-typed λ-calculus with polymorphic constants. The framework makes novel use of isomorphisms between types in the definition of games. The definition of isomorphisms together with additional simple properties make it easy to prove that codecs derived from games never encode two distinct values using the same code, never decode two codes to the same value and interpret any bit sequence as a valid code for a value or as a prefix of a valid code. Formal properties of the framework have been proved using the Coq proof assistant.

scholarly journals A formal approach for the verification of the permission-based security model of Android

2018 ◽  
Vol 21 (2) ◽  
Author(s):  
Carlos Luna ◽  
Gustavo Betarte ◽  
Juan Campo ◽  
Camila Sanz ◽  
Maximiliano Cristiá ◽  
...  
Keyword(s):  
Formal Specification ◽  
Control Policy ◽  
Proof Assistant ◽  
Security Model ◽  
Access Control Policy ◽  
Formal Approach ◽  
Fundamental Properties ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Security Properties

This article reports on our experiences in applying formal methods to verify the security mechanisms of Android. We have developed a comprehensive formal specification of Android's permission model, which has been used to state and prove properties that establish expected behavior of the procedures that enforce the defined access control policy. We are also interested in providing guarantees concerning actual implementations of the mechanisms. Therefore we are following a verification approach that combines the use of idealized models, on which fundamental properties are formally verified, with testing of actual implementations using lightweight model-based techniques. We describe the formalized model, present security properties that have been proved using the Coq proof assistant and propose the use of a certified algorithm for performing verification activities such as monitoring of actual implementations of the platform and also as a testing oracle.

scholarly journals Verification of a brick Wang tiling algorithm

10.29007/2m5f ◽  
2018 ◽  
Author(s):  
Toshiaki Matsushima ◽  
Yoshihiro Mizoguchi ◽  
Alexandre Derouet-Jourdan
Keyword(s):  
Computer Graphics ◽  
Proof Assistant ◽  
Induction Process ◽  
Coq Proof Assistant ◽  
Wang Tile

We have implemented a certified Wang tiling program for tiling a rectangle region using a brick corner Wang tile set. A brick corner Wang tile set is a special Wang tile set introduced by A. Derouet-Jourdan et al. in computer graphics in 2015 to model wall patterns texture. We have implemented a tiling algorithm using Coq proof assistant and proved its correctness. This correctness assures the existence of a tiling of any brick corner Wang tile set for any size of rectangle. The essential points of our proof are the existence of a tiling for a $2 \times 2$ rectangle and a simple induction process. Since the brick corner Wang tile is a class of infinite kinds of tile sets, it is not straightforward and there are many conditional branches to prove the correctness. The certification with Coq assures that there are no lack of conditions.

scholarly journals Ownership and Immutability in Coq

2021 ◽  
Author(s):  
◽  
Julian Mackay
Keyword(s):  
Programming Languages ◽  
Management System ◽  
Type Systems ◽  
Formal Proof ◽  
Proof Assistant ◽  
Significant Issue ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant

<p>A significant issue in modern programming languages is unsafe aliasing. Modern type systems have attempted to address this in two prominent ways; immutability and ownership, and often a combination of the two [4][17]. The goal of this thesis is to formalise Immutability and Ownership using the Coq Proof Assistant, a formal proof management system [13]. We encode three type systems using Coq; Featherweight Immutable Java, Featherweight Generic Java and Featherweight Ownership Generic Java, and prove them sound. We describe the challenges presented in encoding immutability, ownership and type systems in general in Coq.</p>

scholarly journals The Marriage of Univalence and Parametricity

2021 ◽  
Vol 68 (1) ◽  
pp. 1-44
Author(s):  
Nicolas Tabareau ◽  
Éric Tanter ◽  
Matthieu Sozeau
Keyword(s):  
Type Theory ◽  
Program Verification ◽  
Proof Assistants ◽  
Computationally Efficient ◽  
Lightweight Framework ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Efficient Representation ◽  
Term Dependency ◽  
Work First

Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity , is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte : basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

scholarly journals An experimental library of formalized Mathematics based on the univalent foundations

2015 ◽  
Vol 25 (5) ◽  
pp. 1278-1294 ◽  
Author(s):  
VLADIMIR VOEVODSKY
Keyword(s):  
Type Theory ◽  
Proof Assistant ◽  
Formalization Of Mathematics ◽  
Constructive Type Theory ◽  
Short Overview ◽  
Formalized Mathematics ◽  
The Coq Proof Assistant ◽  
Constructive Type ◽  
Coq Proof Assistant ◽  
Univalent Foundations

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

Sign in / Sign up

Export Citation Format

Share Document