### Automated Verification (CS6315)

### Vanderbilt University

### Electrical Engineering and Computer Science (EECS)

#### Instructor:

Taylor Johnson#### Email Address:

firstname.lastname@vanderbilt.edu (replace firstname with Taylor and lastname with Johnson and note there is no mavs subdomain)#### Office Number:

ISIS 401D#### Office Telephone Number:

(email is preferred)#### Faculty Profile:

https://engineering.vanderbilt.edu/bio/taylor-johnson#### Instructor Website:

http://www.taylortjohnson.com/#### Section Information:

CS 6315-01, Spring 2017#### Course Website:

http://www.taylortjohnson.com/class/cs6315/s17/#### Time and Place of Class Meetings:

Tuesdays/Thursdays 11:00am-12:15pm, Vanderbilt - Featheringill Hall 258 (FGH 258)#### Office Hours:

ISIS 401D, Tuesdays/Thursdays 12:15pm-2pm and by appointment (email me to schedule by appointment)#### Graduate Teaching Assistant (GTA):

None#### Graduate Teaching Assistant Email Address:

n/a#### Graduate Teaching Assistant Office Hours:

n/a#### Course Schedule (Syllabus; note that all information appearing on this website supersedes that appearing in the syllabus PDF, that is, this website is more up-to-date):

The instructor for this course reserves the right to adjust this schedule in any way that serves the educational needs of the students enrolled in this course. All assignments and due dates are approximate at this point and will be updated on this website as the semester progresses. All readings refer to the Alur required textbook unless otherwise noted.Date | Content | Resources / Readings | Assignments |
---|---|---|---|

1/10 | Introduction and Course Overview: What is automated software engineering and what are formal methods? (First Day of Classes) | Alur Chapter 1 | |

1/13 | Math review: propositional logic and set theory | Reading: Aho and Ullman, Chapter 12 (particularly 12.2, 12.3, and 12.4, remainder may be skimmed, except skip 12.6, as they will come up again later in the course) and Chapter 14 (14.1, 14.2, 14.3, 14.4); Additional References: Lee and Seshia, Appendix B | |

1/17 | Math review: first-order logic and higher-order logic | Reading: Aho and Ullman, Chapter 12 (particularly 12.2, 12.3, and 12.4, remainder may be skimmed, except skip 12.6, as they will come up again later in the course) and Chapter 14 (14.1, 14.2, 14.3, 14.4); Additional References: Lee and Seshia, Appendix B | |

1/19 | Math review: automata theory and formal languages | Reading: Aho and Ullman, Chapter 12 (particularly 12.2, 12.3, and 12.4, remainder may be skimmed, except skip 12.6, as they will come up again later in the course) and Chapter 14 (14.1, 14.2, 14.3, 14.4); Additional References: Lee and Seshia, Appendix B | Homework 1 Assigned (files on BlackBoard) |

1/24 | Formal models: transition systems | Reading: Alur, Chapters 2 and 4 (skim chapter 4); Additional References: Lee and Seshia, Chapters 3 and 5 (and partly 6) | Homework 1 Due; Homework 2 Assigned (files on BlackBoard) |

1/26 | Formal models: synchronous networks and transition systems | Reading: Alur, Chapters 2 and 4 (skim chapter 4); Additional References: Lee and Seshia, Chapters 3 and 5 (and partly 6) | |

1/31 | Formal specifications: safety | Reading: Alur, Section 3.1, Section 5.1; Additional References: Lee and Seshia, Chapter 13 | |

2/2 | Formal methods for safety: inductive invariant proofs | Reading: Alur, Section 3.2 | Homework 2 Due; Homework 3 Assigned (files on BlackBoard) |

2/7 | Formal methods for safety: reachability analysis | Reading: Alur, Section 3.3 | |

2/9 | Formal models: asynchronous networks and transition systems | Reading: Alur, Section 5.2 | |

2/14 | Formal specifications: liveness, linear temporal logic (LTL), and computation tree logic (CTL) | Reading: Alur, Section 5.2 | |

2/16 | Formal methods for liveness: LTL model checking and repeatability analysis | Reading: Alur, Section 5.3 | Homework 4 Assigned (files on BlackBoard) |

2/21 | Automated/interactive theorem proving: overview | Klein and Nipkow, Chapter 13 | Homework 3 Due |

2/23 | Automated/interactive theorem proving: inductive invariant proofs | Klein and Nipkow, Chapter 13 | Homework 4 Due; Programming Assignment 1 Assigned |

2/28 | Automated/interactive theorem proving: liveness proofs with ranking functions | Alur, Section 5.4; Klein and Nipkow, Chapter 13 | |

3/20 | Timed automata | Alur, Chapter 7.1-7.2 | |

3/22 | Model checking timed automata | Alur, Chapter 7.3 | |

3/27 | Hybrid automata | Alur, Chapter 9 | |

