Program abstraction in a higher-order logic framework.

Tools

Benini, Marco, Kalvala, Sara and Nowotka, Dirk (1998) Program abstraction in a higher-order logic framework. [Paper] In: Theorem Proving in Higher Order Logics (TPHOLs). , 27 Sep - 1 Oct 1998, Canberra, Australia . Theorem Proving in Higher Order Logics. ; pp. 33-48 . DOI 10.1007/BFb0055128. Lecture Notes in Computer Science .

[thumbnail of ProgAbstract.pdf]
Preview
 Text
ProgAbstract.pdf
Download (168kB) | Preview

Supplementary data:

Abstract

We present a hybrid approach to program verification: a higher-order logic, used as a specification language, and a human-driven proof environment, with a process-algebraic engine to allow the use of process simulation as an abstraction technique. The domain of application is the validation of object code, and our intent is to adapt and mix existing formalisms to make the verification of representative programs possible. In this paper, we describe the logic in question and an underlying semantics given in terms of a process algebra.

Document Type: Conference or Workshop Item (Paper)
Keywords: formal verification higher-order logic process algebra automated theorem prover
Research affiliation: Kiel University
Publisher: Springer
Date Deposited: 15 Feb 2013 21:52
Last Modified: 23 Sep 2019 17:14
URI: https://oceanrep.geomar.de/id/eprint/20537

Actions (login required)

View Item View Item