FM - Formal Methods Group

The Formal Methods Group is active in several research areas related to the application of formal methods and symbolic techniques, like formal verification of circuits by means of Model Checking, high-level synthesis and decision techniques in bounded spaces.
The group has worked in the context of logic function representation and manipulation based on Binary Decision Diagrams and SAT solvers. Since 2007 the group has taken part to the Hardware Model Checking Competition with the PdTRAV tool with excellent results.
The group recently extended its range of competence to embedded systems design and to the development of efficient algorithms for embedded systems, with emphasis of GPU and GPGPU platforms and applications to computer vision.


  • Formal verification
  • Logic function representation
  • Binary Decision Diagrams
  • Satisfiability solvers
  • Model Checking
  • Computer vision for embedded systems
  • Embedded systems design
  • Logic synthesis and optimization
  • Embedded systems design for automotive applications

Projects and publications