The Library
Compositional software verification based on game semantics
Tools
Dimovski, Aleksandar (2007) Compositional software verification based on game semantics. PhD thesis, University of Warwick.
|
PDF
WRAP_THESIS_Dimovski_2007.pdf - Requires a PDF viewer. Download (10Mb) |
Official URL: http://webcat.warwick.ac.uk/record=b2232072~S15
Abstract
One of the major challenges in computer science is to put programming on a firmer mathematical basis, in order to improve the correctness of computer programs. Automatic program verification is acknowledged to be a very hard problem, but current work is reaching the point where at least the foundational�· aspects of the problem can be addressed and it is becoming a part of industrial software development. This thesis presents a semantic framework for verifying safety properties of open sequ;ptial programs. The presentation is focused on an Algol-like programming language that embodies many of the core ingredients of imperative and functional languages and incorporates data abstraction in its syntax. Game semantics is used to obtain a compositional, incremental way of generating accurate models of programs. Model-checking is made possible by giving certain kinds of concrete automata-theoretic representations of the model. A data-abstraction refinement procedure is developed for model-checking safety properties of programs with infinite integer types. The procedure starts by model-checking the most abstract version of the program. If no counterexample, or a genuine one, is found, the procedure terminates. Otherwise, it uses a spurious counterexample to refine the abstraction for the next iteration. Abstraction refinement, assume-guarantee reasoning and the L* algorithm for learning regular languages are combined to yield a procedure for compositional verification. Construction of a global model is avoided using assume-guarantee reasoning and the L* algorithm, by learning assumptions for arbitrary subprograms. An implementation based on the FDR model checker for the CSP process algebra demonstrates practicality of the methods.
Item Type: | Thesis (PhD) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Library of Congress Subject Headings (LCSH): | Computer programs -- Verification -- Research, Programming (Mathematics) -- Research, Game theory -- Computer programs, Model-driven software architecture, Abstraction | ||||
Official Date: | July 2007 | ||||
Dates: |
|
||||
Institution: | University of Warwick | ||||
Theses Department: | Department of Computer Science | ||||
Thesis Type: | PhD | ||||
Publication Status: | Unpublished | ||||
Supervisor(s)/Advisor: | Lazić, Ranko ; Jurjinski, Marcin | ||||
Sponsors: | Engineering and Physical Sciences Research Council (Great Britain) (EPSRC) ; Overseas Research Students Award Scheme (ORSAS) | ||||
Format of File: | |||||
Extent: | 200 leaves : ill., charts | ||||
Language: | eng |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year