Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2008 | Buch

Twenty Years of Theorem Proving for HOLs Past, Present and Future Kapitel lesen Erstes Kapitel lesen

Theorem Proving in Higher Order Logics

21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings

herausgegeben von: Otmane Ait Mohamed, César Muñoz, Sofiène Tahar

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008, held in Montreal, Canada, in August 2008. The 17 revised full papers presented together with 1 proof pearl (concise and elegant presentations of interesting examples), 5 tool presentations, and 2 invited papers were carefully reviewed and selected from 40 submissions. The papers cover all aspects of theorem proving in higher order logics as well as related topics in theorem proving and verification such as formal semantics of specification, modeling, and programming languages, specification and verification of hardware and software, formalisation of mathematical theories, advances in theorem prover technology, as well as industrial application of theorem provers.

Inhaltsverzeichnis

Frontmatter

Invited Papers

Twenty Years of Theorem Proving for HOLs Past, Present and Future
Abstract
There are two kinds of theorem provers for higher order logics: fully automatic (e.g. TPS and Leo) and user guided (e.g. HOL4, HOL Light, ProofPower, Isabelle/HOL, Coq, Nuprl and PVS). All the user guided systems, except PVS, are based on the LCF “fully expansive” approach invented by Robin Milner. PVS evolved from a different tradition that doesn’t expand everything down to primitive inferences.
The emphasis here is on user guided proof assistants, but future developments in automatic higher order proof methods are likely to be incorporated into these as the automatic methods available today are mainly propositional or first order.
Mike Gordon
Will This Be Formal?
Abstract
While adding formal methods to traditional software development processes can provide very high levels of assurance and reduce costs by finding errors earlier in the development cycle, there are at least four criteria that should be considered before introducing formal methods into a project. This paper describes five successful examples of the use of formal methods in the development of high integrity systems and discusses how each project satisfied these criteria.
Steven P. Miller

Tutorials

A Short Presentation of Coq
Abstract
The Coq proof assistant has been developed at INRIA, Ecole Normale Supérieure de Lyon, and University of Paris South for more than twenty years [6]. Its theoretical foundation is known as the “Calculus of Inductive Constructions” [4,5]. Versions of the system were distributed regularly from 1989 (version 4.10). The current revision is 8.1 and a revision 8.2 is about to come out. This 8th generation was started in 2004, at the time when a radical change in syntax was enforced and a textbook [2] was published. A more complete historical overview, provided by G. Huet and C. Paulin-Mohring, is available in the book foreword.
The calculus of Inductive constructions is a variant of typed lambda-calculus based on dependent types. Theorems are directly represented by terms of the lambda-calculus, in the same language that is also used to describe formulas and programs. Having all elements of the logic at the same level makes it possible to mix computation and theorem proving in productive ways.
Yves Bertot
An ACL2 Tutorial
Abstract
We describe a tutorial that demonstrates the use of the ACL2 theorem prover. We have three goals: to enable a motivated reader to start on a path towards effective use of ACL2; to provide ideas for other interactive theorem prover projects; and to elicit feedback on how we might incorporate features of other proof tools into ACL2.
Matt Kaufmann, J Strother Moore
A Brief Overview of PVS
Abstract
PVS is now 15 years old, and has been extensively used in research, industry, and teaching. The system is very expressive, with unique features such as predicate subtypes, recursive and corecursive datatypes, inductive and coinductive definitions, judgements, conversions, tables, and theory interpretations. The prover supports a combination of decision procedures, automatic simplification, rewriting, ground evaluation, random test case generation, induction, model checking, predicate abstraction, MONA, BDDs, and user-defined proof strategies. In this paper we give a very brief overview of the features of PVS, some illustrative examples, and a summary of the libraries and PVS applications.
Sam Owre, Natarajan Shankar
A Brief Overview of HOL4
Abstract
The HOLF proof assistant supports specification and proof in classical higher order logic. It is the latest in a long line of similar systems. In this short overview, we give an outline of the HOLF system and how it may be applied in formal verification.
Konrad Slind, Michael Norrish
The Isabelle Framework
Abstract
Isabelle, which is available from http://isabelle.in.tum.de , is a generic framework for interactive theorem proving. The Isabelle/Pure meta-logic allows the formalization of the syntax and inference rules of a broad range of object-logics following the general idea of natural deduction [32,33]. The logical core is implemented according to the well-known “LCF approach” of secure inferences as abstract datatype constructors in ML [16]; explicit proof terms are also available [8]. Isabelle/Isar provides sophisticated extra-logical infrastructure supporting structured proofs and specifications, including concepts for modular theory development. Isabelle/HOL is a large application within the generic framework, with plenty of logic-specific add-on tools and a large theory library. Other notable object-logics are Isabelle/ZF (Zermelo-Fraenkel set-theory, see [34,36] and Isabelle/HOLCF [26] (Scott’s domain theory within HOL). Users can build further formal-methods tools on top, e.g. see [53].
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow

Regular Papers

A Compiled Implementation of Normalization by Evaluation
Abstract
We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.
Klaus Aehlig, Florian Haftmann, Tobias Nipkow
LCF-Style Propositional Simplification with BDDs and SAT Solvers
Abstract
We improve, in both a logical and a practical sense, the simplification of the propositional structure of terms in interactive theorem provers. The method uses Binary Decision Diagrams (BDDs) and SAT solvers. We present experimental results to show that the time cost is acceptable.
Hasan Amjad
Nominal Inversion Principles
Abstract
When reasoning about inductively defined predicates, such as typing judgements or reduction relations, proofs are often done by inversion, that is by a case analysis on the last rule of a derivation. In HOL and other formal frameworks this case analysis involves solving equational constraints on the arguments of the inductively defined predicates. This is well-understood when the arguments consist of variables or injective term-constructors. However, when alpha-equivalence classes are involved, that is when term-constructors are not injective, these equational constraints give rise to annoying variable renamings. In this paper, we show that more convenient inversion principles can be derived where one does not have to deal with variable renamings. An interesting observation is that our result relies on the fact that inductive predicates must satisfy the variable convention compatibility condition, which was introduced to justify the admissibility of Barendregt’s variable convention in rule inductions.
Stefan Berghofer, Christian Urban
Canonical Big Operators
Abstract
In this paper, we present an approach to describe uniformly iterated “big” operations, like \(\sum_{i=0}^n f(i)\) or max i ∈ I f(i) and to provide lemmas that encapsulate all the commonly used reasoning steps on these constructs.
We show that these iterated operations can be handled generically using the syntactic notation and canonical structure facilities provided by the Coq system. We then show how these canonical big operations played a crucial enabling role in the study of various parts of linear algebra and multi-dimensional real analysis, as illustrated by the formal proofs of the properties of determinants, of the Cayley-Hamilton theorem and of Kantorovitch’s theorem.
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca
A Type of Partial Recursive Functions
Abstract
Our goal is to define a type of partial recursive functions in constructive type theory. In a series of previous articles, we studied two different formulations of partial functions and general recursion. We could obtain a type only by extending the theory with either an impredicative universe or with coinductive definitions. Here we present a new type constructor that eludes such entities of dubious constructive credentials. We start by showing how to break down a recursive function definition into three components: the first component generates the arguments of the recursive calls, the second evaluates them, and the last computes the output from the results of the recursive calls. We use this dissection as the basis for the introduction rule of the new type constructor. Every partial recursive function is associated with an inductive domain predicate; evaluation of the function requires a proof that the input values satisfy the predicate. We give a constructive justification for the new construct by interpreting it into the base type theory. This shows that the extended theory is consistent and constructive.
Ana Bove, Venanzio Capretta
Formal Reasoning About Causality Analysis
Abstract
Systems that can immediately react to their inputs may suffer from cyclic dependencies between their actions and the corresponding trigger conditions. For this reason, causality analysis has to be employed to check the constructiveness of the programs which implies the existence of unique and consistent behaviours. In this paper, we describe the embedding of various views of causality analysis into the HOL4 theorem prover to check their equivalence. In particular, we show the equivalence between the classical analysis procedure, which is based on a fixpoint computation, and a formulation as a (bounded) model checking problem.
Jens Brandt, Klaus Schneider
Imperative Functional Programming with Isabelle/HOL
Abstract
We introduce a lightweight approach for reasoning about programs involving imperative data structures using the proof assistant Isabelle/HOL. It is based on shallow embedding of programs, a polymorphic heap model using enumeration encodings and type classes, and a state-exception monad similar to known counterparts from Haskell. Existing proof automation tools are easily adapted to provide a verification environment. The framework immediately allows for correct code generation to ML and Haskell. Two case studies demonstrate our approach: An array-based checker for resolution proofs, and a more efficient bytecode verifier.
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews
HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
Abstract
Boogie is a program verification condition generator for an imperative core language. It has front-ends for the programming languages C# and C enriched by annotations in first-order logic.
Its verification conditions — constructed via a wp calculus from these annotations — are usually transferred to automated theorem provers such as Simplify or Z3. In this paper, however, we present a proof-environment, HOL-BoogieP, that combines Boogie with the interactive theorem prover Isabelle/HOL. In particular, we present specific techniques combining automated and interactive proof methods for code-verification.
We will exploit our proof-environment in two ways: First, we present scenarios to ”debug” annotations (in particular: invariants) by interactive proofs. Second, we use our environment also to verify ”background theories”, i.e. theories for data-types used in annotations as well as memory and machine models underlying the verification method for C.
Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff
Secure Microkernels, State Monads and Scalable Refinement
Abstract
We present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. We achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties.
We report on our experience in applying the techniques in an extensive (100,000 lines of proof) case study—the formal verification of an executable model of the seL4 operating system microkernel.
David Cock, Gerwin Klein, Thomas Sewell
Certifying a Termination Criterion Based on Graphs, without Graphs
Abstract
Although graphs are very common in computer science, they are still very difficult to handle for proof assistants as proving properties of graphs may require heavy computations. This is a problem when it comes to issues such as the certification of a proof of well-foundedness, since premises of generic theorems involving graph properties may be at least as difficult to prove as their conclusion. We define a framework and propose an original approach based on both shallow and deep embeddings for the mechanical certification of these kinds of proofs without the help of any graph library. This framework actually avoids concrete models of graphs and handles those implicitly. We illustrate this approach on a powerful refinement of the dependency pairs approach for proving termination. This refinement makes heavy use of graph analysis and our technique is powerful enough to deal efficiently –and with full automation– with graphs containing thousands of arcs, as they may occur in practice.
Pierre Courtieu, Julien Forest, Xavier Urbain
Lightweight Separation
Abstract
Lightweight separation is a novel approach to automatic reasoning about memory updates in pointer programs. It replaces the spatial formulae of separation logic, which complicate automation, by independent assertions about the memory content and the memory layout. As a result, assertions about the content can be treated by existing reasoners. The effect of memory updates is evaluated using specialized tactics that prove disjointness of memory regions from a given memory layout.
Holger Gast
Real Number Calculations and Theorem Proving
Validation and Use of an Exact Arithmetic
Abstract
When handling proofs of properties in the real world we often need to assert that one numeric quantity is greater than another. When these numeric quantities are real-valued, it is often tempting to get out the calculator to calculate the values of the expressions and then enter the results directly into the theorem prover as “facts” or axioms, since formally proving the desired properties can often be very tiresome. Obviously, such a procedure poses a few risks.
An alternative approach, presented in this paper, is to prove the correctness of an arbitrarily accurate calculator for the reals. If this calculator is expressed in terms of the underlying integer arithmetic operations of the theorem-prover’s implementation language, then there is a reasonable expectation that a practical evaluator of real-valued expressions may have been constructed.
Obviously, there are some constraints imposed by computability theory. It is well known, for example, that it is not possible to determine the sign of a computable real in finite time. We show that for all practical purposes, we need not worry about such fussy details. After all, mathematicians have – throughout the centuries – been prepared to make such calculations without being overly punctilious about the computability of the operations they were performing!
We report on the experience of validating and using a real number calculator in PVS.
David R Lester
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
Abstract
Correctness of many hybrid and distributed systems require stability and convergence guarantees. Unlike the standard induction principle for verifying invariance, a theory for verifying stability or convergence of automata is currently not available. In this paper, we formalize one such theory proposed by Tsitsiklis [27]. We build on the existing PVS metatheory for untimed, timed, and hybrid input/output automata, and incorporate the concepts about fairness, stability, Lyapunov-like functions, and convergence. The resulting theory provides two sets of sufficient conditions, which when instantiated and verified for particular automata, guarantee convergence and stability, respectively.
Sayan Mitra, K. Mani Chandy
Certified Exact Transcendental Real Number Computation in Coq
Abstract
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implemented a library for reasoning and computing with complete metric spaces in the Coq proof assistant and used this library to build a constructive real number implementation including elementary real number functions and proofs of correctness. Using this library, I have created a tactic that automatically proves strict inequalities over closed elementary real number expressions by computation.
Russell O’Connor
Formalizing Soundness of Contextual Effects
Abstract
A contextual effect system generalizes standard type and effect systems: where a standard effect system computes the effect of an expression e, a contextual effect system additionally computes the prior and future effect of e, which characterize the behavior of computation prior to and following, respectively, the evaluation of e. This paper describes the formalization and proof of soundness of contextual effects, which we mechanized using the Coq proof assistant. Contextual effect soundness is an unusual property because the prior and future effect of a term e depends not on e itself (or its evaluation), but rather on the evaluation of the context in which e appears. Therefore, to state and prove soundness we must “match up” a subterm in the original typing derivation with the possibly-many evaluations of that subterm during the evaluation of the program, in a way that is robust under substitution. We do this using a novel typed operational semantics. We conjecture that our approach could prove useful for reasoning about other properties of derivations that rely on the context in which that derivation appears.
Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks, Iulian Neamtiu
First-Class Type Classes
Abstract
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for specifying with abstract structures by quantification on contexts. However, both systems are limited by second-class implementations of these constructs, and these limitations are only overcomed by ad-hoc extensions to the respective systems. We propose an embedding of type classes into a dependent type theory that is first-class and supports some of the most popular extensions right away. The implementation is correspondingly cheap, general and integrates well inside the system, as we have experimented in Coq. We show how it can be used to help structured programming and proving by way of examples.
Matthieu Sozeau, Nicolas Oury
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
Abstract
Slicing is a widely-used technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correctness of slicing, which should ideally be proven independent of concrete programming languages and with the help of well-known verifying techniques such as proof assistants. As a first step in this direction, this contribution presents a framework for dynamic slicing based on control flow and program dependence graphs and machine checked in Isabelle/HOL. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and well-formedness properties.
Daniel Wasserrab, Andreas Lochbihler

Proof Pearls

Proof Pearl: Revisiting the Mini-rubik in Coq
Abstract
The Mini-Rubik is the 2x2x2 version of the famous Rubik’s cube. How many moves are required to solve the 3x3x3 cube is still unknown. The Mini-Rubik, being simpler, is always solvable in a maximum of 11 moves. This is the result that is formalised in this paper. From this formalisation, a solver is also derived inside the Coq prover. This rather simple example illustrates how safe computation can be used to do state exploration in order to derive non-trivial properties inside a prover.
Laurent Théry
Backmatter
Metadaten
Titel
Theorem Proving in Higher Order Logics
herausgegeben von
Otmane Ait Mohamed
César Muñoz
Sofiène Tahar
Copyright-Jahr
2008
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-71067-7
Print ISBN
978-3-540-71065-3
DOI
https://doi.org/10.1007/978-3-540-71067-7

Premium Partner

    Bildnachweise