| 2014 | CAV | Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. | Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Z. Kwiatkowska |
| 2014 | EMSOFT | Synthesising optimal timing delays for Timed I/O Automata. | Marco Diciolla, Chang Hwan Peter Kim, Marta Z. Kwiatkowska, Alexandru Mereacre |
| 2014 | ISoLA | On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers. | Marta Z. Kwiatkowska, Alexandru Mereacre, Nicola Paoletti |
| 2012 | RTSS | Quantitative Verification of Implantable Cardiac Pacemakers. | Taolue Chen, Marco Diciolla, Marta Z. Kwiatkowska, Alexandru Mereacre |
| 2011 | TACAS | Efficient CTMC Model Checking of Linear Real-Time Objectives. | Benot Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre |
| 2009 | ATVA | LTL Model Checking of Time-Inhomogeneous Markov Chains. | Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre |
| 2009 | LICS | Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. | Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre |
| 2008 | RTSS | Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability. | Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre |