We describe recent improvements on small inversions, a technique presented earlier as a possible alternative to Coq standard inversion

Van Breugel et al. [F. van Breugel et al, Theor. Comput. Sci. 333(1-2):171-197, 2005] have given an elegant testing framework that can characterise probabilistic bisimulation, but its completeness proof is highly involved. Deng and Feng [Y. Deng and Y. Feng, Inf. Comput. 257:58-64, 2017] have simplified that result for finite-state processes. The crucial part in the latter work is an algorithm that can construct enhanced tests. We formalise the algorithm and prove its correctness by maintaining a number of subtle invariants in Coq. To support the formalisation, we develop a reusable library for manipulating finite sets. This sets an early example of formalising probabilistic concurrency theory or quantitative aspects of concurrency theory at large, which is a rich field to be pursued

This paper introduces CertiCAN, a tool produced using the Coq proof assistant for the formal certification of CAN analysis results. Result certification is a process that is light-weight and flexible compared to tool certification, which makes it a practical choice for industrial purposes. The analysis underlying CertiCAN, which is based on a combined use of two well-known CAN analysis techniques, is computationally efficient. Experiments demonstrate that CertiCAN is faster than the corresponding certified combined analysis. More importantly, it is able to certify the results of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. This result paves the way for a broader acceptance of formal tools for the certification of real-time systems analysis results.

We describe a generic method to implement and extract partial recursive algorithms in Coq in a purely constructive way, using L. Paulson's if-then-else normalization as a running example.

In the context of computer assisted verification of schedulability analyses, very expressive task models are useful to factorize the correctness proofs of as many analyses as possible. The digraph task model seems a good candidate due to its powerful expressivity. Alas, its ability to capture dependencies between arrival and execution times of jobs of different tasks is very limited. We propose here a task model that generalizes the digraph model and its corresponding analysis for fixed-priority scheduling with limited preemption. A task may generate several types of jobs, each with its own worst-case execution time, priority, non-preemptable segments and maximum jitter. We present the correctness proof of the analysis in a way amenable to its formalization in the Coq proof assistant. Our objective (still in progress) is to formally certify the analysis for that general model such that the correctness proof of a more specific (standard or novel) analysis boils down to specifying and proving its translation into our model. Furthermore, expressing many different analyses in a common framework paves the way for formal comparisons.

This paper presents a generic proof of Typical Worst-Case Analysis (TWCA), an analysis technique for weakly-hard real-time uniprocessor systems. TWCA was originally introduced for systems with fixed priority preemptive (FPP) schedulers and has since been extended to fixed-priority nonpreemptive (FPNP) and earliest-deadline-first (EDF) schedulers. Our generic analysis is based on an abstract model that characterizes the exact properties needed to make TWCA applicable to any system model. Our results are formalized and checked using the Coq proof assistant along with the Prosa schedulability analysis library. Our experience with formalizing real-time systems analyses shows that this is not only a way to increase confidence in our claimed results: The discipline required to obtain machine checked proofs helps understanding the exact assumptions required by a given analysis, its key intermediate steps and how this analysis can be generalized.

This paper presents the first steps toward a formally proven tool for schedulability analysis of tasks with offsets. We formalize and verify the seminal response time analysis of Tindell by extending the Prosa proof library, which is based on the Coq proof assistant. Thanks to Coq's extraction capabilities, this will allow us to easily obtain a certified analyzer. Additionally, we want to build a Coq certifier that can verify the correctness of results obtained using related (but uncertified), already existing analyzers. Our objective is to investigate the advantages and drawbacks of both approaches, namely the certified analysis and the certifier. The work described in this paper as well as its continuation is intended to enrich the Prosa library.

This paper presents an approach to construct a verified virtual prototyping framework of embedded software. The machine code executed on a simulated target architecture can be proven to provide the same results as the real hardware, and the proof is verified with a theorem prover. The method consists in proving each instruction of the instruction set independently, by proving that the execution of the C code simulating an instruction yields an identical result to that obtained by a formal executable model of the processor architecture. This formal model itself is obtained through an automated translation process from the architecture specifications. Each independent proof draws a number of lemmas from a generic lemma library and also uses the automation of inversion tactics in the theorem prover. The paper presents the proof of the ARM architecture version 6 Instruction Set Simulator of the SimSoC open source simulator, with all of the proofs being verified by the Coq proof assistant, using automated tactics to reduce manual proof development.

