Model Checking & Abstract Interpretation

 
Related Projects:
 

Model Checking of Automated Needle Steering
New techniques for the simulation and model checking of needle-tissue interaction

Uppyyl Simulator
A Python implementation of a DBM-based simulator for Uppaal models

i3m4
Model Guided Machine Learning for Simulating Soft Tissue Materials in Medicine

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