 English only
Lab for Automated Reasoning and Analysis LARA
Software Analysis and Verification 2008
Taught in Spring 2008 by Viktor Kuncak and Ruzica Piskac from the LARA group.
 later edition: Software Analysis and Verification 2009
Projects
Project suggestions (acess only for class members)
Projects completed by students:
 Ersoy Bayramoglu: Verification of Equals Methods in Java Programs
 PierreEvariste Dagand: Model Checking Opis
 Sebastian Gfeller: Combining Jahob and STP to Generate Test Cases
 Thomas Hofer: Solving Satisfiable Constraints over Finite Domains
 Thibaud Hottelier: Counterexample Analysis in Valigator
 David Joaquim: SAT Solver
 Giuliano Losa: Simple constant propagation for the simple programming language
 Stephane Rabie: Term Algebra Quantifier Elimination
 Damien Zufferey: Static Analysis on a Functional Subset of Scala
Lectures, Exercises, and Homeworks

 Exercises 01: Relations, Aunt Agatha, SPASS, formDecider, FOL Formulas, FOL is undecidable

 Exercises 02: Homework analysis, Proving properties of wp, sp

 Homework06 (an alternative April 1st Version will also be accepted)

 Exercises10

 Exercises11

 Exercies12

 Exercises13
 Project presentations: Thursday, May 29th, 12:00until we are done
 Project writeup and source code are due on Friday, June 6, following the EPFL Academic Calendar
Here are last year's lectures.