Verification of Concurrent Object-Oriented Programs

  • Rustan Leino ,
  • Peter Müller, (ETH Zurich)

Published by Microsoft Research

Software engineering research

  • Goal
    • Better build, maintain, and understand programs
  • How?
    • Specifications
    • Tools, tools, tools
      • Program semantics
      • Verification-condition generation, symbolic execution, model checking, abstract interpretation, fuzzing, test generation
      • Satisfiability Modulo Theories (SMT)