Search

In Mizar, unlike in most other proof assistants, the types are not part of the foundations of the system. Mizar is based on untyped set theory, which means that in Mizar expressions are typed but the values of those expressions are not. In this paper we present the Mizar type system as a collection of type inference rules. We will interpret Mizar types as soft types, by translating Mizar's type judgments into sequents of untyped first order predicate logic. We will then prove that the Mizar type system is correct with respect to this translation in the sense that each derivable type judgment translates to a provable sequent. [ABSTRACT FROM AUTHOR]

We present a formal treatment of normalization by evaluation in type theory. The involved semantics of simply-typed λ-calculus is exactly the simply typed fragment of the type theory. This means we have constructed and proved correct a decompilation function which recovers the syntax of a program, provided it belongs to the simply typed fragment. The development runs and is checked in Coq. Possible applications include the formal treatment of languages with binders. [ABSTRACT FROM AUTHOR]

We present the generic system framework of Isabelle/Isar underlying recent versions of Isabelle. Among other things, Isar provides an infrastructure for Isabelle plug-ins, comprising extensible state components and extensible syntax that can be bound to tactical ML programs. Thus the Isabelle/Isar architecture may be understood as an extension and refinement of the traditional "LCF approach", with explicit infrastructure for building derivative systems. To demonstrate the technical potential of the framework, we apply it to a concrete formal methods tool: the HOL-Z 3.0 environment, which is geared towards the analysis of Z specifications and formal proof of forward-refinements. [ABSTRACT FROM AUTHOR]

This paper introduces the logical system HOL2P that extends classical higher order logic (HOL) with type operator variables and universal types. HOL2P has explicit term operations for type abstraction and type application. The formation of type application terms t [T] is restricted to small types T that do not contain any universal types. This constraint ensures the existence of a set-theoretic model and thus consistency. The expressiveness of HOL2P allows category-theoretic concepts such as natural transformations and initial algebras to be applied at the level of polymorphic HOL functions. The parameterisation of terms with type operators adds genericity to theorems. Type variable quantification can also be expressed. A prototype of HOL2P has been implemented on top of HOL-Light. Type inference is semi-automatic, and some type annotations are necessary. Reasoning is supported by appropriate tactics. The implementation has been used to check some sample derivations. [ABSTRACT FROM AUTHOR]

Elliptic curves are fascinating mathematical objects. In this paper, we present the way they have been represented inside the Coq system, and how we have proved that the classical composition law on the points is internal and gives them a group structure. We then describe how having elliptic curves inside a prover makes it possible to derive a checker for proving the primality of natural numbers. [ABSTRACT FROM AUTHOR]

This paper concerns the formal semantics of programming languages, and the specification and verification of software. We are interested in the verification of real programs, written in real programming languages, running on machines with real memory models. To this end, we verify a Caml implementation of a concurrent algorithm, Peterson's mutual exclusion algorithm, down to the operational semantics. The implementation makes use of Caml features such as higher order parameters, state, concurrency and nested general recursion. Our Caml model includes a datatype of expressions, and a small step reduction relation for programs (a Caml expression together with a store). We also develop a new proof of correctness for a modified version of Peterson's algorithm, designed to run on a machine with a weak memory. [ABSTRACT FROM AUTHOR]

We present an advanced modeling and verification toolbox for functional programs with state and exceptions. The toolbox integrates an extensible, monad-based, component model, a monad-based Hoare logic and weakest pre-condition calculus, and proof systems for temporal logic and bisimilarity. It is implemented in Isabelle/HOL using shallow embeddings and incorporates as much modeling and reasoning power as possible from Isabelle/HOL. We have validated the toolbox's usefulness in a substantial security protocol verification project. [ABSTRACT FROM AUTHOR]

We use the theorem prover Isabelle to formalise and machine-check results of the theory of generalised substitutions given by Dunne and used in the B method. We describe the model of computation implicit in this theory and show how this is based on a compound monad, and we contrast this model of computation and monad with those implicit in Dunne's theory of abstract commands. Subject to a qualification concerning frames, we prove, using the Isabelle/HOL theorem prover, that Dunne's results about generalised substitutions follow from the model of computation which we describe. [ABSTRACT FROM AUTHOR]

We discuss a proof of the wellfounded induction theorem for the ordinals up to ε0. The proof is performed on the embedding of ACL2 in HOL-4, thus providing logical justification for that embedding and supporting the claim that the ACL2 logic has a model. [ABSTRACT FROM AUTHOR]

Placing our result in a web of related mechanised results, we give a direct proof that the de Bruijn λ-calculus (à la Huet, Nipkow and Shankar) is isomorphic to an α-quotiented λ-calculus. In order to establish the link, we introduce an "index-carrying" abstraction mechanism over de Bruijn terms, and consider it alongside a simplified substitution mechanism. Relating the new notions to those of the α-quotiented and the proper de Bruijn formalisms draws on techniques from the theory of nominal sets. [ABSTRACT FROM AUTHOR]

We verify three decision procedures on context-free grammars utilized in a program analyzer for a server-side programming language. One of the procedures decides inclusion between a context-free language and a regular language. The other two decide decision problems related to the well-formedness and validity of XML documents. From its formalization, we generate executable code for a balancedness checking procedure and incorporate it into an existing program analyzer. [ABSTRACT FROM AUTHOR]

In this proof pearl, we demonstrate the power of higher-order encodings in the logical framework Twelf[PS99] by investigating proofs about an algorithmic specification of bounded subtype polymorphism, a problem from the POPLmark challenge [ABF + 05].. Our encoding and representation of the problem plays to the strengths of the logical framework LF. Higher-order abstract syntax is used to deal with issues of bound variables. More importantly, we exploit the full advantage of parametric and higher-order judgments. As a key benefit we get a tedious narrowing lemma, which must normally be proven separately, for free. Consequently, we obtain an extremely compact and elegant encoding of the admissibility of general transitivity and other meta-theoretic properties. [ABSTRACT FROM AUTHOR]

We describe an automatic, semantics preserving translation between HOL, the higher-order logic supported by the HOL4 theorem proving environment, and a deep embedding of the first order logic supported by ACL2. An implementation of this translation allows ACL2 to be used as a symbolic execution engine for functions defined in HOL. [ABSTRACT FROM AUTHOR]

Interactive proof assistants should verify the proofs they receive from automatic theorem provers. Normally this proof reconstruction takes place internally, forming part of the integration between the two tools. We have implemented source-level proof reconstruction: resolution proofs are automatically translated to Isabelle proof scripts. Users can insert this text into their proof development or (if they wish) examine it manually. Each step of a proof is justified by calling Hurd's Metis prover, which we have ported to Isabelle. A recurrent issue in this project is the treatment of Isabelle's axiomatic type classes. [ABSTRACT FROM AUTHOR]

We reexamine the While combinator of higher-order logic (HOL) and introduce the For combinator. We argue that both combinators should be part of the toolbox of any HOL practitioner, not only because they make efficient computations within HOL possible, but also because they facilitate elegant inductive reasoning about loops. We present two examples that support this argument. [ABSTRACT FROM AUTHOR]

Formal, modular, and mechanized verification of realistic systems code is desirable but challenging. Verification of machine context management (a basis of multi-tasking) is one representative example. With context operations occurring hundreds to thousands of times per second on every computer, their correctness deserves careful examination. Given the small and stable code bases, it is a common misunderstanding that the context management code is suitable for informal scrutiny and testing. Unfortunately, after being extensively studied and used for decades, it still proves to be a common source of bugs and confusion. Yet its verification remains difficult due to the machine-level detail, irregular patterns of control flows, and rich application scenarios. This paper reports our experience applying XCAP—a recent theoretical verification framework—to certify a realistic x86 implementation of machine context management. XCAP supports expressive and modular logical specifications, but has only previously been applied on simple idealized machine and code. By applying the XCAP theory to an x86 machine model, building libraries of common proof tactics and lemmas, composing specifications for the context data structures and routines, and proving that the code behave accordingly, we achieved the first formal, modular, and mechanized verification of realistic x86 context management code. Our proofs are fully mechanized in the Coq proof assistant. Our certified library code runs on stock hardware and can be linked with other certified systems and application code. Our technique applies to other variants or extensions of context management (e.g., more complex context, different platforms), provides a solid basis for further verification of thread implementation and concurrent programs, and illustrates how to achieve formal, modular, and mechanized verification of realistic systems code. [ABSTRACT FROM AUTHOR]

