Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains. - Joost-Pieter Katoen; Alexandru Mereacre (FORMATS, 2008)

Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. - Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (HSCC, 2008)

Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability. - Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (RTSS, 2008)

LTL Model Checking of Time-Inhomogeneous Markov Chains. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (ATVA, 2009)

Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (LICS, 2009)

Time-Inhomogeneous Markov Chains and Piecewise Deterministic Markov Processes. - Alexandru Mereacre (AlgoSyn, 2010)

Computing Optimal Schedules for battery Usage in Embedded Systems. - Marijn R. Jongerden; Alexandru Mereacre; Henrik C. Bohnenkamp; Boudewijn R. Haverkort; Joost-Pieter Katoen (IEEE Trans. Ind. Informatics, 2010)

Reachability probabilities in Markovian Timed Automata. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (CDC/ECC, 2011)

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

Quantitative automata model checking of autonomous stochastic hybrid systems. - Alessandro Abate; Joost-Pieter Katoen; Alexandru Mereacre (HSCC, 2011)

Observing Continuous-Time MDPs by 1-Clock Timed Automata. - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (RP, 2011)

Efficient CTMC Model Checking of Linear Real-Time Objectives. - Benoît Barbot; Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (TACAS, 2011)

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications - Taolue Chen 001; Tingting Han 001; Joost-Pieter Katoen; Alexandru Mereacre (Log. Methods Comput. Sci., 2011)

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

Verification of continuous-space stochastic systems. - Alexandru Mereacre (2012)

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

Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. - Ilya Tkachev; Alexandru Mereacre; Joost-Pieter Katoen; Alessandro Abate (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)

Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. - Zhenqi Huang; Chuchu Fan; Alexandru Mereacre; Sayan Mitra; Marta Z. Kwiatkowska (CAV, 2014)

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

Formal Modelling and Validation of Rate-Adaptive Pacemakers. - Marta Z. Kwiatkowska; Harriet Lea-Banks; Alexandru Mereacre; Nicola Paoletti (ICHI, 2014)

On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers. - Marta Z. Kwiatkowska; Alexandru Mereacre; Nicola Paoletti (ISoLA (2), 2014)

Automated Verification of Quantitative Properties of Cardiac Pacemaker Software. - Marta Z. Kwiatkowska; Alexandru Mereacre (MCPS, 2014)

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

Estimation and Verification of Hybrid Heart Models for Personalised Medical and Wearable Devices. - Benoît Barbot; Marta Z. Kwiatkowska; Alexandru Mereacre; Nicola Paoletti (CMSB, 2015)

Hardware-in-the-loop simulation and energy optimization of cardiac pacemakers. - Chris Barker; Marta Z. Kwiatkowska; Alexandru Mereacre; Nicola Paoletti; Andrea Patane (EMBC, 2015)

Synthesising Robust and Optimal Parameters for Cardiac Pacemakers Using Symbolic and Evolutionary Computation Techniques. - Marta Z. Kwiatkowska; Alexandru Mereacre; Nicola Paoletti; Andrea Patane (HSB, 2015)

Simulation-Based Verification of Cardiac Pacemakers With Guaranteed Coverage. - Zhenqi Huang; Chuchu Fan; Alexandru Mereacre; Sayan Mitra; Marta Z. Kwiatkowska (IEEE Des. Test, 2015)

Building Power Consumption Models from Executable Timed I/O Automata Specifications. - Benoît Barbot; Marta Kwiatkowska; Alexandru Mereacre; Nicola Paoletti (HSCC, 2016)

Quantitative model-checking of controlled discrete-time Markov processes. - Ilya Tkachev; Alexandru Mereacre; Joost-Pieter Katoen; Alessandro Abate (Inf. Comput., 2017)

SoK: How Not to Architect Your Next-Generation TEE Malware? - Kubilay Ahmet Küçük; Steve Moyle; Andrew Martin 002; Alexandru Mereacre; Nicholas Allott (HASP@MICRO, 2022)