<%@ page language="java" contentType="text/html" %> <%-- Include common initialisation code --%> <%@ include file="/arch/common.jsp" %> <%-- The current tab --%> <% String currentTab = "Research"; %> <%-- Content of navigation pane --%> <%@ include file="nav.jsp" %> <% showCurrentLink=true; %> <%-- Current navigation location --%> <% String currentNav = "Reports and Theses"; %> <%-- Include the code for the document header --%> <%@ include file="/arch/header.jsp" %>

Research Report CS-RR-354

<%-- Include the code for the lines and navigation --%> <%@ include file="/arch/middle.jsp" %>

M. Wahab, Verification and Abstraction of Flow-Graph Programs with Pointers and Computed Jumps (November 9, 1998).

Abstract

A flow-graph language which includes a simultaneous assignment, pointers and computed jumps is developed. The language is expressive enough that sequential composition can be defined as a function on commands, constructing a single command from its arguments. This allows the abstraction of a program to be constructed from the program text. This form of abstraction is the reverse of compilation: the abstraction of a program is also a program. The sequential composition operator can reduce the number of commands which must be considered when verifying a program. This provides a method for simplifying program verification. Proof rules are defined for reasoning about the liveness properties of flow-graph programs. The language is expressive enough to describe sequential object code programs and a program for the Alpha AXP processor is verified as an example.

Download

cs-rr-354.ps.gz

<%-- Include the code for the document footer --%> <%@ include file="/arch/footer.jsp" %>