The LMV (Logic, Models and Verification) team conducts research on both development and application of formal methods for improving software reliability. We study properties ranging from simple invariants over reachable states to more subtle functional specifications and temporal properties. We heavily rely on approximations to make the calculations tractable for both finite and infinite systems.

Theme 1

  • Semantics of Programming Languages
  • Static Analysis
  • Programs Proof
  • Certification

Theme 2

  • Rewriting Systems
  • Approximation and Tree Automaton
  • Model Checking
  • Partial-Order Semantics