Scalable Verification of Imperative Programs

Deductive verification is a subdiscipline of computer science which ensures software reliability and safety by formally modeling and proving program behavior. It is currently difficult to apply by non-experts and scales badly with program size and complexity. Pluggable type systems, which annotate variables and sub-programs with types that describe their expected values and behavior, offer a light-weight alternative, offering more scalability and ease-of-use for less expressiveness and precision. Based on our previous research, we aim to develop a formal link between these two approaches, which allows programmers to use type systems where possible and formal verification where necessary to obtain formal safety guarantees for their software. We also aim to implement our approach based on existing verification tools for the Java programming language and to evaluate our approach on realistic programs with mutable data structures, which are so far not amenable to scalable formal treatment.

Faculty Supervisor:

Werner Dietl

Student:

Partner:

Karlsruher Institut für Technologie

Discipline:

Computer science

Sector:

Education

University:

University of Waterloo

Program: