View source for CS598 - Runtime Verification (Spring 2017)

__NOEDITSECTION__
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''.

:* '''''Introduction''''' {{pptx|CS598-Spring-2017-01.pptx|slides}}
::* Some runtime verification systems to try out:
:::* [http://fsl.cs.illinois.edu/index.php/JavaMOP4 JavaMOP] ([http://www.kframework.org/tool/run/javamop online]) for monitor synthesis and runtime monitoring of safety properties
:::* [https://runtimeverification.com/predict/ RV-Predict] for predictive runtime analysis
:::* [https://runtimeverification.com/match/ RV-Match] for semantics-based runtime verification
:* '''''Safety and Monitoring Foundations''''' {{pdf|CS598-Spring-2017-02.pdf|Book Draft}}