When reasoning on formulas involving large-size inductively defined relations, such as the semantics of a real programming language, many steps require the inversion of a hypothesis. The built-in "inversion" tactic of Coq can then be used, but it suffers from severe controllability, maintenance and efficiency issues, which makes it unusable in practice in large applications. To circumvent this issue, we propose a proof technique based on the combination of an antidiagonal argument and the impredicative encoding of inductive data-structures. We can then encode suitable helper tactics in LTac, yielding scripts which are much shorter (as well as corresponding proof terms) and, more importantly, much more robust against changes in version changes in the background software. This is illustrated on correctness proofs of non-trivial C programs according to the operational semantics of C defined in CompCert.

Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They greatly simplify the code, while still admitting efficient distributed execution, including on sensor networks. From previous work [discotec11], we know that they also provide a promising approach to another tough issue about distributed protocols: their formal verification. Indeed, we can take advantage of their data centric orientation, which allows us to explicitly handle global structures such as the topology of the network. We illustrate here our approach on two non-trivial protocols and discuss its Coq implementation.

The simulation of Systems-on-Chip (SoC) is nowadays a hot topic because, beyond providing many debugging facilities, it allows the development of dedicated software before the hardware is available. Low-consumption CPUs such as ARM play a central role in SoC. However, the effectiveness of simulation depends on the faithfulness of the simulator. To this effect, we propose here to prove significant parts of such a simulator, SimSoC. Basically, on one hand, we develop a Coq formal model of the ARM architecture while on the other hand, we consider a version of the simulator including components written in Compcert-C. Then we prove that the simulation of ARM operations, according to Compcert-C formal semantics, conforms to the expected formal model of ARM. Size issues are partly dealt with using automatic generation of significant parts of the Coq model and of SimSoC from the official textual definition of ARM. However, this is still a long-term project. We report here the current stage of our efforts and discuss in particular the use of Compcert-C in this framework.

Data centric languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. They simplify greatly the code, which is orders of magnitude shorter, much more declarative, while still admitting efficient distributed execution. We show that they also provide a promising approach to the verification of distributed protocols, thanks to their data centric orientation, which allows to explicitly handle global structures, such as the topology of the network, routing tables, trees, etc, as well as their properties. We consider a framework using an original formalization in the Coq proof assistant of a distributed computation model based on message passing with either synchronous or asynchronous behavior. The declarative rules of the Netlog language for specifying distributed protocols, as well as the virtual machines for evaluating these rules, are encoded in Coq as well. We consider as a case study tree protocols, and show how this framework enables us to formally verify them in both the asynchronous and synchronous setting.

Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this report, we show that moreover they provide a promising approach to the verification of distributed protocols. We consider the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq and we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed protocols, as shown on a concrete case study, a spanning tree construction in both the asynchronous and synchronous setting.

For validating low level embedded software, engineers use simulators that take the real binary as input. Like the real hardware, these full-system simulators are organized as a set of components. The main component is the CPU simulator (ISS), because it is the usual bottleneck for the simulation speed, and its development is a long and repetitive task. Previous work showed that an ISS can be generated from an Architecture Description Language (ADL). In the work reported in this paper, we generate a CPU simulator directly from the pseudo-formal descriptions of the reference manual. For each instruction, we extract the information describing its behavior, its binary encoding, and its assembly syntax. Next, after automatically applying many optimizations on the extracted information, we generate a SystemC/TLM ISS. We also generate tests for the decoder and a formal specification in Coq. Experiments show that the generated ISS is as fast and stable as our previous hand-written ISS.

The design and debugging of Systems-on-Chip using a hardware implementation is difficult and requires heavy material. Simulation is an interesting alternative approach, which is both more flexible and less expensive. SimSoC is a fast instruction set simulator for various ARM, PowerPC, and RISC-based architectures. However, speed involves tricky short-comings and design decisions, resulting in a complex software product. This makes the accuracy of the simulator a non-trivial question: there is a strong need to strengthen the confidence that simulations results match the expected accuracy. We therefore decided to certify SimSoC, that is, to formally prove in Coq the correctness of a significant part of this software. The present paper reports our first efforts in this direction, targeting the ARMv6 architecture.