This paper introduces the concept of controlled automation as a balanced medium between high-level automated reasoning and low-level primitive tactics in HOL. We created a new tactic that subsumes many existing low-level tactics for logical operations and three new tactics that simplify common uses of term rewriting: definition expansion, simplification, and equational rewriting. To implement the tactics, we extended HOL with a facility to label assumptions and operate uniformly on both goals and assumptions. We select automatically and predictably which low-level tactic to apply by examining the structure of the selected assumption or goal. A simple and uniform set of hints enable users to provide the minimal information needed to guide the tactics. We performed two case studies and achieved a 60% reduction in the number of unique tactics used. [ABSTRACT FROM AUTHOR]

Terminator is a static analysis tool developed by Microsoft Research for proving termination of Windows device drivers written in C. This proof pearl describes a formalization in higher order logic of the program analysis employed by Terminator, and verifies that if the analysis succeeds then program termination logically follows. [ABSTRACT FROM AUTHOR]

The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a family of logical formalisms for representing and reasoning about conceptual and terminological knowledge. Among these, the logic $\mathcal{ALC\,}$is a ground DL used in many practical cases. Moreover, the Semantic Web appears as a new field for the application of formal methods, that could be used to increase its reliability. A starting point could be the formal verification of satisfiability provers for DLs. In this paper, we present the PVS specification of a prover for $\mathcal{ALC\,}$, as well as the proofs of its termination, soundness and completeness. We also present the formalization of the well-foundedness of the multiset relation induced by a well-founded relation. This result has been used to prove the termination and the completeness of the $\mathcal{ALC\,}$ prover. [ABSTRACT FROM AUTHOR]

One of the most important concepts in probability theory is that of the expectation of a random variable, which basically summarizes the distribution of the random variable in a single number. In this paper, we develop the basic techniques for analyzing the expected values of discrete random variables in the HOL theorem prover. We first present a formalization of the expectation function for discrete random variables and based on this definition, the expectation properties of three commonly used discrete random variables are verified. Then, we utilize the definition of expectation in HOL to verify the linearity of expectation property, a useful characteristic to analyze the expected values of probabilistic systems involving multiple random variables. To demonstrate the usefulness of our approach, we verify the expected value of the Coupon Collector's problem within the HOL theorem prover. [ABSTRACT FROM AUTHOR]

Techniques based on sums of squares appear promising as a general approach to the universal theory of reals with addition and multiplication, i.e. verifying Boolean combinations of equations and inequalities. A particularly attractive feature is that suitable ‘sum of squares' certificates can be found by sophisticated numerical methods such as semidefinite programming, yet the actual verification of the resulting proof is straightforward even in a highly foundational theorem prover. We will describe our experience with an implementation in HOL Light, noting some successes as well as difficulties. We also describe a new approach to the univariate case that can handle some otherwise difficult examples. [ABSTRACT FROM AUTHOR]

In this paper, we present a formalisation of elementary group theory done in Coq. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way. [ABSTRACT FROM AUTHOR]

We propose a method to extract purely functional contents from logical inductive types in the context of the Calculus of Inductive Constructions. This method is based on a mode consistency analysis, which verifies if a computation is possible w.r.t. the selected inputs/outputs, and the code generation itself. We prove that this extraction is sound w.r.t. the Calculus of Inductive Constructions. Finally, we present some optimizations, as well as the implementation designed in the coq proof assistant framework. [ABSTRACT FROM AUTHOR]

We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination problems encountered in daily theorem proving practice. [ABSTRACT FROM AUTHOR]

We formalise the data race free (DRF) guarantee provided by Java, as captured by the semi-formal Java Memory Model (JMM) [1] and published in the Java Language Specification [2].The DRF guarantee says that all programs which are correctly synchronised (i.e., free of data races) can only have sequentially consistent behaviours. Such programs can be understood intuitively by programmers. Formalisation has achieved three aims. First, we made definitions and proofs precise, leading to a better understanding; our analysis found several hidden inconsistencies and missing details. Second, the formalisation lets us explore variations and investigate their impact in the proof with the aim of simplifying the model; we found that not all of the anticipated conditions in the JMM definition were actually necessary for the DRF guarantee. This allows us to suggest a quick fix to a recently discovered serious bug [3] without invalidating the DRF guarantee. Finally, the formal definition provides a basis to test concrete examples, and opens the way for future work on JMM-aware logics for concurrent programs. [ABSTRACT FROM AUTHOR]

cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to cminor and from cminor to machine language. We have redesigned cminor so that it is suitable for Hoare Logic reasoning and we have designed a Separation Logic for cminor. In this paper, we give a small-step semantics (instead of the big-step of the proved-correct compiler) that is motivated by the need to support future concurrent extensions. We detail a machine-checked proof of soundness of our Separation Logic. This is the first large-scale machine-checked proof of a Separation Logic w.r.t. a small-step semantics. The work presented in this paper has been carried out in the Coq proof assistant. It is a first step towards an environment in which concurrent cminor programs can be verified using Separation Logic and also compiled by a proved-correct compiler with formal end-to-end correctness guarantees. [ABSTRACT FROM AUTHOR]

Algorithms that process geometric objects become more and more important for many safety-critical embedded systems, e.g. for motion planning or collision detection, where correctness is indispensable. The main challenge to demonstrating correctness is the consistent handling of degenerate cases like collinear line segments. In this paper, we therefore propose the use of an interactive theorem prover to develop dependable geometry algorithms for safety-critical embedded systems. Our solution is based on the use of a three-valued logic to make degenerate cases explicit. Using the theorem prover, we are not only able to prove the correctness of the obtained algorithms, but also to directly derive a software library of provably correct geometry algorithms for safety-critical applications. [ABSTRACT FROM AUTHOR]

Many safety-critical systems deal with geometric objects. Reasoning about the correctness of such systems is mandatory and requires the use of basic definitions of geometry for the specification of these systems. Despite the intuitive meaning of such definitions, their formalisation is not at all straightforward: In particular, degeneracies lead to situations where none of the Boolean truth values adequately defines a geometric primitive. Therefore, we use a three-valued logic for the definition of geometric primitives to explicitly handle such degenerate cases. We have implemented a three-valued library of linear geometry in an interactive theorem prover for higher order logic which allows us to specify and verify entire algorithms of computational geometry. [ABSTRACT FROM AUTHOR]

In embedded systems, safety and reliability are usually important quality characteristics. It is required to determine these properties including hardware and software. Many techniques have been proposed to analyze, model and predict software and hardware quality characteristics on a quantified basis, e.g. fault trees, Markov analysis, and statistical reliability models. [ABSTRACT FROM AUTHOR]

During the past three decades, many formal methods have been proposed whose goal is to improve the quality of computer systems. I use the term formal method to refer to any mathematically-based technique or tool useful in either hardware or software development. Recently, formal methods have played a significantly increased role in hardware design. More and more companies that sell microprocessors and hardware chips, including Intel, IBM, and Motorola, are using formally-based tools, such as model checkers, theorem provers, and equivalence checkers, to check hardware designs for flaws. While applied less frequently in practical software development, formal methods have, in a few recent cases, also been effective in detecting software defects. A prominent example is the set of tools developed in Microsoft's SLAM project which were designed to detect flaws in device drivers [1], a primary source of software defects in Microsoft programs. In 2006, Microsoft released the Static Driver Verifier (SDV) as part of Windows Vista, the latest Microsoft operating system. SDV uses the SLAM model checker to detect cases in which device drivers linked to Vista violate one of a set of interface rules. [ABSTRACT FROM AUTHOR]