OBJ as a Theorem Prover with Applications to Hardware Verification

1989 ◽  
pp. 219-267 ◽  
Author(s):  
Joseph A. Goguen
Keyword(s):  
Hardware Verification ◽  
Theorem Prover

scholarly journals Higher-order theorem proving and its applications

2019 ◽  
Vol 61 (4) ◽  
pp. 187-191
Author(s):  
Alexander Steen
Keyword(s):  
Theorem Proving ◽  
Formal Analysis ◽  
Logical Consequence ◽  
Effective Means ◽  
Industrial Applications ◽  
Higher Order ◽  
Hardware Verification ◽  
Theorem Prover ◽  
Computer Assisted ◽  
Higher Order Logic

Abstract Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.

scholarly journals Michael John Caldwell Gordon. 28 February 1948—22 August 2017

2018 ◽  
Vol 65 ◽  
pp. 89-113
Author(s):  
Lawrence C. Paulson
Keyword(s):  
Programming Languages ◽  
Interactive Theorem Proving ◽  
Hardware Verification ◽  
Theorem Prover ◽  
Probabilistic Algorithms ◽  
Higher Order Logic ◽  
Functional Programming Languages ◽  
And Mathematics ◽  
Tools And Techniques ◽  
Hardware Designs

Michael Gordon was a pioneer in the field of interactive theorem proving and hardware verification. In the 1970s, he had the vision of formally verifying system designs, proving their correctness using mathematics and logic. He demonstrated his ideas on real-world computer designs. His students extended the work to such diverse areas as the verification of floating-point algorithms, the verification of probabilistic algorithms and the verified translation of source code to correct machine code. He was elected to the Royal Society in 1994, and he continued to produce outstanding research until retirement. His achievements include his work at Edinburgh University helping to create Edinburgh LCF, the first interactive theorem prover of its kind, and the ML family of functional programming languages. He adopted higher-order logic as a general formalism for verification, showing that it could specify hardware designs from the gate level right up to the processor level. It turned out to be an ideal formalism for many problems in computer science and mathematics. His tools and techniques have exerted a huge influence across the field of formal verification.

Evaluation Opportunities in Mechanized Theories

10.29007/7kx8 ◽  
2018 ◽  
Author(s):  
Joe Hurd
Keyword(s):  
Mathematical Theory ◽  
Theorem Prover ◽  
Mechanized Mathematics ◽  
Reasoning Tasks

This invited talk will look at logic solvers through the application lens of constructing and processing a theory library of mechanized mathematics. In fact, constructing and processing theories are two distinct applications, and each will be considered in turn. Construction is carried out by formalizing a mathematical theory using an interactive theorem prover, and logic solvers can remove much of the drudgery by automating common reasoning tasks. At the theory library level, logic solvers can provide assistance with theory engineering tasks such as compressing theories, managing dependencies, and constructing new theories from reusable theory components.

CSim 2

2021 ◽  
Vol 43 (1) ◽  
pp. 1-46
Author(s):  
David Sanan ◽  
Yongwang Zhao ◽  
Shang-Wei Lin ◽  
Liu Yang
Keyword(s):  
Programming Languages ◽  
Concurrent Systems ◽  
Theorem Prover ◽  
Compositional Techniques ◽  
Machine Code ◽  
Top Down ◽  
Hol Theorem Prover ◽  
High Level ◽  
High Degree

To make feasible and scalable the verification of large and complex concurrent systems, it is necessary the use of compositional techniques even at the highest abstraction layers. When focusing on the lowest software abstraction layers, such as the implementation or the machine code, the high level of detail of those layers makes the direct verification of properties very difficult and expensive. It is therefore essential to use techniques allowing to simplify the verification on these layers. One technique to tackle this challenge is top-down verification where by means of simulation properties verified on top layers (representing abstract specifications of a system) are propagated down to the lowest layers (that are an implementation of the top layers). There is no need to say that simulation of concurrent systems implies a greater level of complexity, and having compositional techniques to check simulation between layers is also desirable when seeking for both feasibility and scalability of the refinement verification. In this article, we present CSim 2 a (compositional) rely-guarantee-based framework for the top-down verification of complex concurrent systems in the Isabelle/HOL theorem prover. CSim 2 uses CSimpl, a language with a high degree of expressiveness designed for the specification of concurrent programs. Thanks to its expressibility, CSimpl is able to model many of the features found in real world programming languages like exceptions, assertions, and procedures. CSim 2 provides a framework for the verification of rely-guarantee properties to compositionally reason on CSimpl specifications. Focusing on top-down verification, CSim 2 provides a simulation-based framework for the preservation of CSimpl rely-guarantee properties from specifications to implementations. By using the simulation framework, properties proven on the top layers (abstract specifications) are compositionally propagated down to the lowest layers (source or machine code) in each concurrent component of the system. Finally, we show the usability of CSim 2 by running a case study over two CSimpl specifications of an Arinc-653 communication service. In this case study, we prove a complex property on a specification, and we use CSim 2 to preserve the property on lower abstraction layers.

Structural ambiguity in Montague Grammar and categorial grammar

2015 ◽  
Vol 32 (1) ◽  
Author(s):  
Glyn Morrill
Keyword(s):  
Categorial Grammar ◽  
Theorem Prover ◽  
Montague Grammar ◽  
Structural Ambiguity

AbstractWe give a type logical categorial grammar for the syntax and semantics of Montague's seminal fragment, which includes ambiguities of quantification and intensionality and their interactions, and we present the analyses assigned by a parser/theorem prover CatLog to the examples in the first half of Chapter 7 of the classic text

Sign in / Sign up

Export Citation Format

Share Document