Time-Bounded Verification of CTMCs against Real-Time Specifications. - Taolue Chen 001; Marco Diciolla; Marta Z. Kwiatkowska; Alexandru Mereacre (FORMATS, 2011)

Time-Bounded Verification of CTMCs against MTL specifications. - Marco Diciolla (ICCSW, 2011)

Quantitative Verification of Implantable Cardiac Pacemakers. - Taolue Chen 001; Marco Diciolla; Marta Z. Kwiatkowska; Alexandru Mereacre (RTSS, 2012)

A simulink hybrid heart model for quantitative verification of cardiac pacemakers. - Taolue Chen 001; Marco Diciolla; Marta Z. Kwiatkowska; Alexandru Mereacre (HSCC, 2013)

Verification of linear duration properties over continuous-time markov chains. - Taolue Chen 001; Marco Diciolla; Marta Z. Kwiatkowska; Alexandru Mereacre (ACM Trans. Comput. Log., 2013)

Synthesising optimal timing delays for Timed I/O Automata. - Marco Diciolla; Chang Hwan Peter Kim; Marta Z. Kwiatkowska; Alexandru Mereacre (EMSOFT, 2014)

Quantitative verification of implantable cardiac pacemakers over hybrid heart models. - Taolue Chen 001; Marco Diciolla; Marta Z. Kwiatkowska; Alexandru Mereacre (Inf. Comput., 2014)

Quantitative verification of real-time properties with application to medical devices. - Marco Diciolla (2014)