We show how an inductive hypothesis can be inverted with small proof terms, using just dependent elimination with a diagonal predicate. The technique works without any auxiliary type such as True, False, eq. It can also be used to discriminate, in some sense, the constructors of an inductive type of sort Prop in Coq.

Declarative languages, such as recursive rule based languages, have been proposed to program distributed applications over networks. It has been shown that they simplify greatly the code, while still offering efficient distributed execution. In this paper, we show that moreover they provide a promising approach to the verification of distributed protocols. We choose the Netlog language and use the Coq proof assistant. We first formalize the distributed computation model based on message passing with either synchronous or asynchronous behavior. We then see how the declarative rules of the protocols can be simply encoded in Coq. Finally, we develop the machine embedded on each node of the network which evaluates the rules. This framework enables us to formally verify distributed declarative protocols, as sketched on a concrete example, a breadth-first search tree construction in a distributed network.

Population protocols are an elegant model recently introduced for distributed algorithms running in large and unreliable networks of tiny mobile agents. Correctness proofs of such protocols involve subtle arguments on infinite sequences of events. We propose a general formalization of self-stabilizing population protocols with the Coq proof assistant. It is used in reasoning about a concrete protocol for leader election in complete graphs. The protocol is formally proved to be correct for networks of arbitrarily large size. To this end we develop an appropriate theory of infinite sequences, including results for reasoning on abstractions. In addition, we provide a constructive correctness proof for a leader election protocol in directed rings. An advantage of using a constructive setting is that we get more informative proofs on the scenarios that converge to the desired configurations.

We study a normalization function in an algebra of terms quotiented by an associative, commutative and involutive operator (logical xor). This study is motivated by the formal verification of cryptographic systems, where a normalization function for xor-terms turns out to play a key role. Such a function is easy to define using general recursion. However, as it is to be used in a type theoretic proof assistant, we also need a proof termination of this function. Instead of using a clever mixture of various rewriting orderings, we follow an approach involving the power of Type Theory with dependent types. The results are to be applied in the proof of the security API described in [28].

This chapter is an attempt to provide a formal specification which is as faithful as possible to the informal one and consistent. The features of Coq are powerful enough to make the specification both very abstract and executable. We construct mathematical structures or functions whenever possible, instead of specifying them with axioms. If the axiomatic way turns out better, we look for structures satisfying the axioms we need.

We show how the proof-assistant Coq helped us formally verify the security of an API. As far as we know, this is the first mathematical proof of security of an API. The API we verified is a fixed version of Bond's modelization of IBM's Common Cryptographic Architecture. We explain the methodology we followed, sketch our proof and explain the points the formal verification raised.

Inductive characterizations of words containing the same number of 'a' and 'b' can easily be given. However, formally proving the completeness of some of them turns out to be trickier than one may expect. We discuss and compare two Coq developments relating such balanced words to their inductive characterizations. One is based on auxiliary inductive structures and elementary arguments. The other one is based on a discrete variant of the intermediate value theorem.

Nous décrivons comment Coq nous a permis de démontrer mathématiquement et formellement la sécurité d'une interface de programmation de sécurité. À notre connaissance il s'agit de la première démonstration mathématique de sécurité d'une interface de programmation. Nous présentons brièvement notre démonstration et expliquons les difficultés rencontrées lors du processus de formalisation.

We provide a proof that the elegant trick of Olivier Danvy for expressing printf-like functions without dependent types is correct, where formats are encoded by functional expressions in continuation-passing style. Our proof is formalized in the Calculus of Inductive Constructions. We stress a methodological point: when one proves equalities between functions, a common temptation is to introduce a comprehension axiom and then to prove that the considered functions are extensionally equal. Rather than weakening the result (and adding an axiom), we prefer to strenghten the inductive argumentation in order to stick to the intensional equality.

