Laboratory for Automated Reasoning and Analysis (and TRESOR)
Context
- background
- ProgLab vision
- have a worked out plan
- looking for several sources of funding
LARA (and TRESOR) approach: new theory + new working tools
Software Verification
Ongoing and Future Work
Jahob++
- 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