Jeremy Sproston 

Ricercatore (lecturer)

Dipartimento di Informatica
Università degli Studi di Torino
Corso Svizzera 185, 10149 Torino, Italy
tel: +39 011 6706772
fax: +39 011 751603
email:sproston@di.unito.it

Research interests

The use of formal methods to verify the correctness and reliability of computer systems, with emphasis on model checking methods for probabilistic timed systems.

In particular, much of my activity has concerned the formalism of probabilistic timed automata.


Publications

Full list of publications.

Recent publications:

  • Simulation and Bisimulation for Probabilistic Timed Automata, J. Sproston and A. Troina. FORMATS 2010.
  • An Extension of the Inverse Method to Probabilistic Timed Automata, E. André, L. Fribourg and J. Sproston. AVOCS 2009.
  • Strict Divergence for Probabilistic Timed Automata, J. Sproston. CONCUR 2009.
  • Model Checking Timed and Stochastic Properties with CSLTA, S. Donatelli, S. Haddad and J. Sproston. IEEE Transactions on Software Engineering, 2009.
  • Model Checking Probabilistic Timed Automata with One or Two Clocks , M. Jurdzinski, F. Laroussinie and J. Sproston, Logical Methods in Computer Science, 2008.
  • Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata N. Chamseddine, M. Duflot, L. Fribourg, C. Picaronny and J. Sproston. QEST 2008.

  • Program committees

  • QEST 2010 (7th International Conference on the Quantitative Evaluation of SysTems)
  • MOVEP 2010 (9th Summer School on Modeling and Verifying Parallel Processes)
  • SUMo 2010 (International Workshop on Scalable and Usable Model Checking for Petri Nets and Other Models of Concurrency) (program co-chair)
  • QAPL 2010 (8th Workshop on Quantitative Aspects of Programming Languages, ETAPS workshop)
  • QFM 2009 (Workshop on Quantitative Formal Methods: Theory and Applications, FM 2009 workshop)
  • QAPL 2009 (7th Workshop on Quantitative Aspects of Programming Languages, ETAPS workshop)
  • QEST 2008 (5th International Conference on the Quantitative Evaluation of SysTems)
  • MOVEP 2008 (8th Summer School on Modeling and Verifying Parallel Processes)
  • QAPL 2008 (6th Workshop on Quantitative Aspects of Programming Languages, ETAPS workshop)

  • Links

    PaCo - Performability-Aware Computing: Logics, Models, and Languages [2008-2010] (research project funded by Italian Ministry for Education, University, and Research under programme PRIN).

    PRISM - a tool for probabilistic model checking.


    Teaching (in Italian)

    Click here/cliccare qui.


    Last modified: 12/07/2010