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

2005 | Buch

On the Correctness of Operating System Kernels Kapitel lesen Erstes Kapitel lesen

Theorem Proving in Higher Order Logics

18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings

herausgegeben von: Joe Hurd, Tom Melham

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 volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22–25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005.

Inhaltsverzeichnis

Frontmatter

Invited Papers

On the Correctness of Operating System Kernels
Abstract
The Verisoft project aims at the pervasive formal verification of entire computer systems. In particular, the seamless verification of the academic system is attempted. This system consists of hardware (processor and devices) on top of which runs a microkernel, an operating system, and applications. In this paper we define the computation model CVM (communicating virtual machines) in which concurrent user processes interact with a generic microkernel written in C. We outline the correctness proof for concrete kernels, which implement this model. This result represents a crucial step towards the verification of a kernel, e.g. that in the academic system. We report on the current status of the formal verification.
Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, Wolfgang Paul
Alpha-Structural Recursion and Induction
(Extended Abstract)
Abstract
There is growing evidence for the usefulness of name permutations when dealing with syntax involving names and name-binding. In particular they facilitate an attractively simple formalisation of common, but often technically incorrect uses of structural recursion and induction for abstract syntax trees modulo α-equivalence. At the heart of this formalisation is the notion of finitely supported mathematical objects. This paper explains the idea in as concrete a way as possible and gives a new derivation within higher-order logic of principles of α-structural recursion and induction for α-equivalence classes from the ordinary versions of these principles for abstract syntax trees.
Andrew M. Pitts

Regular Papers

