Differences

This shows you the differences between two versions of the page.

--- fv19:top [2019/08/13 17:43]
vkuncak [Formal Verification EPFL Course (CS-550), Fall 2019]
+++ fv19:top [2019/12/08 00:10]
vkuncak
@@ Line 1: / Line 1: @@
-====== Formal Verification EPFL Course (CS-550), Fall 2019 ======
+====== Formal Verification: EPFL Course (CS-550), Fall 2019 ======
+In this course we introduce formal verification as a principled approach
+for developing systems that do what they should do.
 [[https://moodle.epfl.ch/course/view.php?id=13051|Moodle]]
-Autumn 2019 Semester. 2h Lectures, 2h Exercises, 2h Labs. Continuous Control
+Autumn 2019 Semester. 2h Lectures, 2h Exercises, 2h Labs. Continuous Control.
-Instructors: [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]] and [[https://people.epfl.ch/jad.hamza?lang=en|Jad Hamza]]
+[[https://edu.epfl.ch/coursebook/en/formal-verification-CS-550?cb_cycle=bama_cyclemaster&cb_section=in|CS-550 in Course Catalog]]
+Instructors: [[http://lara.epfl.ch/~kuncak/|Viktor Kuncak]], [[https://people.epfl.ch/jad.hamza?lang=en|Jad Hamza]], with the help of [[https://romac.me/|Romain Ruetschi]]
-One of the verification tools used: [[http://stainless.epfl.ch/|Stainless]]
+All project assignments will be in Scala. If you do not know Scala, please consider these free EPFL Courseware courses:
+  * [[https://courseware.epfl.ch/courses/course-v1:EPFL+progfun1+2018_T1/about|Functional Programming Principles in Scala]]
+  * [[https://courseware.epfl.ch/courses/course-v1:EPFL+progfun2+2018_T1/about|Functional Program Design in Scala]]
-[[http://concrete-semantics.org|Concrete semantics]]
+The primary verification tools used: [[http://stainless.epfl.ch/|Stainless]]. Stainless is a formal way of doing Scala.
-===== Introduction =====
+===== Grading =====
-In this course we introduce formal verification as an approach for developing highly reliable systems.
+  * 50% based on the **quiz on 12 December**: 15:15-18:00. You can bring printed lecture and exercise slides
+  * 50% based on all lab assignments and home works taken together
-Formal verification finds proofs that computer systems work
+There will be 7 labs in total: 6 fixed ones that everyone should do individually, and a 7th one that are to be done in groups of 1-3 students. You will need to present the plan for the final lab in the last week of the semester.
-under all scenarios of interest. Formal verification tools help developers
-construct such proofs, automatically searching for proofs
-using theorem proving and constraint solving (using,
-e.g. SMT solvers), and static analysis to discover program
-invariants. When it succeeds, formal verification is guaranteed to identify
-all software errors, including, for example, security
-vulnerabilities or cases when the computation produces a
-wrong numerical or symbolic result. The best approach to obtain formally
-verified software is to perform formal verification while software is
-developed, as opposed to after the fact.
-Companies, research labs and research groups have developed
-proofs of correctness of operating system kernels, brake
-system for a metro line in Paris, compilers, databases, data
-structures, smartcard wallets, communication protocols, and
-distributed systems.
-In this course we will learn how to use formal verification tools and explain the theory and the practice behind them.
+===== Outline =====
+**First class: Thursday 19 September at 15:15 in the classroom INF213.**
-Warmup videos by others:
+The material consists of approximately four parts:
-  * [[https://www.youtube.com/watch?v=-CTNS2D-kbY|What is Formal Verification? - Video from Galois]]
+  * I: Introduction and Finite State Systems
-  * [[http://slideshot.epfl.ch/play/suri_moore|Machines Reasoning about Machines - EPFL talk by J Moore]]
+  * II: Proof Assistants
-  * [[https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A|Verification Corner videos - by Rustan Leino and others]]
+  * III: Automating Software Verification
+  * IV: Semantics for Verification
-===== Topics =====
+----
+**Part I: Introduction and Finite State Systems**
+----
+==== Week 01, September 16 ====
+Watch and understand the [[MooreMachinesReasoningMachines|Talk of J Moore 'Machines Reasoning about Machines']]
+| Thursday | 15:15 | Lecture 01: Introduction. Transition Systems: {{lec01.pdf|slides}}, {{lec01-scala-examples.zip|Scala examples}} |
+| Thursday | 17:15 | [[labs01|Labs 01: Scala, Stainless, and State Machines]]  ({{labs01-solutions.tar.gz|Solutions}}) |
+| Friday   | 13:15 | {{ex01-problems.pdf|Exercises 01: State machines and propositional logic}} ({{ex01-problems-and-solutions.pdf|Solutions}}) |
+==== Week 02, September 23 ====
+| Thursday | 15:15 | Lecture 02: {{lec02-bmc.pdf|Bounded Model Checking}}  |
+| Thursday | 16:15 | IC Colloquium by Catalin Hritcu, INRIA |
+| Thursday | 17:30 | [[labs02|Labs 02: Bounded model checker]] ({{labs02-03-solutions.tar.gz|Solutions}})            |
+| Friday      | 13:15 | {{exercise-and-review02.pdf|Exercises 02}} ({{ex2-main-with-solutions.pdf|Solutions}}) |
+Reading:
+  * Chapter 10 of the Model Checking Handbook
+==== Week 03, September 30 ====
+| Thursday | 15:15 | Lecture 03: {{lec03.pdf|Propositional Proofs and SAT Idea}}  |
+| Thursday | 17:15 | Continue [[labs02|Labs 02]] (no new lab)    |
+| Friday   | 13:15 | Lecture 04: SAT Solvers: {{sharad-malik-history-sat-16x9.pdf|Slides of Prof. Sharad Malik (Princeton)}}, {{lec04-more.pdf|Further Slides}}  |
+Reading:
+  * Chapter 9 of the Model Checking Handbook
+  * [[sav13/lecturecise_15|A Lecture and material on SAT]]
+  * Chapter 24 and 2 of the Model Checking Handbook
+==== Week 04, October 7 ====
+| Thursday | 15:15 | Lecture 05: Hardware Verification lecture by [[https://people.epfl.ch/barbara.jobstmann|Barbara Jobstmann]] (see Moodle for slides) |
+| Thursday | 17:15 | [[labs03|Labs 03: Building a SAT solver]] ({{labs02-03-solutions.tar.gz|Solutions}}) |
+| Friday   | 13:15 | {{lecture06.pdf|Lecture 06: Linear Temporal Logic and Binary Decision Diagrams}} |
+==== Week 05, October 14 ====
+| Thursday | 15:15 | Lecture 07: {{lec07-interpolation.pdf|Interpolation-Based Model Checking}},{{mcmillan2003_chapter_interpolationandsat-basedmodel.pdf|McMillan 2003 paper}},{{interpolantstrength.pdf|Interpolant Strength}} |
+| Thursday | 17:15 | Continue Labs 03  |
+| Friday   | 13:15 | Exercises 03: {{ex3-problems-only.pdf|Syntax, Semantics, and Exercises for First-Order Logic}} ({{ex3-solutions.pdf|Solutions}}) |
+For further reading, check some of the recent papers:
+  * [[https://link.springer.com/chapter/10.1007%2F978-3-319-08867-9_17|Interpolating Property Directed Reachability (CAV 2014)]]
+  * [[https://doi.org/10.1007/978-3-030-25543-5_21|Interpolating Strong Induction (CAV 2019)]]
+----
+**Part II: Proof Assistants**
+----
+==== Week 06, October 21 ====
+| Thursday | 15:15 |  {{lecture08-lcf.pdf|Lecture 08: LCF Approach to Formal Proof}} |
+| Thursday | 17:15 | [[labs04|Labs 04: LCF Approach]] |
+| Friday   | 13:15 | Lecture 09: First-Order Logic Normal Forms and Resolution: {{lec09-draft.pdf|Slide Deck 1}}, [[https://lara.epfl.ch/w/_media/sav17/lec14.pdf|Slide Deck 2]], check also material such as [[sav08/lecture11|this]] |
+Reading for LCF approach:
+  * {{holhistory.pdf|Michael J. C. Gordon.  From LCF to HOL: a short history.  In Gordon Plotkin, Colin Stirling, and Mads Tofte,editors,Proof, Language, and Interaction: Essays in Honor of Robin Milner, pages 169–185. MIT Press, 2000.}}
+  * Practical Logic and Automated Reasoning (Harrison), Chapter 6
+Reading for resolution:
+  * Practical Logic and Automated Reasoning (Harrison), Chapter 3
+==== Week 07, October 28 ====
+| Thursday | 15:15 | {{lecture10-isabelle.pdf|Lecture 10: Isabelle/HOL}} from [[http://concrete-semantics.org/|Concrete Semantics]] with [[http://concrete-semantics.org/demos.tar|demos]] |
+| Thursday | 17:15 | Continue Labs 04 and start [[labs05|Labs 05]] on Isabelle |
+| Friday   | 13:15 | {{lecture11-isabelle.pdf|Quantifiers, Rules, and Structured Proofs}}, {{mylecture.zip|Sleepy Student Paradox Example}} |
+Reading:
+  * [[https://isabelle.in.tum.de/|Isabelle proof assistant (with tutorials)]], **especially** [[https://isabelle.in.tum.de/dist/Isabelle2019/doc/prog-prove.pdf|Programming and Proving in Isabelle/HOL]]
+  * [[http://concrete-semantics.org/|Concrete Semantics]] (source of the slides and demos)
+  * [[https://arxiv.org/pdf/1907.02836.pdf|From LCF to Isabelle/HOL]]
+  * [[https://isabelle.in.tum.de/community/Main_Page|Isabelle Wiki]]
+  * {{noschinskitraut-patternbasedsubtermselection.pdf|Patter-Based Subterm Selection}} (for precise rewriting); see also [[https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Rewrite_Examples.html|src/HOL/ex/Rewrite_Examples.thy]]
+More advanced:
+  * [[https://nms.kcl.ac.uk/christian.urban/Cookbook/|Isabelle programming tutorial]]
+----
+**Part III: Automating Software Verification**
+----
+==== Week 08, November 4 ====
+| Thursday | 15:15 |  {{lecture12-vcg.pdf|Lecture 12: Hoare Logic and Translating Code to Formulas}} |
+| Thursday | 17:15 | [[labs05|Labs 05]] on Isabelle |
+| Friday   | 13:15 | {{lecture13-hoare.pdf|Lecture 13: More on Hoare Logic}} |
+==== Week 09, November 11 ====
+| Thursday | 15:15 | {{lecture14-loops.pdf|Lecture 14: Contexts, Local Variables, Loops}} |
+| Thursday | 17:15 | Continue [[labs05]] and do watch-and-answer Lab0-Rustan of [[LeinoVerifiedSoftware|talk of Rustan Leino 'Directions to and for Verified Software']] |
+| Friday   | 13:15 | {{lecture15-recursion-qe.pdf|Lecture 15: Recursion. Quantifier Elimination}} |
+==== Week 10, November 18 ====
+| Thursday | 15:15 |  {{lecture16.pdf|Lecture 16: More QE. Satisfiability Modulo Theories and DPLL(T)}} |
+| Thursday | 17:15 | [[Labs06|Labs 06: Verifier for Recursive Procedures]] |
+| Friday   | 13:15    | {{lecture17-annot.pdf|Lecture 17a: More on SMT}}. Exercises: {{quiz2013.pdf|Quiz 2013}}, {{quiz2015.pdf|Quiz 2015}} |
+  * {{sav13:lecturecise23.pdf|older slides}}
+Milestones in SMT solver development:
+  * results of Nelson and Oppen, including {{:nelsonoppen80decisionprocedurescongruenceclosure.pdf|Nelson's dissertation}}
+  * inclusion of SAT solvers and the DPLL(T) algorithm: [[ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/NieOT-JACM-06.pdf|Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland
+Procedure to DPLL(T)]]
+  * The [[http://www.smtlib.org/|SMT-LIB initiative]] with standardized format, benchmarks, and competitions
+  * The provers such as [[http://research.microsoft.com/en-us/um/redmond/projects/z3/|Z3 prover]]
+Introduction from {{sav12:selected-verifun.pdf|Selected VeriFun slides}}
+({{sav12:part-verifun.pdf|Full VeriFun slides are here}})
+==== Week 11, November 25 ====
+A web demo version of the Leon system:
+  * http://leon.epfl.ch/
+  * [[https://www.youtube.com/watch?v=JFbx4iryNb0|Recording of Leon Demo]]
+| Thursday | 15:15 | {{lecture17b.pdf|Lecture 17b: Bounded Checking for Recursive Programs. Elements of Abstract Interpretation}} |
+| Thursday | 16:15 | [[https://memento.epfl.ch/event/tla-model-checking-made-symbolic-2/|Talk: TLA Model Checking Made Symbolic]] {{igor-talk.pdf|Slides of Igor's talk}} |
+| Thursday | 17:15 | [[Labs06|Labs 06: Verifier for Recursive Procedures]] |
+| Friday   | 13:15 | {{nicolasvoirol-lecture.pdf|Guest lecture by Nicolas Voirol on Stainless system architecture, encoding of recursion and higher-order functions}} |
+----
+====== Future ======
+----
+----
+**Part IV: Semantics for Verification**
+----
+==== Week 12, December 2 ====
+| Thursday | 15:15 | {{lecture19-ai.pdf|Lecture 19: Abstract Interpretation Introduction}} |
+| Thursday | 17:15 | [[https://docs.google.com/document/d/1kAHSABMFVFtg8-r4z-rzl0HRFj71kpmbhCdU47I610Y/edit?usp=sharing|Personalized Labs]] |
+| Friday   | 13:15 | Lecture 20: More Abstract Interpretation. Predicate Abstraction |
+==== Week 13, December 9 ====
+| Thursday | **15:15-18:00** | Quiz in the usual INF room |
+| Friday    | 13:15    | Personalized Labs: Final Choice of Topics by The end of Day |
+==== Week 14, December 16 ====
+| Thursday | 15:15 | Personalized Labs Presentations |
+| Thursday | 17:15 | Personalized Labs Presentations |
+| Friday    | 13:15   | Personalized Labs Presentations |
+===== (Further) Topic List =====
+  * Modelling local state and program heap. Intermediate verification languages (Why3, Horn clauses, Inox)
+    * Example paper: [[https://link.springer.com/chapter/10.1007/978-3-030-03592-1_12|SideTrail: Verifying Time-Balancing of Cryptosystems]] (based on Boogie)
   * Importance of Reliable Systems. Methodology of Formal Verification. Soundness and Completeness in Modeling and Tools. Successful Tools and Flagship Case Studies
   * Review of Sets, Relations, Computability, Propositional and First-Order Logic Syntax, Semantics, Sequent Calculus.
@@ Line 60: / Line 209: @@
 ===== Relevant Textbooks =====
+  * Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
+  * Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. [[https://beast-epfl.hosted.exlibrisgroup.com/primo-explore/fulldisplay?docid=EPFL_SFX4100000004243430&context=L&vid=EPFL&lang=fr_FR&search_scope=default_scope&adaptor=Local%20Search%20Engine&tab=default_tab&query=any,contains,Handbook%20of%20model%20checking&offset=0|Available online from within EPFL through the EPFL library]]
+  * Tobias Nipkow, Gerwin Klein:  [[http://concrete-semantics.org|Concrete semantics]] with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
+  * John Harrison: Handbook of Practical Logic Logic and Automated Reasoning ([[https://www.cl.cam.ac.uk/~jrh13/atp/index.html|resources]])
   * Michael Huth and Mark Rayan: Logic in Computer Science - Modelling and Reasoning about Systems. Cambridge University Press 2004.
-  * Handbook of Model Checking, https://www.springer.com/de/book/9783319105741 Springer 2018. Including Chapter Model Checking Security Protocols by David Basin.
-  * Tobias Nipkow, Gerwin Klein: Concrete Semantics with Isabelle/HOL. http://concrete-semantics.org/concrete-semantics.pdf
-  * Aaron Bradley and Zohar Manna: The Calculus of Computation - Decision Procedures with Applications to Verification, Springer 2007.
   * Nielson, Flemming, Nielson, Hanne R., Hankin, Chris: Principles of Program Analysis. ISBN 978-3-662-03811-6. Springer 1999.
   * Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory (To Truth Through Proof), Springer 2002.
@@ Line 74: / Line 223: @@
   * Kenneth H. Rosen. Discrete Mathematics and Its Applications. E.g. 8th Edition.
   * Formally Verified Software in the Real World. Communications of the ACM, October 2018. https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext
+===== Introduction =====
+Formal verification finds proofs that computer systems work
+under all scenarios of interest. Formal verification tools help developers
+construct such proofs, automatically searching for proofs
+using theorem proving and constraint solving (using,
+e.g. SMT solvers), and static analysis to discover program
+invariants. When it succeeds, formal verification is guaranteed to identify
+all software errors, including, for example, security
+vulnerabilities or cases when the computation produces a
+wrong numerical or symbolic result. The best approach to obtain formally
+verified software is to perform formal verification while software is
+developed, as opposed to after the fact.
+Companies, research labs and research groups have developed
+proofs of correctness of operating system kernels, brake
+system for a metro line in Paris, compilers, databases, data
+structures, smartcard wallets, communication protocols, and
+distributed systems.
+In this course we will learn how to use formal verification tools and
+explain the theory and the practice behind them.
+A short illustrative video: [[https://www.youtube.com/watch?v=-CTNS2D-kbY|What is Formal Verification? - by Galois, a formal methods company]]
+Somewhat related past course: [[sav17:top|SAV 2017]]