Sample projects from 2008:

• Ersoy Bayramoglu: Verification of Equals Methods in Java Programs
• Pierre-Evariste 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

Recall Homework 01

Summary Example with Integers

Applications of Quantifier Elimination

Quantifier Elimination Definition

QE from Conjunction of Literals Suffices

Simple QE for Dense Linear Orders

Simple QE for Integer Difference Inequalities

Definition of Presburger Arithmetic

QE for Presburger Arithmetic

(Continued in Labs 07)