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:

Optional Textbooks and Additional References (free online):

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.):

Optional Textbooks and Additional References (for purchase):

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%
Letter grades will be determined based on the following ranges:
  • 100 >= A >= 90
  • 90 > B >= 80
  • 80 > C >= 70
  • 70 > D >= 60
  • 60 > F >= 0
The instructor reserves the right to move the thresholds down based on the distribution of final percentages, but they will not move up (e.g., if a grade percentage is between 90 and 100, this will receive an A). Students are expected to keep track of their performance throughout the semester and seek guidance from available sources (including the instructor) if their performance drops below satisfactory levels.

Make-Up Assignments, Exams, and Late Assignment Submission:

If you miss an exam or quiz due to unavoidable circumstances (e.g., health), you must notify the instructor in writing via email as soon as possible and request a makeup approval. If it is a planned (non-emergency) abcense, you must inform the instructor ahead of time! Do NOT ask for make-ups if you do not complete something due to travel (except when you are required to travel to represent the university or department on official business, but request at least 3 days ahead of the due date or exam time). If you submit an assignment late, it will have points taken off at a rate of 33% per day.

Last modified:

January 21, 2017 01:50:28.