Model Checking & Abstract Interpretation

 
Related Projects:
 

QMTL-VT
A quantitative metric temporal logic for verification time

 

Past projects:

Online Model Checking
Apply model checking to systems where accurate long-term models are difficult to obtain

ZenoTool
A Zeno Run detection tool for UPPAAL

BDDStab
A non-convex abstract domain for the binary analysis framework Jakstab

SPALTER
Frama-C plug-in that iteratively improves the precision of Frama-C's value analysis results