Runtime Verification

Fall 2020

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.

This course is in Beta. CS 6156 is a brand new course. Everything might change. Nothing is certain.

 

News  


Lectures:
 Tuesday/Thursday
 3:00pm -- 4:15pm
 Online

Instructor:
 Owolabi Legunsen
 legunsen@cornell.edu

 Office Hours:
 After class
 Held online on Zoom
 (Link is on Piazza)

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 20%
  • There will be 4 -- 6 homework assignments.
  • Students must work individually on each homework and submit on CMS by the due date.
  • Each student may request to submit one homework late, no questions asked.
  • The lowest homework grade will be dropped for those students who make a good-faith effort on all homework by submitting something credible and on time.
Readings 20%
  • Readings to complement the discussions will be noted in the schedule.
  • Students will review assigned readings and summarize them in up to 500 words.
  • Summaries will respond to provided prompts and will be due by 11:59pm AOE the day before class, on CMS.
  • Students may skip or submit late up to 3 summaries without penalty. After that, each skip or late submission will decrease the grade by 3%.
  • Submitting all summaries on time will result in 3% of extra credit.
Presentations 10%
  • Students will lead the discussion of one research paper and they will present their final project.
  • Schedule a meeting with Owolabi a week before your presentation.
  • Submit a final version of the slides to Owolabi 48 hours before class.
  • Discussion leads are not required to summarize the assigned reading for that day.
Project 50%
  • To be completed individually or in self-selected pairs.
  • Students working in pairs will get the same scores and their project scope will be approximately double that of students who work alone.
  • We will discuss possible projects in class 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 brief reports submitted after each meeting with the instructor and on a more detailed final project report:
    • Project proposal (1 page): 5%
    • Two project reports (up to 2 pages each) of progress, problems, and plans: 15%
    • Final report (up to 5 pages): 30%

 

Tentative Schedule  


Date Topic Leader Reading Notes
9/3
Introduction
Owolabi
 slides
9/8
Events, traces, and properties
Owolabi
 slides,
 demo
Text: Bartocci+18
Prompt: questions
Homework-0 is assigned
9/10
Safety properties and monitoring
Owolabi
 slides
Text: Rosu12, pages 1--8
Prompt: questions
9/15
Program instrumentation
Owolabi
 slides,
examples
Texts: Intro, Nusayr+09
Prompt: questions
Homework-0 is due
9/17
Course project discussion
Owolabi
slides
Texts: Griswold, Shaw03
Prompt: questions
Optional reading: Halle+17
9/22
Past-time LTL monitor synthesis
BL
Text: Havelund+02
Prompt: questions
9/24
LTL monitor synthesis
Owolabi
slides
Text: Rosu+05
Prompt: instructions+questions
9/29
ERE monitor synthesis
VHA
Text: Sen+03
Prompt: questions
10/1
CFG monitor synthesis
CE
Text: Meredith+08
Prompt: questions
10/6
Parametric trace slicing and monitoring
BG
Text: Chen+09
Prompt: questions
Project proposal is due
10/8
Efficient parametric monitoring
WK
Text: Chen+09b
Prompt: questions
10/13
Garbage collection of monitors
DP
Text: Jin+11
Prompt: questions
10/15
Simultaneous monitoring of multiple specifications
TD
Text: Luo+14
Prompt: questions
10/20
Specification mining
NR
Text: Gabel+08
Prompt: questions
10/22
Specification quality
ZB
Text: Legunsen+16
Prompt: questions
10/27
Improving specification quality
YA
Text: Gabel+12
Prompt: questions
Project phase 1 report is due.
Homework-1 is assigned.
10/29
Scaling RV using static analysis
SG
Text: Bodden+07
Prompt: questions
11/3
Scaling RV using evolution awareness
LA & DF
Texts: Legunsen+15, Legunsen+19
Prompt: questions
11/5
Guest Lecture
Grigore Rosu
Text: None
Prompt: questions
Homework-1 is due.
11/10
Scaling RV using program transformations
SY
Text: Purandare+10
Prompt: questions
Homework-2 has been assigned.
11/12
FPGA-assisted RV
LYH
Text: Lu+07
Prompt: questions
11/17
No class (Semi-Finals week)
Homework-2 is due. Reading 21 is assigned.
11/19
No class (Semi-Finals week)
Project phase 2 report is due
11/24
No class (Semi-Finals week)
Reading 21 response is due.
11/26
No class (Thanksgiving)
12/1
Project presentations (1)

Optional Reading: Arnold+08
Prompt: questions
12/3
Project presentations (2)

Optional Reading: Havelund12
Prompt: questions
12/8
Project presentations (3)

Optional Reading: Purandare+13
Prompt: questions
Homework-3 has been assigned.
12/10
Project presentations (4)

Optional Reading: Hussein+12
Prompt: questions
12/15
Course wrap-up

Optional Reading: Havelund+19
Prompt: questions
Homework-3 is due.
12/17
No class (Finals Week)
Project final report is due
 

Course Resources  

Course Administration

  • Announcements will be posted on the course web page. Check the news section regularly for updates.
  • We will use Piazza as an online discussion forum.
  • We are using the course management system, CMS.

Project Reports

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

Sources

  • Some readings will 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: