LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
fv19:top [2019/08/13 17:44]
vkuncak
fv19:top [2019/12/08 00:11] (current)
vkuncak [Week 12, December 2]
Line 1: Line 1:
-====== Formal Verification EPFL Course (CS-550), Fall 2019 ======+====== Formal VerificationEPFL 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]] ​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]]
  
-===== 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 an approach for developing highly reliable systems. ​+===== Grading =====
  
-Formal verification finds proofs that computer systems work +  * 50% based on the **quiz on 12 December**: 15:15-18:00You can bring printed lecture ​and exercise slides 
-under all scenarios of interestFormal 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.+
  
-Companiesresearch 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. 
  
 +===== Outline =====
  
-Warmup videos by others: +**First classThursday 19 September at 15:15 in the classroom INF213.**
-  ​[[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]]+
  
-===== Topics =====+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**
 +----
 +
 +==== 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 | {{lecture20-predicates.pdf|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 58: Line 209:
  
 ===== Relevant Textbooks ===== ===== 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.   * 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. 
   * 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 72: 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]]