LARA: Lab for Automated Reasoning and Analysis

Laboratory for Automated Reasoning and Analysis (LARA), led by Viktor Kuncak, develops precise automated techniques for reasoning about computer systems. Among the uses of these techniques is improving software reliability and programmer productivity.

Information on joining and collaborating with LARA:

• for postdoc positions, email Viktor Kuncak
• PhD Positions and information about EPFL
  • Slides from a Seminar for Starting PhD Students (September 2009, somewhat context-specific)
• Master's program
• EPFL internships
• Exchanges for EPFL students

Publications in Infoscience

Master’s theses:

• Ersoy Bayramoglu: Programming with Undo
• Sebastian Gfeller: Robust Dynamically Deployed Static Analysis for Java
• Mirco Dotta: State Exploration of Scala Actor Programs
• Philippe Suter: Non-Clausal Satisfiability Modulo Theories
• Gizil Oguz: Decision Tree Learning for Drools

Faculty member: Viktor Kuncak

PhD Students:

• Hossein Hojjat
• Giuliano Losa
• Ruzica Piskac
• Philippe Suter

First-year PhD students on IC Fellowship involved in LARA projects:

• Eva Darulová
• Tihomir Gvero
• Flaviu Roman

Current master’s students: Mikael Mayer, Remi Bonnet

Secretary: mme Danielle Chamberlain

System Manager: Fabien Salvi

Past visitors and members: Pierre-Evariste Dagand, Mirco Dotta, Abhinav Kumar, Abhishek Kumar Dubey, Sebastian Gfeller, Milos Gligoric, Sasa Misailovic, Marco Muniz, Hai Huu Nguyen, Steven Obua, Gizil Oguz, Thomas Wies, Kuat Yessenov

We also host from time to time short visits by researchers in our area, please see TRESOR Seminars Page for talk abstracts and selected video recordings.

A relatively mature project is Jahob system on verification of Java programs.

For the other recent projects, please see the following reports and papers:

• On Combining Theories with Shared Set Operations
• Linear Arithmetic with Stars
• On Static Analysis for Expressive Pattern Matching
• On Delayed Choice Execution for Falsification
• CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems
• Opis: Reliable Distributed Systems in OCaml

• Rich Model Toolkit (http://RichModels.epfl.ch)

Spring 2010: Software Analysis and Verification

Fall 2009: Compiler Construction

Fall 2009: Logic and Automata Theory

Spring 2009: Software Analysis and Verification

Fall 2008: Compiler Construction

Spring 2008: Software Analysis and Verification

Spring 2007: Software Analysis and Verification

TRESOR

EPFL Laboratory for Automated Reasoning and Analysis is supported by the funding from the Swiss National Science Foundation, the Microsoft Innovation Cluster for Embedded Software, and the EPFL School of Computer and Communication Sciences.