Towards verifying mobile code, we choose to formalize an appropriate elementary model of concurrency in type theory (more precisely: the calculus of inductive constructions, CIC, implemented in the Coq proof assistant). The chosen process calculus is the Join-Calculus (JC) of Fournet, Gonthier and Levy. The latter can be seen as a variant of the pi-calculus of Milner, Parrow and Walker, with better locality properties. We use Coq for encoding a structural operational semantics of JC based on the reflexive chemical abstract machines model. Our formalisation uses the full power of inductive constructions and dependent types available in the underlying theory of Coq, in order to capture the reflexive features of JC.

The ABR conformance protocol is a real-time program that controls data ow rates on ATM networks. A crucial part of this protocol is the dynamical computation of the expected rate of data cells. We present here a modelling of the corresponding program with its environment, using the notion of (parametric) timed automata. A fundamental property of the service provided by the protocol to the user is expressed in this framework and proved by two di erent methods. The rst proof relies on inductive invariants, and was originally veri ed using theorem- proving assistant Coq. The second proof is based on reachability analysis, and was obtained using model-checker HyTech. We explain and compare these two proofs in the uni ed framework of timed automata.

This book is intended to help the student or the engineer who wants an introduction to formal techniques, as well as the practitioner who wishes to broaden her or his knowledge of this subject. It mainly aims at providing a synthetic view of the logical foundations of such techniques, with an emphasis on intuitive ideas, so that it can also be considered as a practical complement to classical introductory manuals to logic, which generally focus more detail on specific subjects (e.g. first-order logic), and to books dedicated to particular formal methods.

Conformance control for ATM cells is based on a real-time reactive algorithm which delivers a value depending on inputs from the network. This value must always fit with a well defined theoretical value. We present here the correctness proof of the algorithm standardized for the ATM transfer capability called ABR. The proof turned out to produce a key argument during the standardization process of ABR.

Conformance control for ATM cells is based on a real-time reactive algorithm which delivers a value depending on inputs from the network. This value must always agree with a well defined theoretical value. We present here the correctness proof of the algorithm standardized for the ATM transfer capability called ABR. The proof turned out a key argument during the standardization process of ABR.

This paper presents the techniques used for proving, in the framework of type theory, the correctness of an algorithm recently standardized at ITU-T that handles time explicitly. The structure of the proof and its formalization in Coq are described, as well as the main tools which have been developed: an abstract model of “real-time” that makes no assumption on the nature of time and a way to actually find proofs employing transitivity, using only logical definitions and an existing tactic.

Program extraction is a well known technique for developing correct functional programs from a constructive proof of their specification. This paper shows how to deal with exceptions in such a framework. We propose a modular (and impredicative) formalization in the calculus of constructions and we illustrate the technique on three examples.

This paper is about exceptions handling using classical techniques of program extraction. We propose an impredicative formalization in the calculus of constructions and we illustrate the technique on two examples. The first one, though simple, allows us to experiment various techniques. The second one is an adaptation of a bigger algorithm previously developed in Coq by J. Rouyer, namely first order unification. Only small changes were needed in order to get a more efficient program from the original one.

We introduce a new execution model for implementing FDTs based on the reactive approach. In this model, called the PAM, systems are divided into several reactive entities communicating by an activation mechanism. This paper introduces the PAM approach and shows how different communication mechanisms such as asynchronous fifo in ESTELLE or multiple rendez-vous in LOTOS can be implemented. It then presents the analysis of an implementation of a transport protocol (CCITT T70).

Since the seminal paper of Colmerauer (1975) on metamorphosis grammars, Prolog has been recognised as a potentially interesting language for writing compilers. However very few real size compilers have been written in Prolog until now. We describe here such an experiment, called Veda, carried out at CNET since 1984, in which an Estelle compiler-simulator for protocol checking was successfully developed. We sketch the (to our knowledge original) techniques which were introduced in Veda for enhancing performances up to a usable level, while keeping clarity, flexibility and declarativity in the programming style. One of them, based on “arrows”, has applications in a class of problems independant from compilation.

The development of a simulator, called Veda, is described. Veda is a software tool to help designers in protocol modeling and validation. It is oriented towards the rapid prototyping of distributed algorithms. Algorithms are described using an ISO (International Organisation for Standardization) formal description technique, called Estelle. The development of Veda and its internal structure is presented, emphasizing the use of Prolog as a software engineering tool. Typical uses of Veda are discussed.

Keywords: Parallel Programming