Scalable Verification of Imperative Programs

  • Partner:

    University of Waterloo

Deductive verification is a subdiscipline of computer science concerned with ensuring software reliability and safety by formally modeling and proving program behavior. This kind of verification is 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, but they trade scalability and ease-of-use for expressiveness and precision. We developed a formal link between these two approaches, which allows programmers to use type systems where possible and deductive verification where necessary to obtain formal safety guarantees for their software. We also implemented this combined approach based on existing verification tools for the Java programming language.