Dimovski, Aleksandar, 1977- (2007) Compositional software verification based on game semantics. PhD thesis, University of Warwick.

Preview

PDF WRAP_THESIS_Dimovski_2007.pdf - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader Download (10Mb)

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 or Dissertation (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
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:	pdf
Extent:	200 leaves : ill., charts
Language:	eng
URI:	http://wrap.warwick.ac.uk/id/eprint/2398

Request changes to a record

Actions (login required)

View Item