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: