Dynamic invariants for runtime verification

Potential supervisors: 
Description: 

An invariant is a property of a program’s state that is always true while the program executes. Invariants are fundamental for program analysis and verification, but inferring them statically -- from the program text -- is quite hard, and possible only in restricted scenarios. In contrast, dynamic invariant inference, popularized by the Daikon tool, tries to infer invariants by monitoring predicates of interests over a finite number of concrete program executions, typically in the form of tests. This makes it more widely applicable than static inference techniques, even if it comes with little or no guarantees of soundness.

In this project, you will implement dynamic invariant inference for Larva -- a runtime verification platform for Java programs. The basic technique will be based on the Daikon technique [1]. You will run experiment with your implementation on a number of case studies coming from the StarVoors tool for combined static/dynamic verification.

Related courses:

  • Testing, debugging and verification
  • Formal methods for software development

Related skills:

  • Good programming skills in object-oriented languages, especially Java
  • A basic knowledge of fundamental notions of verification (pre- and postconditions, and invariants)
  • An interest in verification technology

Reading and resources:

  1. The Daikon technique https://homes.cs.washington.edu/~mernst/pubs/daikon-tool-scp2007.pdf and tool https://plse.cs.washington.edu/daikon/
  2. The Larva runtime verification tool: http://www.cs.um.edu.mt/svrg/Tools/LARVA/
  3. The StarVoors verification tool: http://cse-212294.cse.chalmers.se/starvoors/

Contact: Gerardo Schneider (gersch@chalmers.se)

Date range: 
October, 2017 to October, 2022