Model Checking & Abstract Interpretation

 
Related Projects:
 

Harmonics Mover
... and its main application in Online Model Checking for Robotic Radiation Therapy

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

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

QMTL-VT
A quantitative metric temporal logic for verification time

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

 

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