1. M. Aiello, I. Pratt-Hartmann & J. (editors) van Benthem (2007): Handbook of Spatial Logics. Springer, doi:10.1007/978-1-4020-5587-4.
  2. A. Aziz, K. Sanwal, V. Singhal & R. Brayton (2000): Model checking Continuous Time Markov Chains. ACM Transactions on Computational Logic 1(1), pp. 162–170, doi:10.1145/343369.343402.
  3. C. Baier, B. Haverkort, H. Hermanns & J.-P. Katoen (2003): Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Transactions on Software Engineering. IEEE CS 29(6), pp. 524–541, doi:10.1109/TSE.2003.1205180.
  4. M. Bernardo, R. De Nicola & J. Hillston (2016): Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems. LNCS 9700. Springer.
  5. L. Bortolussi & J. Hillston (2015): Model checking single agent behaviours by fluid approximation. Inf. Comput. 242, pp. 183–226, doi:10.1016/j.ic.2015.03.002.
  6. L. Bortolussi & J. Hillston (2012): Fluid Model Checking. In: M. Koutny & I. Ulidowski: CONCUR, LNCS 7454. Springer, pp. 333–347, doi:10.1007/978-3-642-32940-1_24.
  7. V. Ciancia, S. Gilmore, D. Latella, M. Loreti & M. Massink (2014): Data verification for collective adaptive systems: spatial model-checking of vehicle location data. In: FoCAS Workshp @ SASO - 2014 IEEE Eighth International Conference on Self-Adaptive and Self-Organizing Systems Workshops. IEEE. Computer Society Press, pp. 32–37, doi:10.1109/SASOW.2014.16.
  8. V. Ciancia, D. Latella & M. Massink (2015): On Space in CARMA. Technical Report TR-QC-01-2015. QUANTICOL.
  9. V. Ciancia, G. Grilletti, D. Latella, M. Loreti & M. Massink (2015): An Experimental Spatio-Temporal Model Checker. In: D. Bianculli, R. Clinescu & B. Rumpe: Software Engineering and Formal Methods (SEFM 2015). Co-located Workshops, York, UK, September 7-8, 2015. Revised Selected Papers, LNCS 9509. Springer, pp. 297–311, doi:10.1007/978-3-662-49224-6_24.
  10. V. Ciancia, D. Latella, M. Loreti & M. Massink (2014): Specifying and Verifying Properties of Space. In: J. Diaz, I. Lanese & D. Sangiorgi: Theoretical Computer Science (TCS 2014), LNCS 8705. Springer, pp. 222–235, doi:10.1007/978-3-662-44602-7_18.
  11. V. Ciancia, S. Gilmore, G. Grilletti, D. Latella, M. Loreti & M. Massink (2016): On Spatio-temporal model-checking of vehicular movement in public transport systems - Preliminary Version.. Technical Report TR-QC-02-2016. QUANTICOL.
  12. V. Ciancia, D. Latella, M. Loreti & M. Massink (2016): Model Checking Spatial Logics for Closure Spaces - Extended Version.. Technical Report TR-QC-03-2016. QUANTICOL.
  13. V. Ciancia, D. Latella, M. Loreti & M. Massink (2016): Spatial Logic and Spatial Model Checking for Closure Spaces. In: Bernardo, chapter 6, pp. 156–201, doi:10.1007/978-3-319-34096-8_6.
  14. V. Ciancia, D. Latella & M. Massink (2016): On-the-Fly Mean-field Model-checking for Attribute-based Coordination. In: A. Lluch Lafuente & J. Proença: Coordination Models and Languages, LNCS 9686. Springer, pp. 67–83, doi:10.1007/978-3-319-39519-7_5.
  15. V. Ciancia, M. Latella, D. Massink, R. Paskauskas & A. Vandin (2016): A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems. In: T. Margaria & B. Steffen: ISoLA 2016, Imperial, Corfu, Greece, October 5-14, 2016, Proceedings, LNCS. Springer. (To appear).
  16. R. De Nicola, D. Latella, A. Lluch Lafuente, M. Loreti, A. Margheri, M. Massink, A. Morichetta, R. Pugliese, F. Tiezzi & A. Vandin (2015): The SCEL Language: Design, Implementation, Verification. In: M. Wirsing, M. Hölzl, N. Koch & P. Mayer: Software Engineering for Collective Autonomic Systems, chapter I.1, LNCS 8998. Springer, pp. 3–71, doi:10.1007/978-3-319-16310-9_1.
  17. A. Galton (2003): A generalized topological view of motion in discrete space. Theoretical Computer Science. 305((1-3)), pp. 111–134, doi:10.1016/S0304-3975(02)00701-6.
  18. R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. Smolka & A. Wasilewska (2008): Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes. In: M. Egerstedt & B. Mishra: Hybrid Systems: Computation and Control, 11th International Workshop, (HSCC'08) 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings, LNCS 4981. Springer, pp. 229–243, doi:10.1007/978-3-540-78929-1_17.
  19. R. Grosu, S. Smolka, F. Corradini, A. Wasilewska, E. Entcheva & E. Bartocci (2009): Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), pp. 97–105, doi:10.1145/1467247.1467271.
  20. I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Grosu & C. Belta (2015): SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: A. Girard & S. Sankaranarayanan: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC'15) Seattle, WA, USA, April 14-16, 2015. ACM, pp. 189–198, doi:10.1145/2728606.2728633.
  21. H. Hansson & B. Jonsson (1994): A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing 6, pp. 512–535, doi:10.1007/BF01211866.
  22. C. Jones (2001): Thinking Tools for the Future of Computing Science. In: R. Wilhelm: Informatics 10 Years Back 10 Years Ahead, LNCS 2000. Springer, pp. 112–130, doi:10.1007/3-540-44577-3_8.
  23. A. Kolesnichenko, P.-T. de Boer, A. Remke & B. Haverkort (2013): A logic for model-checking mean-field models. In: 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Budapest, Hungary, June 24-27, 2013. IEEE Computer Society, pp. 1–12, doi:10.1109/DSN.2013.6575345.
  24. A. Kolesnichenko, A. Remke, P.-T. de Boer & B. Haverkort (2012): A logic for model-checking of mean-field models. Technical Report TR-CTIT-12-11,
  25. K. Larsen & A. Legay (2014): Statistical Model Checking Past, Present, and Future - (Track Introduction). In: T. Margaria & B. Steffen: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II, LNCS 8803. Springer, pp. 135–142, doi:10.1007/978-3-662-45231-8_10.
  26. D. Latella, M. Loreti & M. Massink (2013): On-the-fly PCTL Fast Mean-Field Model-Checking for Self-organising Coordination - Preliminary Version. Technical Report TR-QC-01-2013. QUANTICOL.
  27. D. Latella, M. Loreti & M. Massink (2014): On-the-fly Fast Mean-Field Model-Checking. In: M. Abadi & A. Lluch Lafuente: Trustworthy Global Computing, 4th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, LNCS 8358. Springer, pp. 297–314, doi:10.1007/978-3-319-05119-2_17.
  28. D. Latella, M. Loreti & M. Massink (2015): On-the-fly Fluid Model Checking via Discrete Time Population Models. In: M. Beltrán, W. Knottenbelt & J. Bradley: Computer Performance Engineering, LNCS 9272. Springer, pp. 193–207, doi:10.1007/978-3-319-23267-6_13.
  29. D. Latella, M. Loreti & M. Massink (2015): On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination. Science of Computer Programming. 110, pp. 23–50, doi:10.1016/j.scico.2015.06.009.
  30. J.-Y. Le Boudec, D. McDonald & J. Mundinger (2007): A Generic Mean Field Convergence Result for Systems of Interacting Objects. In: QEST07. IEEE Computer Society Press, pp. 3–18, doi:10.1109/QEST.2007.8.
  31. M. Loreti & J. Hillston (2016): Modelling and Analysis of Collective Adaptive Systems with CARMA and its Tools. In: Bernardo, chapter 4, pp. 83–119, doi:10.1007/978-3-319-34096-8_4.
  32. L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti & M. Massink (2015): Qualitative and Quantitative Monitoring of Spatio-Temporal Properties. In: E. Bertocci & R. Majumdar: Runtime Verification, LNCS 9333. Springer, pp. 21–37, doi:10.1007/978-3-319-23820-3_2.
  33. S. Sebastio & A. Vandin (2013): MultiVeStA: statistical model checking for discrete event simulators. In: A. Horváth, P. Buchholz, V. Cortellessa, L. Muscariello & M. Squillante: 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools '13, Torino, Italy, December 10-12, 2013. ICST/ACM, pp. 310–315, doi:10.4108/icst.valuetools.2013.254377.

Comments and questions to:
For website issues: