Runtime Verification

Spring 2022

Runtime Verification is a lightweight formal method for checking program executions against specifications. Foundations, algorithms, and tools for major approaches to runtime verification will be covered, including monitor synthesis, specification languages, parametric monitoring, monitorability, instrumentation, and static analysis for reducing runtime verification overhead. Students will become familiar with recent research results and challenges in runtime verification, gain experience with runtime verification tools, and conduct a research project.

Prerequisites. Graduate standing (Ph.D, MS, or MEng) in CS or CS majors with CS 3110 grade of B+ or better. Experience with Java programming will be helpful for programming assignments.

 

News  

  • 1/2/2022: The website is up!


Lectures:
 Tuesday/Thursday
 2:45 -- 4:00pm
 Bard Hall 140

Instructor:
 Owolabi Legunsen
 legunsen@cornell.edu

 Office Hours:
 Wed 1:30-2:30pm
 Fri 2:00-3:00pm

Assessment  

This is a research-oriented software engineering course. It will include lectures, reading research papers, homeworks, in-class discussions, and a research project. Final course grades are based on the following:

Activity Grade Details
Homeworks 5%
  • There will be 2 -- 3 homework assignments.
  • Students must work individually on each homework and submit on Canvas by the due date.
Readings and in-class participation 10%
  • Readings to complement in-class discussions will be noted in the schedule.
  • Students will review assigned readings and add 2-3 unique questions to a shared document.
  • Questions will be due by 11:59pm AOE the day before class, on the shared document.
  • Students may skip or submit questions late for up to 3 times without penalty. After that, each skip or late submission will result in a 0 grade for that reading.
Presentations and discussion lead 15%
  • Students will lead the discussion of one research paper and they will present their final project.
  • Schedule a meeting with Owolabi a week before you are due to lead a paper discussion.
  • Discussion leads do not have to submit questions for the paper that they are in charge of.
Project 70%
  • To be completed individually or in self-selected pairs.
  • We will discuss possible projects early in the semester.
  • There will be mandatory project meetings with the instructor: once in the beginning to discuss potential topics and project scope, and two meetings to keep track of project progress.
  • Project grade will be based on the quality of the progress made, rather than on the length of the reports. Each project phase will attract the following proportions of the total course grade :
    • Project proposal (500 words or less): 6%
    • Two project reports (up to 1 page each) of progress, problems, and plans: 24%
    • Final report (up to 2 pages): 40%

 

Tentative Schedule  


Date Topic Leader Reading Notes
1/25
Introduction
 Owolabi
 slides
1/27
Demo, Reading Software Engineering Papers
 Owolabi
 slides		 Texts: Griswold, Shaw03
2/1
The Basics: Events, Traces, Properties
 Owolabi
 slides		 Text: Bartocci+18
2/3
The Basics: Part II
 Owolabi
 slides		 Text: Bartocci+18
2/8
Discussion: Intro to RV
 Owolabi
 slides		 Text: Bartocci+18
2/10
Safety Properties and Monitoring I
 Owolabi
 slides		 Text: Rosu'12
2/15
Safety Properties and Monitoring II
 Owolabi
 slides		 Text: Rosu'12
2/17
Program Instrumentation with ASM
 Owolabi
 slides		 Code: ASM
2/22
Program Instrumentation with AspectJ
 Owolabi
 slides		 Code: AspectJ
2/24
LTL Monitor Synthesis
 Owolabi
 slides		 Text: Rosu+Havelund'04
3/1
Break (No class)
3/3
LTL Monitor Synthesis II
 Owolabi
 slides		 Text: Rosu+Havelund'04
3/8
CFG Monitor Synthesis
 GK Text: Meredith+08
3/10
SRS Monitor Synthesis
 MQ Text: Meredith+Rosu'13
3/15
Parametric trace slicing and monitoring
 SB Text: Chen+Rosu'09
3/17
Monitor Garbage Collection
 PS Text: Jin+11
3/22
Specification Mining
 MT Text: Gabel+Su'08
3/24
Survey of Specification Mining
 Owolabi Text: Robillard+'13
3/29
On RV Specification Quality
 Owolabi Text: Legunsen+'16
3/31
Improving Specification Quality
 Owolabi Text: Gabel+Su'12
4/5
Spring Break (No Class)
4/7
Spring Break (No Class)
4/12
Hyperproperties
 MM Text: Clarkson+Schneider'08
4/14
Optimizing Runtime Verification I
 SBA Text: Purandare+'10
4/19
Optimizing Runtime Verification II
 Owolabi Text: Legunsen+'19
4/21
Project Clinic
 All
4/26
Project Presentation I
 TBD
4/28
Project Presentation II
 TBD
5/3
Project Presentation III
 TBD
5/5
Project Presentation IV
 TBD
5/10
Course Wrap-up
 Owolabi
 

Course Resources  

Course Administration

  • Announcements will be posted on the course web page. Check the news section regularly for updates.

Project Reports

This template may be used for preparing the various project reports.

Sources

  • Some readings may be assigned from a free, work-in-progress book on runtime verification and from publicly available research papers that will be linked in the schedule section.
  • There will be periodic homework assignments in Java. Instructions for installing Java and associated software can be found here.
  • Projects and homework will involve applying a runtime verification tool on open-source projects that use Maven as a build system. Brief introductions to Maven can be found here and here.
  • If you need to brush up on your Java skills, invest some time studying the following resources:

Runtime Verification

Community:
  • Runtime Verification -- A website about history, events, resources, and leadership in the broader runtime verification community.
(Our) Tools:  

General Resources  

Academic Integrity

Students are expected to know and abide by Cornell's policies on academic integrity, including: Academic integrity violations will be prosecuted aggressively. If you are not sure what constitutes an academic integrity violation, please ask.

Special Needs and Wellness

We provide accommodations for disabilities. Students with disabilities can contact Student Disability Services at 607-254-4545 or the instructor for a confidential discussion of their individual needs. If you experience personal or academic stress or need to talk to someone who can help, contact the instructor or: