Bringing Formal Verification into Widespread Programming Language Ecosystems

Formal verification is a powerful tool for ensuring program correctness but is often hard to learn to use and has not yet spread into the commercial world. This thesis focuses on finding an easy-to-use solution to make formal verification available in popular programming language ecosystems. We propose a solution where users can write code in an...

Practical Verification of Concurrent Haskell Programs

The formal verification of concurrent programs is of particular importance, because concurrent programs are notoriously difficult to test. Because Haskell is a purely functional language, it is relatively easy to reason about the correctness of such programs and write down manual proofs. However, since these methods are still prone to error,...

Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures

Dynamic Binary Translation (DBT) is a powerful approach to support cross-architecture emulation of unmodified binaries. However, DBT systems face correctness and performance challenges, when emulating concurrent binaries from strong to weak memory consistency architectures. As a matter of fact, we report several translation errors in QEMU,...

Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs

Equational reasoning based verification address some of the limitations of classical testing. The Curry-Howard correspondence shows a direct link between type systems and mathematical logic based proofs. Agda is a language with totality and dependent types which makes use of the CH isomorphism to support equational reasoning in its programs. ...

Formal guarantees on controller performance for autonomous vehicles during highway lane changing manoeuvres

Annually over 60.000 people die and another 3.7 million get injured in car accidents in the United States and Europe combined. Automation of vehicles can reduce the number of accidents by 90%. Therefore, it is of great interest in academia and industry. For the automated vehicles that are being presented in industry however, proofs of safe...

Traffic Characterization of Aperiodic Control Systems

In networked systems, particularly over wireless or shared channels, the scarcity of communication resources makes the application of traditional control strategies with periodic sampling problematic. Alternative approaches with aperiodic sampling, such as: event triggered control and self triggered control, have been recently proposed to reduce...

Adaptive and Sequential Gridding Procedures for the Abstraction and Verification of Stochastic Processes

This work is concerned with the generation of finite abstractions of general state-space processes to be employed in the formal verification of probabilistic properties by means of automatic techniques such as probabilistic model checkers. The work employs an abstraction procedure based on the partitioning of the state-space, which generates a...

Model checking GOAL agents

This thesis presents a novel approach to model checking of agent programs written in an agent programming language. The language we consider is GOAL. The novelty of the approach is that we implement model checking algorithms from scratch on top of the standard language interpreter. In contrast, in the literature on agent program verification,...