Inductive assertions and operational semantics

Author: Moore, J.

Source: International Journal on Software Tools for Technology Transfer, Volume 8, Numbers 4-5, August 2006 , pp. 359-371(13)

Publisher: Springer

Buy & download fulltext article:

OR

Price: $47.00 plus tax (Refund Policy)

Abstract:

This paper shows how classic inductive assertions can be used in conjunction with a formal operational semantics to prove partial correctness properties of programs. The method imposes only the proof obligations that would be produced by a verification condition generator – but does not require the definition of a verification condition generator. All that is required is a theorem prover, a formal operational semantics, and the object program with appropriate assertions at user-selected cut points. The verification conditions are generated in the course of the theorem-proving process by straightforward symbolic evaluation of the formal operational semantics. The technique is demonstrated by proving the partial correctness of simple bytecode programs with respect to a preexisting operational model of the Java Virtual Machine.

Keywords: JVM; Software verification; Theorem proving; Verification condition

Document Type: Research Article

DOI: http://dx.doi.org/10.1007/s10009-005-0180-2

Affiliations: Email: Moore@cs.utexas.edu

Publication date: August 1, 2006

Related content

Key

Free Content
Free content
New Content
New content
Open Access Content
Open access content
Subscribed Content
Subscribed content
Free Trial Content
Free trial content

Text size:

A | A | A | A
Share this item with others: These icons link to social bookmarking sites where readers can share and discover new web pages. print icon Print this page