Lab for Automated Reasoning and Analysis LARA

Synthesis, Analysis, and Verification (SAV 2011)

New edition of this course is SAV 2012.

Course Material

Week 01, February 21

  • Lecture 01 - Introduction to Verification. Monday, February 21 at 14:15, INR 219
  • Exercise 01 - Hands-on specification and verification in Spec#. Tuesday, February 22 at 16:15, INM 10
  • Lab 01 - Introductory Lecture about Synthesis. Background on sets and relations, Friday, February 25, INR 219

Week 02, February 28

  • Lecture 02 - Lecture on relational semantics, Monday, February 28
  • Exercise 02 - First-order logic and relations, Tuesday, March 1
  • Lab 02 - Labs on doing proofs using the Isabelle interactive proof assistant
  • Homework 02 - Expressions built from relations. Isabelle

Week 03, March 07

  • Lecture 03 - Hoare logic. Building formulas from programs
  • Exercise 03 - More Hoare Logic. Construction of formulas
  • Lab 03 - Exercises and a 1/2 lecture on Strongest Postconditions
  • Homework 03 - Hoare logic

Week 04, March 14

Week 05, March 21

  • Lecture 05 - Homework discussion and exercises
  • Exercise 05 - Modeling Arrays and Fields
  • Lab 05 - Models of Dynamic Memory Allocation. Definition of WS1S

Week 06, March 28

  • Lecture 06 - preparation for the quiz
  • Exercise 06 - Quiz from 16:00 until 19:00 (not open book)
  • Labs 06 - Lecture on Predicate Abstraction for Invariant Inference

Week 07, April 4

  • Lecture 07 - Lecture and Demo of Verification of Functional Programs in Scala
  • Exercise 07 - Mini Project Discussions. Quantifier Elimination
  • Labs 07 - More Quantifier Elimination

Week 08, April 11

Week 09, April 18

Week 10, April 25

Week 11, May 2

  • Lecture 11: Remaining project descriptions. Exercises with lattices
  • Exercise 11 - Fixpoint theorems. Galois connection. Transition system.
  • Labs 11 - Abstract interpretation Framework

Week 12, May 9

  • Lecture 12: Combining Galois Connections. Predicate Abstraction Demo
  • Exercise 12: Collecting Semantics and its Abstract Interpretation. Fixed point and Prefix Point Formulation through example
  • Labs 12: Abstract interepretation through example

Week 13, May 16

  • Monday: Phantm and Insane tools
  • Tuesday: Quiz gymnastics through monotonic functions on sets. Remarks on predicate abstraction
  • Friday: Quiz

Week 14, May 23

Week 15, May 30

Friday, June 10: Project Reports Due in Moodle (5 pages, 2 column)

General Information

Announcements

February 17, 2011

  • the first lecture will be on Monday, February 21st.
  • in subsequent weeks, lecture, exercise, and lab slots are interchangeable, and will be announced the week before
  • for all further announcements see http://moodle.epfl.ch forum
 
sav11/top.txt · Last modified: 2012/01/07 19:23 by vkuncak