Past research projects

Verification of machine code (past) 

• Automatic recovery of a behavioural model of an executable file and  automatic test data generation
• Prototype OSMOSE (slides), prototype CFGBuilder [safe CFG recovery]  (slides)    
  
• DBA formal model  (slides)

Model checking systems with infinite state-space (past)

• Counter systems,  pointer systems, heterogeneous systems
• Symbolic representations for infinite sets and acceleration to unfold loops
• Software FAST and FASTeR  [model checking of (unbounded) counter systems]