The Library
Verification and abstraction of flow-graph programs with pointers and computed jumps
Tools
Tools
Tools
Wahab, Matthew (1998) Verification and abstraction of flow-graph programs with pointers and computed jumps. University of Warwick. Department of Computer Science. (Department of Computer Science research report). (Unpublished)
|
PDF (Department of Computer Science Research Report)
WRAP_cs-rr-354.pdf - Other - Requires a PDF viewer. Download (431Kb) | Preview |
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.
| Item Type: | Report | ||||
|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
| Library of Congress Subject Headings (LCSH): | Assembly languages (Electronic computers) | ||||
| Series Name: | Department of Computer Science research report | ||||
| Publisher: | University of Warwick. Department of Computer Science | ||||
| Official Date: | 9 November 1998 | ||||
| Dates: |
|
||||
| Number: | Number 354 | ||||
| Number of Pages: | 49 | ||||
| DOI: | CS-RR-354 | ||||
| Institution: | University of Warwick | ||||
| Theses Department: | Department of Computer Science | ||||
| Status: | Not Peer Reviewed | ||||
| Publication Status: | Unpublished | ||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
