@phdthesis{
    thesisPr06,
    author = "Preoteasa, Viorel",
    school = "Turku Centre for Computer Science",
    title = "Program Variables -- The Core of Mechanical Reasoning about Imperative Programs",
    abstract = {Imperative programming languages are widely used in practice in most of the software development projects. Examples of such languages include C, C++, C#, Java, Pascal, and many more. This thesis is concerned with reasoning about imperative programs. We study both refinement (the construction of correct programs starting from specifications) and correctness (an already written program is proved correct against a pre, post-condition specification), and we provide theorem prover support for reasoning about programs. Although extensive work has been done in the area of program verification, we are still far from expecting software developers to use it routinely in practice. This is justified by the fact that verification methods are very expensive to use when developing programs. In this thesis, we address some problems that occur when one formalizes the semantics of a programming language for mechanical verification purposes. In order to tackle such issues, we introduce a predicate transformer semantics for an imperative programming language and we give a shallow embedding of it in the PVS theorem prover. We treat local variables, mutually recursive procedures, and pointers. In our embedding, program variables can have any type whose cardinal is bounded by an arbitrary fixed cardinal. For pointers, we use two models: one in which they are modeled as functions from addresses to values, and another one based on separation logic. We propose refinement rules and Hoare total correctness rules for local variables and pointer statements, and also for mutually recursive procedures. The Hoare rules are proved correct with respect to the predicate transformer semantics mentioned above. Various examples show our theory at work. <p> More details about the PVS implementation can be found <a href="../thesis">here</a>.},
    month = "November",
    flags = "copy",
    year = "2006",
    pdf = "thesis.pdf",
    type = "{PhD} Thesis"
}