CS598 - Runtime Verification (Spring 2017)

From FSL
Jump to: navigation, search

Students enrolled in this class are expected to check this web page regularly. Complete lecture notes will be posted here.

Course Description

Runtime verification (RV) is a software analysis approach where programs are formally analyzed as they execute. This can be done using program instrumentation, or using special execution environments (for example, a semantics-based symbolic execution engine), or both. In its most simplistic form, RV can be used to detect or predict bugs in programs. In a more sophisticated form, RV can be used to prove programs correct by systematically executing programs on all their (symbolic) paths. The course will cover the major RV approaches and techniques, as well as semantic foundations.

By the end of the course, students are expected to master the major RV approaches, at both the foundational and the algorithmic levels. They will also read and present papers on RV, and will likely do a (joint) project that falls at the intersection of their area of interest and RV. Since RV is a relatively new area, the course will also stimulate research ideas and possibly lead to some publications.

Meetings: W/F 14:00 - 15:15, 1131 Siebel Center
Credit: 4 credits
Professor: Grigore Rosu (Office: SC 2110)
Office hours: Held by Grigore Rosu in SC 2110; by appointment.

Lecture Notes, Useful Material

The links below provide you with useful material for this class, including complete lecture notes. These materials will be added by need.

  • Some runtime verification systems to try out:
  • JavaMOP (online) for monitor synthesis and runtime monitoring of safety properties
  • RV-Predict for predictive runtime analysis
  • RV-Match for semantics-based runtime verification
  • Safety and Monitoring Foundations 25px-Pdf_icon.png Book Draft Info_circle.png (version 1)
  • Safety Properties (Chapter 3), Monitoring (Chapter 4) 25px-Pdf_icon.png Book Draft Info_circle.png (version 2)
HW1 (due Friday, February 10) Downarrow.png

Exercise 1 (page 16); Exercises 2,3,4,5,6 (page 36); Exercise 7 (page 51).

  • Monitoring ERE is Non-Elementary (Section 6.1) 25px-Pdf_icon.png Book Draft Info_circle.png (version 3)
  • Generating Optimal ERE Monitors (Section 6.1.2) 25px-Pdf_icon.png Book Draft Info_circle.png (version 4)
  • Monitoring Finite-Trace Future-Time LTL (Sections 8 (LTL) and 6 (BTT)) 25px-Pdf_icon.png Book Draft Info_circle.png (version 5)
  • Monitoring Omega-Regular Expressions (Section 9) 25px-Pdf_icon.png Book Draft Info_circle.png (version 6)
  • HW2 version 25px-Pdf_icon.png Book Draft Info_circle.png (version 7)
HW2 (due Wednesday, March 1st) Downarrow.png

Exercise 8 (page 87); Exercises 10,11 (page 121); Exercise 13 (page 151); Exercise 14 (page 169).

  • Efficient Monitoring of Always-Past Temporal Safety (Section 10) 25px-Pdf_icon.png Book Draft Info_circle.png (version 8)
  • Monitoring Always-Past Temporal Safety with Call-Return (Section 11) 25px-Pdf_icon.png Book Draft Info_circle.png (version 9)
  • Monitoring with String Rewrite Systems (Section 13) 25px-Pdf_icon.png Book Draft Info_circle.png (version 10)
  • Monitoring Allen LTL Safety (Section 14) 25px-Pdf_icon.png Book Draft Info_circle.png (version 11)
  • Monitoring Context-Free Patterns (Section 12) 25px-Pdf_icon.png Book Draft Info_circle.png (version 13)
  • HW3 version 25px-Pdf_icon.png Book Draft Info_circle.png (version 13)
HW3 (due Wednesday, April 5) Downarrow.png

Exercise 15 (page 222); Exercise 19 (page 253-254) - do only S_c; Exercise 22 (page 292); Exercise 25 (page 320); Exercise 27 (page 321); Exercise 28 (page 341).

  • Parametric Property Monitoring (Section 15) 25px-Pdf_icon.png Book Draft Info_circle.png (version 12)
  • Monitoring Fixed-Point Properties with Data
  • Predictive Runtime Analysis (Chapter 19) 25px-Pdf_icon.png Book Draft Info_circle.png (version 14)
  • Predictive Runtime Analysis with Control Flow Abstraction (Chapter 20) 25px-Pdf_icon.png Book Draft Info_circle.png (version 15)
HW4 (last one) Downarrow.png

Exercise 29 (page 485); Exercises 30-31 (page 553).

Personal tools
Namespaces

Variants
Actions
Navigation