Shallow Lazy Proofs
Abstract
We show that delaying fully-expansive proof reconstruction for non-interactive decision procedures can result in a more efficient work-flow. In contrast with earlier work, our approach to postponed proof does not require making deep changes to the theorem prover.
Hasan Amjad
Mechanized Metatheory for the Masses: The PoplMark Challenge
Abstract
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?
We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F< :, a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
A Structured Set of Higher-Order Problems
Abstract
We present a set of problems that may support the development of calculi and theorem provers for classical higher-order logic. We propose to employ these test problems as quick and easy criteria preceding the formal soundness and completeness analysis of proof systems under development. Our set of problems is structured according to different technical issues and along different notions of semantics (including Henkin semantics) for higher-order logic. Many examples are either theorems or non-theorems depending on the choice of semantics. The examples can thus indicate the deductive strength of a proof system.
Christoph E. Benzmüller, Chad E. Brown
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
Abstract
This paper presents the formalization of an algorithm for slicing Java event spaces in PVS. In short, Java event spaces describe how multi-threaded Java programs operate in memory. We show that Java event spaces can be sliced following an algorithm introduced in previous work and still preserve properties in a subset of CTL. The formalization and proof presented in this paper can be extended to other state-space reduction techniques as long as some sufficient conditions are fulfilled.
Néstor Cataño
Proving Equalities in a Commutative Ring Done Right in Coq
Abstract
We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation.
Benjamin Grégoire, Assia Mahboubi
A HOL Theory of Euclidean Space
Abstract
We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is \({\mathbb R}^{N}\) with the usual notion of distance.) A notable feature is that the HOL type system is used to encode the dimension N in a simple and useful way, even though HOL does not permit dependent types. In the resulting theory the HOL type system, far from getting in the way, naturally imposes the correct dimensional constraints, e.g. checking compatibility in matrix multiplication. Among the interesting later developments of the theory are a partial decision procedure for the theory of vector spaces (based on a more general algorithm due to Solovay) and a formal proof of various classic theorems of topology and analysis for arbitrary N-dimensional Euclidean space, e.g. Brouwer’s fixpoint theorem and the differentiability of inverse functions.
John Harrison
A Design Structure for Higher Order Quotients
Abstract
The quotient operation is a standard feature of set theory, where a set is partitioned into subsets by an equivalence relation. We reinterpret this idea for higher order logic, where types are divided by an equivalence relation to create new types, called quotient types. We present a design to mechanically construct quotient types as new types in the logic, and to support the automatic lifting of constants and theorems about the original types to corresponding constants and theorems about the quotient types. This design exceeds the functionality of Harrison’s package, creating quotients of multiple mutually recursive types simultaneously, and supporting the equivalence of aggregate types, such as lists and pairs. Most importantly, this design supports the creation of higher order quotients, which enable the automatic lifting of theorems with quantification over functions of any higher order.
Peter V. Homeier
Axiomatic Constructor Classes in Isabelle/HOLCF
Abstract
We have definitionally extended Isabelle/HOLCF to support axiomatic Haskell-style constructor classes. We have subsequently defined the functor and monad classes, together with their laws, and implemented state and resumption monad transformers as generic constructor class instances. This is a step towards our goal of giving modular denotational semantics for concurrent lazy functional programming languages, such as GHC Haskell.
Brian Huffman, John Matthews, Peter White
Meta Reasoning in ACL2
Abstract
The ACL2 system is based upon a first-order logic and implements traditional first-order reasoning techniques, notably (conditional) rewriting, as well as extensions including mathematical induction and a “functional instantiation” capability for mimicking second-order reasoning. Additionally, one can engage in meta-reasoning — using ACL2 to reason, and prove theorems, about ACL2’s logic from within ACL2. One can then use these theorems to augment ACL2’s proof engine with custom extensions. ACL2 also supports forms of meta-level control of its rewriter. Relatively recent additions of these forms of control, as well as extensions to ACL2’s long-standing meta-reasoning capability, allow a greater range of rules to be written than was possible before, allowing one to specify more comprehensive proof strategies.
Warren A. Hunt Jr, Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
Reasoning About Java Programs with Aliasing and Frame Conditions
Abstract
Several tools exist for reasoning about Java programs annotated with JML specifications. A main issue is to deal with possible aliasing between objects and to handle correctly the frame conditions limiting the part of memory that a method is allowed to modify. Tools designed for automatic use (like ESC/Java) are not complete and even not necessarily correct. On the other side, tools which offer a full modeling of the program require a heavy user interaction for discharging proof obligations. In this paper, we present the modeling of Java programs used in the Krakatoa tool, which generates proof obligations expressed in a logic language suitable for both automatic and interactive reasoning. Using the Simplify automatic theorem prover, we are able to establish automatically more properties than static analysis tools, with a method which is guaranteed to be sound, assuming only the correctness of our logical interpretation of programs and specifications.
Claude Marché, Christine Paulin-Mohring
Real Number Calculations and Theorem Proving
Abstract
Wouldn’t it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this paper we outline how this can be done within a theorem proving framework. First, we formally establish upper and lower bounds for trigonometric and transcendental functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations can be performed in an algebraic setting. This pragmatic approach has been implemented as a strategy in PVS. The strategy provides a safe way to perform explicit calculations over real numbers in formal proofs.
César Muñoz, David Lester
Verifying a Secure Information Flow Analyzer
Abstract
Denotational semantics for a substantial fragment of Java is formalized by deep embedding in PVS, making extensive use of dependent types. A static analyzer for secure information flow for this language is proved correct, that is, it enforces noninterference.
David A. Naumann
Proving Bounds for Real Linear Programs in Isabelle/HOL
Abstract
Linear programming is a basic mathematical technique for optimizing a linear function on a domain that is constrained by linear inequalities. We restrict ourselves to linear programs on bounded domains that involve only real variables. In the context of theorem proving, this restriction makes it possible for any given linear program to obtain certificates from external linear programming tools that help to prove arbitrarily precise bounds for the given linear program. To this end, an explicit formalization of matrices in Isabelle/HOL is presented, and how the concept of lattice-ordered rings allows for a smooth integration of matrices with the axiomatic type classes of Isabelle.
As our work is a contribution to the Flyspeck project, we argue that with the above techniques it is now possible to prove bounds for the linear programs arising in the proof of the Kepler conjecture sufficiently fast.
Steven Obua
Essential Incompleteness of Arithmetic Verified by Coq
Abstract
A constructive proof of the Gödel-Rosser incompleteness theorem [9] has been completed using Coq proof assistant. Some theory of classical first-order logic over an arbitrary language is formalized. A development of primitive recursive functions is given, and all primitive recursive functions are proved to be representable in a weak axiom system. Formulas and proofs are encoded as natural numbers, and functions operating on these codes are proved to be primitive recursive. The weak axiom system is proved to be essentially incomplete. In particular, Peano arithmetic is proved to be consistent in Coq’s type theory and therefore is incomplete.
Russell O’Connor
Verification of BDD Normalization
Abstract
We present the verification of the normalization of a binary decision diagram (BDD). The normalization follows the original algorithm presented by Bryant in 1986 and transforms an ordered BDD in a reduced, ordered and shared BDD. The verification is based on Hoare logics and is carried out in the theorem prover Isabelle/HOL. The work is both a case study for verification of procedures on a complex pointer structure, as well as interesting on its own, since it is the first proof of functional correctness of the pointer based normalization process we are aware of.
Veronika Ortner, Norbert Schirmer
Extensionality in the Calculus of Constructions
Abstract
This paper presents a method to translate a proof in an extensional version of the Calculus of Constructions into a proof in the Calculus of Inductive Constructions extended with a few axioms. We use a specific equality in order to translate the extensional conversion relation into an intensional system.
Nicolas Oury
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
Abstract
We present a system of first order logic, together with soundness and completeness proofs wrt. standard first order semantics. Proofs are mechanised in Isabelle/HOL. Our definitions are computable, allowing us to derive an algorithm to test for first order validity. This algorithm may be executed in Isabelle/HOL using the rewrite engine. Alternatively the algorithm has been ported to OCaML.
Tom Ridge, James Margetson
A Generic Network on Chip Model
Abstract
We present a generic network on chip model (named GeNoC) intended to serve as a reference for the design and the validation of high level specifications of communication virtual modules. The definition of the model relies on three independent groups of constrained functions: routing and topology, scheduling, interfaces. The model identifies the sufficient constraints that these functions must satisfy in order to prove the correctness of GeNoC. Hence, one can concentrate his efforts on the design and the verification of one group. As long as the constraints are satisfied the overall system correctness is still valid. We show some concrete instances of GeNoC. One of them is a state-of-the-art network taken from industry.
Julien Schmaltz, Dominique Borrione
Formal Verification of a SHA-1 Circuit Core Using ACL2
Abstract
Our study was part of a project aiming at the design and verification of a circuit for secure communications between a computer and a terminal smart card reader. A SHA-1 component is included in the circuit. SHA-1 is a cryptographic primive that produces, for any message, a 160 bit message digest. We formalize the standard specification in ACL2, then automatically produce the ACL2 model for the VHDL RTL design; finally, we prove the implementation compliant with the specification. We apply a stepwise approach that proves theorems about each computation step of the RTL design, using intermediate digest functions.
Diana Toma, Dominique Borrione
From PSL to LTL: A Formal Validation in HOL
Abstract
Using the HOL theorem prover, we proved the correctness of a translation from a subset of Accellera’s property specification language PSL to linear temporal logic LTL. Moreover, we extended the temporal logic hierarchy of LTL that distinguishes between safety, liveness, and more difficult properties to PSL . The combination of the translation from PSL to LTL with already available translations from LTL to corresponding classes of ω-automata yields an efficient translation from PSL to ω-automata. In particular, this translation generates liveness or safety automata for corresponding PSL fragments, which is important for several applications like bounded model checking.
Thomas Tuerk, Klaus Schneider

