Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
fv19:top [2019/08/21 15:11] vkuncak |
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]] | [[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]], [[https://people.epfl.ch/jad.hamza?lang=en|Jad Hamza]], with the help of Romain Edelmann, Georg Schmid, Romain Ruetschi | + | [[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]] | ||
- | ===== Introduction ===== | + | The primary verification tools used: [[http://stainless.epfl.ch/|Stainless]]. Stainless is a formal way of doing Scala. |
- | In this course we introduce formal verification as a principled approach for developing systems that do what they should do. | + | ===== Grading ===== |
- | Formal verification finds proofs that computer systems work | + | * 50% based on the **quiz on 12 December**: 15:15-18:00. You can bring printed lecture and exercise slides |
- | under all scenarios of interest. Formal verification tools help developers | + | * 50% based on all lab assignments and home works taken together |
- | 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 | + | 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. |
- | 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. | + | |
- | Warmup videos by others: | ||
- | * [[https://www.youtube.com/watch?v=-CTNS2D-kbY|What is Formal Verification? - Video from Galois]] | ||
- | * [[http://slideshot.epfl.ch/play/suri_moore|Machines Reasoning about Machines - EPFL talk by J Moore]] | ||
- | * [[https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A|Verification Corner videos - by Rustan Leino and others]] | ||
===== Outline ===== | ===== Outline ===== | ||
Line 42: | Line 30: | ||
**First class: Thursday 19 September at 15:15 in the classroom INF213.** | **First class: Thursday 19 September at 15:15 in the classroom INF213.** | ||
+ | The material consists of approximately four parts: | ||
+ | * I: Introduction and Finite State Systems | ||
+ | * II: Proof Assistants | ||
+ | * III: Automating Software Verification | ||
+ | * IV: Semantics for Verification | ||
+ | |||
+ | ---- | ||
**Part I: Introduction and Finite State Systems** | **Part I: Introduction and Finite State Systems** | ||
+ | ---- | ||
==== Week 01, September 16 ==== | ==== Week 01, September 16 ==== | ||
- | | Thursday | 15:15 | Lecture 01: Introduction. State machines | | + | Watch and understand the [[MooreMachinesReasoningMachines|Talk of J Moore 'Machines Reasoning about Machines']] |
- | | Thursday | 17:15 | Labs 01: Scala, Stainless, and State Machines | | + | |
- | | Friday | 13:15 | Exercises 01: Proofs about state 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 ==== | ==== Week 02, September 23 ==== | ||
- | | Thursday | 15:15 | Lecture 02: Explicit-State Exploration. BDDs | | + | | Thursday | 15:15 | Lecture 02: {{lec02-bmc.pdf|Bounded Model Checking}} | |
- | | Thursday | 17:15 | Labs 02: Explicit-State Reachability Checker | | + | | Thursday | 16:15 | IC Colloquium by Catalin Hritcu, INRIA | |
- | | Friday | 13:15 | Exercises 02: BDDs | | + | | 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 ==== | ==== Week 03, September 30 ==== | ||
- | | Thursday | 15:15 | Lecture 03: Bounded Model Checking and SAT | | + | | Thursday | 15:15 | Lecture 03: {{lec03.pdf|Propositional Proofs and SAT Idea}} | |
- | | Thursday | 17:15 | Labs 03: BDD-Based Reachability Checker | | + | | Thursday | 17:15 | Continue [[labs02|Labs 02]] (no new lab) | |
- | | Friday | 13:15 | Exercise 03: Propositional logic and SAT | | + | | 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 ==== | ==== Week 04, October 7 ==== | ||
- | | Thursday | 15:15 | Lecture 03: Hardware Verification | | + | | Thursday | 15:15 | Lecture 05: Hardware Verification lecture by [[https://people.epfl.ch/barbara.jobstmann|Barbara Jobstmann]] (see Moodle for slides) | |
- | | Thursday | 17:15 | Labs 04: SAT-Based Checker | | + | | Thursday | 17:15 | [[labs03|Labs 03: Building a SAT solver]] ({{labs02-03-solutions.tar.gz|Solutions}}) | |
- | | Friday | 13:15 | Lecture 04: Interpolation and Other Property-Based Algorithms | | + | | Friday | 13:15 | {{lecture06.pdf|Lecture 06: Linear Temporal Logic and Binary Decision Diagrams}} | |
- | **Part II: Deductive Program Verification** | + | ==== Week 05, October 14 ==== |
- | Loop Invariants. Hoare Logic. Statically Checked Function Contracts. Relational Semantics and Fixed-Point Semantics. Symbolic Execution. Satisfiability Modulo Theories. | + | | 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}}) | | ||
- | **Part III: Abstract Interpretation** | + | 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)]] | ||
- | Abstract Interpretation framework. Predicate Abstraction. | + | ---- |
+ | **Part II: Proof Assistants** | ||
+ | ---- | ||
- | **Part IV: Proof Assistants and Verified Software** | + | ==== Week 06, October 21 ==== |
- | Stainless. Isabelle. Coq. Imperative programs with Heap. Concurrency. | + | | 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]] | | ||
- | ===== Topic List ===== | + | 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 | * 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. | * Review of Sets, Relations, Computability, Propositional and First-Order Logic Syntax, Semantics, Sequent Calculus. | ||
Line 99: | Line 209: | ||
===== Relevant Textbooks ===== | ===== Relevant Textbooks ===== | ||
- | |||
- | * 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: [[http://concrete-semantics.org|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. | * 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. | ||
* Nielson, Flemming, Nielson, Hanne R., Hankin, Chris: Principles of Program Analysis. ISBN 978-3-662-03811-6. Springer 1999. | * 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. | * Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory (To Truth Through Proof), Springer 2002. | ||
Line 113: | Line 223: | ||
* Kenneth H. Rosen. Discrete Mathematics and Its Applications. E.g. 8th Edition. | * 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 | * 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]] | ||