UNSPECIFIED (1998) Program abstraction in a higher-order logic framework. In: 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 98), SEP 27-OCT 01, 1998, CANBERRA, AUSTRALIA.

Full text not available from this repository.

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.

Item Type:	Conference Item (UNSPECIFIED)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Series Name:	LECTURE NOTES IN COMPUTER SCIENCE
Journal or Publication Title:	THEOREM PROVING IN HIGHER ORDER LOGICS
Publisher:	SPRINGER-VERLAG BERLIN
ISBN:	3-540-64987-5
ISSN:	0302-9743
Editor:	Grundy, J and Newey, M
Date:	1998
Volume:	1479
Number of Pages:	16
Page Range:	pp. 33-48
Publication Status:	Published
Title of Event:	11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 98)
Location of Event:	CANBERRA, AUSTRALIA
Date(s) of Event:	SEP 27-OCT 01, 1998
URI:	http://wrap.warwick.ac.uk/id/eprint/14244

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item