COMP 611 - Topics in Programming Languages and Formal Methods

Instructor: Konstantinos Mamouras
Class meetings: Wednesdays 3:55pm-5:25pm at Duncan Hall 1046
Office hours: By appointment at Duncan Hall 3081

Course Description

The course will cover a selection of topics from the areas of programming languages and formal methods. All students will read classical and recent papers on the selected topics and give presentations on them. A student may elect to perform a semester-long project on a topic related to the content of the course and write a short report on their findings.

The Fall 2018 offering of the course will include a selection of readings from the theory of Cyber-Physical Systems (CPS), with an emphasis on the modeling and programming aspects of the theory.

Required Texts and Materials

There are no required textbooks for the class. Course materials, including links to readings, will be provided here.

Grade Policies

For students who are taking COMP 611 as a one-credit course, the grade will be based on class participation (50%) and presentations (50%).

For students who are taking COMP 611 as a three-credit course, the grade will be based on class participation (20%), presentations (20%), and a semester-long research project with a short final report (60%).

Course Schedule

We will read papers that fall within the following broad topics:

(1) Formal CPS models (synchronous & asynchronous)

Suggested readings:
  1. Reactive Modules (presenter: Lingkun)
  2. Kahn Process Networks (presenter: Kurt)
  3. Synchronous Data Flow (presenter: Zhiwei)
  4. Input/Output Automata (presenter: Suguman)
  5. The LUSTRE Synchronous Reactive Language (presenter: Lucas)

(2) Runtime verification of timed and quantitative properties

  1. Timed Automata (presenter: Suguman)
  2. Metric Temporal Logic (presenter: Zhiwei)
  3. Signal Temporal Logic (presenter: Lucas)
  4. Online Monitoring of LTL (presenter: Kurt)
  5. Online Monitoring of STL (presenter: Abhinav)

(3) Applications in medical CPS domain

  1. Verification of Medical Devices (presenter: Lingkun)
Date Topic Readings
August 22 Course Overview
August 29 Synchronous Models Reactive Modules
September 5 Asynchronous Models Kahn Process Networks
September 12 Synchronous Models Synchronous Data Flow
September 19 Asynchronous Models I/O Automata
September 26 Synchronous Models Lustre
October 3 Timed Models
October 10 Timed Logics Metric Temporal Logic
October 17 Timed Models Timed Automata
October 24 Timed Logics Signal Temporal Logic
October 31 Timed Models Application to Medical Devices
November 7 Monitoring Online Monitoring of LTL
November 14 Monitoring Online Monitoring of STL
November 21 Other Topics Reinforcement Learning for LTLf/LDLf Goals
November 28 Discussion

Absence Policies

If a student misses a course meeting, they are expected to review the corresponding material on their own.

Rice Honor Code

In this course, all students will be held to the standards of the Rice Honor Code, a code that you pledged to honor when you matriculated at this institution. If you are unfamiliar with the details of this code and how it is administered, you should consult the Honor System Handbook. This handbook outlines the University's expectations for the integrity of your academic work, the procedures for resolving alleged violations of those expectations, and the rights and responsibilities of students and faculty members throughout the process.

Disability Support Services

If you have a documented disability or other condition that may affect academic performance you should: 1) make sure this documentation is on file with Disability Support Services (Allen Center, Room 111 / / x5841) to determine the accommodations you need; and 2) talk with the instructor to discuss your accommodation needs.