Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

In this contribution we present a formalised algorithm in the Isabelle/HOL proof assistant to compute echelon forms, and, as a consequence, characteristic polynomials of matrices. We have proved its correctness over Bézout domains, but its executability is only guaranteed over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This is possible since the algorithm has been parameterised by a (possibly non-computable) operation that returns the Bézout coefficients of a pair of elements of a ring. The echelon form is also used to compute determinants and inverses of matrices. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, etc.). In order to improve performance, the algorithm has been refined to immutable arrays inside of Isabelle and code can be generated to functional languages as well.     

Proof Pearl—A Mechanized Proof of GHC’s Mergesort

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art proof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.     

Building certified libraries for PCC: dynamic storage allocation

Proof-carrying code (PCC) allows a code producer to provide to a host a program along with its formal safety proof. The proof attests to a certain safety policy enforced by the code, and can be mechanically checked by the host. While this language-based approach to code certification is very general in principle, existing PCC systems have only focused on programs whose safety proofs can be automatically generated. As a result, many low-level system libraries (e.g., memory management) have not yet been handled. In this paper, we explore a complementary approach in which general properties and program correctness are semi-automatically certified. In particular, we introduce a low-level language, CAP, for building certified programs and present a certified library for dynamic storage allocation.     

Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.     

A Mechanized Proof of the Basic Perturbation Lemma

We present a complete mechanized proof of the result in homological algebra known as basic perturbation lemma. The proof has been carried out in the proof assistant Isabelle, more concretely, in the implementation of higher-order logic (HOL) available in the system. We report on the difficulties found when dealing with abstract algebra in HOL, and also on the ongoing stages of our project to give a certified version of some of the algorithms present in the Kenzo symbolic computation system. J. Aransay was partially supported by Ministerio de Educación y Ciencia, MTM2006/06513, and by Gobierno de La Rioja ANGI2005/19 and J. Rubio was partially supported by Ministerio de Educación y Ciencia, MTM2006/06513, and by Gobierno de La Rioja ANGI2005/19.     

Invariant diagrams with data refinement

Invariant based programming is an approach where we start to construct a program by first identifying the basic situations (pre- and post-conditions as well as invariants) that could arise during the execution of the algorithm. These situations are identified before any code is written. After that, we identify the transitions between the situations, which will give us the flow of control in the program. Data refinement is a technique of building correct programs working on concrete data structures as refinements of more abstract programs working on abstract data types. We study in this paper data refinement for invariant based programs and we apply it to the construction of the classical Deutsch–Schorr–Waite graph marking algorithm. Our results are formalized and mechanically proved in the Isabelle/HOL theorem prover.     

Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a “trace” any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.     

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction

We present a formally verified and executable on-the-fly LTL model checker that uses ample set partial order reduction. The verification is done using the proof assistant Isabelle/HOL and covers everything from the abstract correctness proof down to the generated SML code. Building on Doron Peled’s paper “Combining Partial Order Reductions with On-the-Fly Model-Checking”, we formally prove abstract correctness of ample set partial order reduction. This theorem is independent of the actual reduction algorithm. We then verify a reduction algorithm for a simple but expressive fragment of Promela. We use static partial order reduction, which allows separating the partial order reduction and the model checking algorithms regarding both the correctness proof and the implementation. Thus, the Cava model checker that we verified in previous work can be used as a back end with only minimal changes. Finally, we generate executable SML code using a stepwise refinement approach. We test our model checker on some examples, observing the effectiveness of the partial order reduction algorithm.     

Run-Time Validation of Speculative Optimizations using CVC.

Translation validation is an approach for validating the output of optimizing compilers. Rather than verifying the compiler itself, translation validation mandates that every run of the compiler generate a formal proof that the produced target code is a correct implementation of the source code. Speculative loop optimizations are aggressive optimizations which are only correct under certain conditions which cannot be validated at compile time. We propose using an automatic theorem prover together with the translation validation framework to automatically generate run-time tests for such speculative optimizations. This run-time validation approach must not only detect the conditions under which an optimization generates incorrect code, but also provide a way to recover from the optimization without aborting the program or producing an incorrect result. In this paper, we apply the run-time validation technique to a class of speculative reordering transformations and give some initial results of run-time tests generated by the theorem prover CVC.     

A Canonical Locally Named Representation of Binding

