In a modern society we interact with software on a daily basis. We use software not only when we use our personal computers or mobile phones, but also when we drive our cars or watch television. It is not far-fetched to say that our lives rely on the correct functioning of critical software operating in satellites, aircrafts, medical equipment and power stations, among others. To ensure the correctness of such software, which is often extremely complex, a rigorous framework is needed in which properties can be expressed, analysed, and ultimately verified. Program analysis combined with formal methods provides a set of mathematical techniques that allow us to rigorously specify and verify properties.
This thesis presents a number of program analysis techniques and frameworks that aid in proving programs correct. It covers both functional properties, i.e., related to the concrete behaviour of a software system, as well as non-functional properties, i.e., concerning the overall system.
Part 1 presents three different problems that are tackled using the PVS proof assitant. The fist one is modelling a real-world preemptive microkernel. Our model of concurrent threads is well suited for programs with preemption points, i.e. atomic blocks of code. It allows us to reason using techniques for sequential programs. We are able to prove properties related to the absence of deadlock and to uncover a bug. The second one is describing properties of Java programs as security automata and translating these properties into JML annotations such that if the property is breached, an exception is triggered. We are able to formalize the tranlation algorith and prove it correct. This involves formalizing a substantial subset of the semantincs sequential Java programs. And the third one is modelling the semantics of an object-oriented language and studying the effects that assignments can have on recursive data structures. We obtain rules that describe how a path on the heap can be affected by an assignment and we apply these rules to prove, without using induction, the correctness of a reverse list algorithm.
Part 2 is concerned with resource analysis. First we introduce a size-aware type system for a first-order functional language that allows us to check size annotations in fuctions. The annotations relate the size of the output to the size of the inputs. It supports algebraic data types, but only of matrix-like structures, e.g. a complete binary tree. We cope with this restriction in the last chapter at the cost of increasing the complexity of the type checking algorithm and reducing the decidability classes.