Sciweavers

Share
TPHOL
1998
IEEE

Program Abstraction in a Higher-Order Logic Framework

8 years 7 months ago
Program Abstraction in a Higher-Order Logic Framework
Abstraction in a Higher-Order Logic Framework Marco Benini Sara Kalvala Dirk Nowotka Department of Computer Science University of Warwick, Coventry, CV4 7AL, United Kingdom 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.
Marco Benini, Sara Kalvala, Dirk Nowotka
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where TPHOL
Authors Marco Benini, Sara Kalvala, Dirk Nowotka
Comments (0)
books