The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
This paper presents a method for translating a subset of VDM-SL to higher order logic, more specifically the PVS specification language. This method has been used in an experiment where we have taken three existing, relatively large specifications written in VDM-SL, hand-translated these to PVS and then tried to type check the results. This is not as simple as it may sound since the specifications...
We compare formalizations of an example from elementary category theory in the systems HOL (an implementation of Church’s classical simple type theory) and ALF (an implementation of Martin-Löf’s intuitionistic type theory). The example is a proof of coherence for monoidal categories which was extracted from a proof of normalization for monoids. It makes essential use of the identification of proofs...
Formal Synthesis is a methodology developed at Kent for combining circuit design and verification. We have reinterpreted this methodology in Isabelle’s theory of higher-order logic so that circuits are synthesized using higher-order resolution. Our interpretation simplifies and extends Formal Synthesis both conceptually and in implementation. It also supports integration of this development...
Much of the work on verifying software has been done on simple, often artificial, languages or subsets of existing languages to avoid difficult details. In trying to verify a secure application written in C, we have encountered and overcome some semantically complicated uses of the language. We present inference rules for assignment statements with pre- and post-evaluation side effects and...
Cryptographic protocols are sequences of message exchanges, usually involving encryption, intended to establish secure communication over insecure networks. Whether they actually do so is a notoriously subtle question. This paper describes a proof procedure that automatically proves desired properties of cryptographic protocols, using a HOL formalization of a “belief logic” extending that...
A graph-based method for automatically synthesizing liveness proofs of non-finite concurrent systems is described. The implemented procedure is a significant extension of a previous mechanization of TLA[Lam94] in a higher-order logic theorem prover [Bus95].
The refinement calculus provides a theory for the stepwise refinement of programs and this theory has been formalised in HOL. TkWinHOL is a powerful graphical user interface (GUI) that can be used to drive the HOL window Library. In this paper, we describe a tool called the Refinement Calculator which combines TkWinHOL and the HOL Refinement Calculus theory, to provide support for formal program development...
This paper describes a system to support reasoning about lazy functional programs. The system is based on a combination of a deep embedding of the language in HOL with a set of proof tools to raise the level of interaction with the theorem prover. This approach allows metatheoretic reasoning about the semantics and reasoning about undefined programs while still supporting practical reasoning about...
We present several approaches to verifying a class of circuits with the Coq proof-assistant, using the example of a left-to-right comparator. The large capacity of expression of the Calculus of Inductive Constructions allows us to give precise and general specifications. Using Coq’s higher order logic, we state general results useful in establishing the correctness of the circuits. Finally, exploiting...
This paper presents the formalization of some elements of mathematical analysis using the PVS verification system. Our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discusses their merits and effectiveness. We conclude...
This article describes the embedding of high level synthesis algorithms in HOL. For given standard synthesis steps, we describe, how its data can be mapped to terms in HOL and the synthesis process be expressed by means of a logical derivation. In contrast to post-synthesis verification techniques our approach is constructive in a sense that the proof is derived during synthesis rather than “guessed”...
We present five axioms of name-carrying lambda-terms identified up to alpha-conversion—that is, up to renaming of bound variables. We assume constructors for constants, variables, application and lambda-abstraction. Other constants represent a function Fv that returns the set of free variables in a term and a function that substitutes a term for a variable free in another term. Our axioms are (1)...
The majority of general purpose mechanised proof assistants support versions of typed higher order logic, even though set theory is the standard foundation for mathematics. For many applications higher order logic works well and provides, for specification, the benefits of type-checking that are well-known in programming. However, there are areas where types get in the way or seem unmotivated. Furthermore,...
The HOL theorem prover is implemented in the LCF manner. All inference is ultimately reduced to a collection of very simple (forward) primitive inference rules, but by programming it is possible to build alternative means of proving theorems on top, while preserving security. Existing HOL proofs styles are, however, very different from those used in textbooks. Here we describe the addition of another...
Stålmarck’s algorithm is a patented technique for tautology-checking which has been used successfully for industrial-scale problems. Here we describe the algorithm and explore its implementation as a HOL derived rule.
A compositional proof method allows the components of a system to be specified and verified independently, instead of having to verify the entire system as a monolithic unit. This paper describes how the composition principle of Abadi and Lamport can be applied to specify and compose systems that consist of both safety and progress properties, using the HOL theorem proving system. We discuss the translation...
We present a modular embedding of Unity in Coq. Special care has been put on the representation of Unity programs and on the logic used. To keep elimination of invariants and composability of safety properties, we introduce a notion of context. The definition of progress is strengthened so that we can keep progress properties when programs are composed. This is a generalization of the ad’hoc notion...
Nuprl and HOL are both tactic-based interactive theorem provers for higher-order logic, and both have been used in many substantial applications over the last decade. However, the HOL community has accumulated a much larger collection of formalized mathematics of the kind useful for hardware and software verification. Nuprl’s relative lack impedes its application to verification problems of real practical...
We present a semantic representation of the core concepts of the specification language Z in higher-order logic. Although it is a “shallow embedding” like the one presented by Bowen and Gordon, our representation preserves the structure of a Z specification and avoids expanding Z schemas. The representation is implemented in the higher-order logic instance of the generic theorem prover Isabelle. Its...
This paper reports on work to alleviate the problem that high-level synthesis tools cannot in general produce results that are comparable in quality to manual design. We propose to use pre-synthesis transformations of algorithmic input specifications to improve the quality of the synthesis. By mechanising transformational reasoning about specifications as interactive theorem-proving in a proof system...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.