This paper is about completely formal representation of languages with binding. We have previously written about a representation following an approach going back to Frege, based on first-order syntax using distinct syntactic classes for locally bound variables vs. global or free variables?(Sato and Pollack, J Symb Comput 45:598?C616, 2010). The present paper differs from our previous work by being more abstract. Whereas we previously gave a particular concrete function for canonically choosing the names of binders, here we characterize abstractly the properties required of such a choice function to guarantee canonical representation, and focus on the metatheory of the representation, proving that it is in substitution preserving isomorphism with the nominal Isabelle representation of pure lambda terms. This metatheory is formalized in Isabelle/HOL. The final section outlines a formalization in Matita of a challenging language with multiple binding and simultaneous substitution. The Isabelle and Matita proof files are available online.     

A Comparison of Mizar and Isar

The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also differs in many other respects from most current systems. John Harrison has shown that one can have a Mizar mode on top of a tactical prover, allowing one to combine a mathematical proof language with other styles of proof checking. Currently the only fully developed Mizar mode in this style is the Isar proof language for the Isabelle theorem prover. In fact the Isar language has become the official input language to the Isabelle system, even though many users still use its low-level tactical part only. In this paper we compare Mizar and Isar. A small example, Euclid's proof of the existence of infinitely many primes, is shown in both systems. We also include slightly higher-level views of formal proof sketches. Moreover, a list of differences between Mizar and Isar is presented, highlighting the strengths of both systems from the perspective of end-users. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system.     

Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM

Distributed algorithms are subtle and error-prone. Still, very few of them have been formally verified, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms. We consider formal verification of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal verification of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.     

A Formal Proof of Sylow's Theorem

The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a nontrivial combinatorial identity. The mathematical proof is explained in some detail, leading on to the mechanization of group theory and the necessary combinatorics in Isabelle. We present the mechanization of the proof in detail, giving reference to theorems contained in an appendix. Some weak points of the experiment with respect to a natural treatment of abstract algebraic reasoning give rise to a discussion of the use of module systems to represent abstract algebra in theorem provers. Drawing from that, we present tentative ideas for further research into a section concept for Isabelle.     

同步数据流语言输入结构体的可信翻译

为最大程度地减少同步数据流语言编译过程中由编译器引入的错误,需要利用形式化方法自动生成代码,保证编译器产生的代码能够应用于核能仪控系统.本研究使用定理证明工具Coq,对同步数据流语言Lustre到Clight的主节点输入结构翻译阶段涉及的语法、语义及翻译算法进行了形式化定义,并完成翻译算法的形式化证明.研究表明这种经过形式化的编译器能够生成与源代码行为一致的可信目标代码,同时生成的目标代码能够很好满足核能仪控系统的执行规范.     

Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL

Correctness of compilers is a vital precondition for the correctness of the software translated by them. In this paper, we present two approaches for the formalization of static single assignment (SSA) form together with two corresponding formal proofs in the Isabelle/HOL system, each showing the correctness of code generation. Our comparison between the two proofs shows that it is very important to find adequate formalizations in formal proofs since they can simplify the verification task considerably. Our formal correctness proofs do not only verify the correctness of a certain class of code generation algorithms but also give us sufficient, easily checkable correctness criteria characterizing correct compilation results obtained from implementations (compilers) of these algorithms. These correctness criteria can be used in a compiler result checker.     

字节码虚拟机的构造和验证

提出一种虚拟机构造和验证方案.给出字节码程序运行环境BVM(bytecode virtual machine)的形式化定义;采用X86机器语言构造虚拟机CertVM(certified virtual machine);并证明该虚拟机实现符合相应程序规范并和BVM之间具有模拟关系.利用辅助工具Coq给出证明,所有证明均可机器自动检查.CertVM确保在硬件环境满足其语义规范的情况下,已验证的字节码程序能够在给定虚拟机环境中正常运行.给出的方案不仅为虚拟机验证提供理论基础,而且为可信软件构造提供了一种有益的尝试.     

Certified Quantum Computation in Isabelle/HOL

In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch’s algorithm, the Deutsch–Jozsa algorithm and the quantum Prisoner’s Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.

     

Semantics,calculi, and analysis for object-oriented specifications

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.     

A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle

We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt; rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.     

Natural deduction as higher-order resolution

An interactive theorem prover, Isabelle, is under development. In lcf, each inference rule is represented by one function for forwards proof and another (a tactic) for backwards proof. In Isabelle, each inference rule is represented by a Horn clause. Resolution gives both forwards and backwards proof, supporting a large class of logics. Isabelle has been used to prove theorems in Martin-Löf's constructive type theory. Quantifiers pose several difficulties: substitution, bound variables, Skolemization. Isabelle's representation of logical syntax is the typed λ-calculus, requiring higher-order unification. It may have potential for logic programming. Depth-first subgoaling along inference rules constitutes a higher-order PROLOG.