TY - BOOK

T1 - Towards Modular Reasoning for Stateful and Concurrent Programs

AU - Krogh-Jespersen, Morten

PY - 2019/1/16

Y1 - 2019/1/16

N2 - Software is an integral part of our everyday lives and we rely on man-written programs to solve a wide range of problems. Ensuring that programs solve well-defined problems satisfactory can be accomplished by the art of software verification, i.e. formal reasoning about the program in some mathematically founded model. However, formal reasoning about real-world programs is well known to be difficult because of the advanced programming language features used when writing them.The main objective of this dissertation is to develop state-of-the-art models that allow for verification of programs using advanced language features such as (1) higher-order functions, (2) higher-order store (general references) and (3) concurrency. Conceptually, languages with store and concurrency are extremely hard to reason about because threads may race when trying to read and update references. Technically, reasoning about such languages formally require sophisticated mathematical models and some notion of ownership and invariants.In this dissertation we present a relational model for reasoning about a con- current, higher-order language with general references, where all references are tracked by a type-and-effect system. The model validates data-abstraction by masking effects and parallelizing expressions if effects are suitable dis- joint. Masking stateful effects can in pure languages be done monadically as well. In this dissertation we further present a logical relations model that semantically verifies that runST, the run-function of the ST monad, provides proper encapsulation of state for real-world implementations. Finally, we also present Aneris, a logical framework for writing and reasoning about distributed systems. Aneris allow for node-local reasoning and each node can have local state and concurrency. We show that the framework is suitable for verifying distributed systems by verifying a broad range of interesting examples.

AB - Software is an integral part of our everyday lives and we rely on man-written programs to solve a wide range of problems. Ensuring that programs solve well-defined problems satisfactory can be accomplished by the art of software verification, i.e. formal reasoning about the program in some mathematically founded model. However, formal reasoning about real-world programs is well known to be difficult because of the advanced programming language features used when writing them.The main objective of this dissertation is to develop state-of-the-art models that allow for verification of programs using advanced language features such as (1) higher-order functions, (2) higher-order store (general references) and (3) concurrency. Conceptually, languages with store and concurrency are extremely hard to reason about because threads may race when trying to read and update references. Technically, reasoning about such languages formally require sophisticated mathematical models and some notion of ownership and invariants.In this dissertation we present a relational model for reasoning about a con- current, higher-order language with general references, where all references are tracked by a type-and-effect system. The model validates data-abstraction by masking effects and parallelizing expressions if effects are suitable dis- joint. Masking stateful effects can in pure languages be done monadically as well. In this dissertation we further present a logical relations model that semantically verifies that runST, the run-function of the ST monad, provides proper encapsulation of state for real-world implementations. Finally, we also present Aneris, a logical framework for writing and reasoning about distributed systems. Aneris allow for node-local reasoning and each node can have local state and concurrency. We show that the framework is suitable for verifying distributed systems by verifying a broad range of interesting examples.

M3 - Ph.D. thesis

BT - Towards Modular Reasoning for Stateful and Concurrent Programs

PB - Aarhus Universitet

CY - Aarhus

ER -