Proof Pearls

Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2
Abstract
In this paper we present a formalization and proof of Higman’s Lemma in ACL2. We formalize the constructive proof described in [10] where the result is proved using a termination argument justified by the multiset extension of a well-founded relation. To our knowledge, this is the first mechanization of this proof.
Francisco J. Martín-Mateos, José L. Ruiz-Reina, José A. Alonso, Mariá J. Hidalgo
Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2
Abstract
We briefly describe a mechanically checked proof of Dijkstra’s shortest path algorithm for finite directed graphs with nonnegative edge lengths. The algorithm and proof are formalized in ACL2.
J. Strother Moore, Qiang Zhang
Proof Pearl: Defining Functions over Finite Sets
Abstract
Structural recursion over sets is meaningful only if the result is independent of the order in which the set’s elements are enumerated. This paper outlines a theory of function definition for finite sets, based on the fold functionals often used with lists. The fold functional is introduced as a relation, which is then shown to denote a function under certain conditions. Applications include summation and maximum. The theory has been formalized using Isabelle/HOL .
Tobias Nipkow, Lawrence C. Paulson
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof
Abstract
We discuss methods for dealing effectively with let-bindings in proofs. Our contribution is a small set of unconditional rewrite rules, found by the bracket abstraction translation from the λ-calculus to combinators. This approach copes with the usual HOL encodings of paired abstraction, ensures that bound variable names are preserved, and uses only conventional simplification technology.
Michael Norrish, Konrad Slind
Backmatter
Metadaten
Titel
Theorem Proving in Higher Order Logics
herausgegeben von
Joe Hurd
Tom Melham
Copyright-Jahr
2005
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-31820-0
Print ISBN
978-3-540-28372-0
DOI
https://doi.org/10.1007/11541868

Premium Partner

    Bildnachweise