Verifying Quantitative Properties of Continuous Probabilistic Timed Automata. - Marta Z. Kwiatkowska; Gethin Norman; Roberto Segala; Jeremy Sproston (CONCUR, 2000)

Decidable Model Checking of Probabilistic Hybrid Automata. - Jeremy Sproston (FTRTFT, 2000)

Model checking of probabilistic timed and hybrid systems. - Jeremy James Sproston (2000)

Symbolic Computation of Maximal Probabilistic Reachability. - Marta Z. Kwiatkowska; Gethin Norman; Jeremy Sproston (CONCUR, 2001)

Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol. - Marta Z. Kwiatkowska; Gethin Norman; Jeremy Sproston (PAPM-PROBMIV, 2002)

Automatic verification of real-time systems with discrete probability distributions. - Marta Z. Kwiatkowska; Gethin Norman; Roberto Segala; Jeremy Sproston (Theor. Comput. Sci., 2002)

Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol. - Marta Z. Kwiatkowska; Gethin Norman; Jeremy Sproston (Formal Aspects Comput., 2003)

CSL Model Checking for the GreatSPN Tool. - Davide D'Aprile; Susanna Donatelli; Jeremy Sproston (ISCIS, 2004)

Backward Stochastic Bisimulation in CSL Model Checking. - Jeremy Sproston; Susanna Donatelli (QEST, 2004)

Model Checking for Probabilistic Timed Systems. - Jeremy Sproston (Validation of Stochastic Systems, 2004)

Model Checking Durational Probabilistic Systems. - François Laroussinie; Jeremy Sproston (FoSSaCS, 2005)

Verifying Stochastic Well-formed Nets with CSL Model-Checking Tools. - Davide Cerotti; Davide D'Aprile; Susanna Donatelli; Jeremy Sproston (ACSD, 2006)

CSL Model Checking for Generalized Stochastic Petri Nets. - Davide Cerotti; Susanna Donatelli; András Horváth; Jeremy Sproston (QEST, 2006)

Performance analysis of probabilistic timed automata using digital clocks. - Marta Z. Kwiatkowska; Gethin Norman; David Parker 001; Jeremy Sproston (Formal Methods Syst. Des., 2006)

Backward Bisimulation in Markov Chain Model Checking. - Jeremy Sproston; Susanna Donatelli (IEEE Trans. Software Eng., 2006)

CSLTA: an Expressive Logic for Continuous-Time Markov Chains. - Susanna Donatelli; Serge Haddad; Jeremy Sproston (QEST, 2007)

From Time Petri Nets to Timed Automata: An Untimed Approach. - Davide D'Aprile; Susanna Donatelli; Arnaud Sangnier; Jeremy Sproston (TACAS, 2007)

Symbolic model checking for probabilistic timed automata. - Marta Z. Kwiatkowska; Gethin Norman; Jeremy Sproston; Fuzhi Wang (Inf. Comput., 2007)

State explosion in almost-sure probabilistic reachability. - François Laroussinie; Jeremy Sproston (Inf. Process. Lett., 2007)

Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata. - Najla Chamseddine; Marie Duflot; Laurent Fribourg; Claudine Picaronny; Jeremy Sproston (QEST, 2008)

Model Checking Probabilistic Timed Automata with One or Two Clocks. - Marcin Jurdzinski; Jeremy Sproston; François Laroussinie (Log. Methods Comput. Sci., 2008)

Strict Divergence for Probabilistic Timed Automata. - Jeremy Sproston (CONCUR, 2009)

Model Checking Timed and Stochastic Properties with CSL^{TA}. - Susanna Donatelli; Serge Haddad; Jeremy Sproston (IEEE Trans. Software Eng., 2009)

Simulation and Bisimulation for Probabilistic Timed Automata. - Jeremy Sproston; Angelo Troina (FORMATS, 2010)

Performability Measure Specification: Combining CSRL and MSL. - Alessandro Aldini; Marco Bernardo 001; Jeremy Sproston (FMICS, 2011)

Discrete-Time Verification and Control for Probabilistic Rectangular Hybrid Automata. - Jeremy Sproston (QEST, 2011)

Solving Parity Games on Integer Vectors. - Parosh Aziz Abdulla; Richard Mayr; Arnaud Sangnier; Jeremy Sproston (CONCUR, 2013)

An extension of the inverse method to probabilistic timed automata. - Étienne André; Laurent Fribourg; Jeremy Sproston (Formal Methods Syst. Des., 2013)

Model checking for probabilistic timed automata. - Gethin Norman; David Parker 001; Jeremy Sproston (Formal Methods Syst. Des., 2013)

Exact and Approximate Abstraction for Classes of Stochastic Hybrid Systems. - Jeremy Sproston (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014)

Verification and Control of Probabilistic Rectangular Hybrid Automata. - Jeremy Sproston (FORMATS, 2015)

Qualitative Analysis of VASS-Induced MDPs. - Parosh Aziz Abdulla; Radu Ciobanu; Richard Mayr; Arnaud Sangnier; Jeremy Sproston (FoSSaCS, 2016)

Analysis of Timed Properties Using the Jump-Diffusion Approximation. - Paolo Ballarini; Marco Beccuti; Enrico Bibbona; András Horváth; Roberta Sirovich; Jeremy Sproston (EPEW, 2017)

Verification and control for probabilistic hybrid automata with finite bisimulations. - Jeremy Sproston (J. Log. Algebraic Methods Program., 2019)

Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. - James C. A. Main; Mickael Randour; Jeremy Sproston (CONCUR, 2021)

Probabilistic Timed Automata with Clock-Dependent Probabilities. - Jeremy Sproston (Fundam. Informaticae, 2021)

Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities. - Jeremy Sproston (Log. Methods Comput. Sci., 2021)

Timed Games with Bounded Window Parity Objectives. - James C. A. Main; Mickael Randour; Jeremy Sproston (FORMATS, 2022)

Qualitative reachability for open interval Markov chains. - Jeremy Sproston (PeerJ Comput. Sci., 2023)

Clock-Dependent Probabilistic Timed Automata with One Clock and No Memory. - Jeremy Sproston (ICFEM, 2024)