Compositional software verification based on game semantics
Dimovski, Aleksandar, 1977- (2007) Compositional software verification based on game semantics. PhD thesis, University of Warwick.
WRAP_THESIS_Dimovski_2007.pdf - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Official URL: http://webcat.warwick.ac.uk/record=b2232072~S15
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|
|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|
Actions (login required)