This page is for a past semester (s17) and is for archival purposes only
Automated Verification (CS6315)
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.