Laboratory for Automated Reasoning and Analysis (and TRESOR)


General Information


LARA (and TRESOR) approach: new theory + new working tools

Software Verification

Ongoing and Future Work


  • usability
  • feedback
  • integration into ProgLab
  • while maintaining applicability to Java

Theorem Proving

Grew out of Jahob verification effort.

Developing next generation.

Applicable beyond software implementations

  • verifying any model with complex discrete components

Constraint Solving

Motivation: focus on providing concrete feedback (not only yes/no answers):

  • countexamples
  • proofs

Application in

  • verification
  • testing
  • software modelling

Previous work on MIT's Alloy system.

Collaboration with LAMS

Solving Optimization Problems

Mixed Integer Linear Programming:

  • maximize linear objective function
  • subject to linear constraints
  • subject to certain variables taking on only discrete values

Recent results on compact solutions for exponentially large problems

  • grew out of techniques for reasoning about data structures

Collaboration with Prof. Friedrich Eisenbrand's group in EPFL Math

Structured Documents

Beyond software and formal specification:

  • textual specification
  • analysis of structured documents (intern from India)
  • leverage constraint solving, combine with NLP

LARA and Education