Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...
Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...
Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...
Programming with monads can be advantageous even in imperative languages with builtin support for side effects. However, in these languages composing monadic programs is different from composing side effecting imperative programs. This does not need to be ...
We present an automated approach to verify the correctness of programming assignments, such as the ones that arise in a functional programming course. Our approach takes as input student submissions and reference solutions, and uses equivalence checking to ...
Programming has changed; programming languages have not.
Modern software embraced reusable software components, i.e., public libraries, and runs in the cloud, on machines that co-locate applications from various origins.
This new programming paradigm leads ...
Software network functions (NFs), such as a network address translator, load balancer, or proxy,
promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs.
However, continuous updates and flexibility typically c ...
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...
In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language.
Our system is based on a dependently-typed language and an algorithmic type checking procedure
which ensures total correctness. We rely on SMT solve ...
Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...