3/29 | Model checking hybrid automata | Alur, Chapter 9 | |

4/4 | Satisfiability and satisfiability modulo theories (SMT) | Z3 | Programming Assignment 1 Due; Programming Assignment 2 Assigned |

4/6 | Bounded model checking | Z3 | |

4/11 | Bounded model checking for timed and hybrid automata | Z3 | |

4/13 | Test case generation with SAT/SMT | Z3 | |

4/18 | Binary Decision Diagrams (BDDs) | nuXmv | |

4/20 | Data Structures of SAT/SMT | Z3 | Programming Assignment 2 Due; Final Project Assigned |

4/24 | Semester Last Day of Classes | Final Project Due | |

5/3 | Difference Bound Matrices (DBMs) | Uppaal |

#### Required Textbook and Other Course Materials:

- Main Required Textbook: "Principles of Cyber-Physical Systems," Rajeev Alur, MIT Press, First Edition, 2015; a digital copy may be purchased here or a print copy can be found on Amazon

#### Optional Textbooks and Additional References (free online):

- Background math: "Foundations of Computer Science," Al Aho and Jeff Ullman, 1994.
- Alternative main textbook: "Introduction to Embedded Systems: A Cyber-Physical Systems Approach ," Second Edition, Edward Lee and Sanjit Seshia
- Theorem proving: "Concrete Semantics with Isabelle/HOL," Tobias Nipkow and Gerwin Klein, 2015
- nuXmv user manual
- NuSMV user manual

#### Software Tools:

We will use a variety of automated software engineering tools in this course, include test case generation, model checkers, SAT/SMT solvers, and automated/interactive theorem provers integrated with programming languages, such as through the Frama-C static analysis tool's links to Coq, PVS, and Isabelle. In particular, we plan to use the following tools and possibly others, especially dependent upon student interest in various application domains and target languages (e.g., C, Java, .NET, Python, etc.):- Model checkers: nuXmv (newest version) / NuSMV, Spin, Uppaal
- SAT/SMT solvers: Z3
- Static analysis tools: Frama-C
- Dynamic analysis tools: Daikon
- Automated/interactive theorem provers: Isabelle, and possibly PVS or Coq
- Test case generation tools: Pex, Simulink Design Verifier

#### Optional Textbooks and Additional References (for purchase):

- "Model Checking," Edmund Clarke, Orna Grumberg, and Doron Peled, MIT Press, 1999.
- "Principles of Model Checking," Christel Baier and Joost-Pieter Katoen, MIT Press, 2008

#### Description of Course Content:

Study of foundations, techniques and tools for automating software processes and methodologies including analysis, design, implementation, testing, and maintenance of large software systems.#### Prerequisites:

Prerequisite: Consent of instructor. Students are expected to be proficient with elementary computer science theory (discrete math, algorithms, graphs, etc.), discrete mathematics, and software development. Students are expected to have working experiences with software development, including software version control systems such as Git, Mercurial, and/or Subversion.#### Student Learning Outcomes:

The objective of this course is to introduce graduate computer science and engineering students to methods for automated analysis of software systems, in particular, using automated formal methods, such as model checking, model checking-inspired test case generation, satisfiability, theorem proving, etc. At course conclusion, students should be able to:- Understand propositional, first-order, and higher-order logic and their relationships to set theory.
- Understand formal specifications such as linear temporal logic (LTL), invariants, computation tree logic (CTL), etc.
- Be able to write formal specifications from informal (plain English) requirements for software systems
- Understand formal models such as extended state machines, hybrid automata, timed automata, and transition systems
- Understand syntax and semantics for models of software systems
- Use automated software engineering tools, such as test case generation tools, model checkers, SAT/SMT solvers, interactive theorem provers, etc.
- Understand the theoretical basis of algorithms and data structures used in automated software engineering tools such as model checkers, SAT/SMT solvers, etc.
- Understand static analysis and dynamic analysis
- Be profcient in deriving formal specifications and formal models for software systems

#### Descriptions of major assignments and examinations:

Coursework may include homework assignments, several programming assignments/small projects using various automated software engineering tools like model checkers, projects, exams, and quizzes. Online and/or in-class quizzes and discussions will make up a portion of the grade. All assignments are subject to change and are not finalized, but will be determined based on student interest and progress. Approximate due dates of assignments are shown in the course schedule and are all subject to change.#### Other Requirements:

Exams will be closed book, but students will be allowed to bring a two-sided sheet of letter-size paper. Students are expected to check the course website for updates to the course schedule throughout the semester.#### Grading:

Grade percentages will be calculated based on the following weights (however, the instructor reserves the right to change these percentages based on student participation and progress):- Homework and Programming Assignments: 40%
- Course Project: 20%
- Quizzes / Participation: 20%
- Final Exam: 20%

- 100 >= A >= 90
- 90 > B >= 80
- 80 > C >= 70
- 70 > D >= 60
- 60 > F >= 0