Model checking languages and applications

  • NEW G.Pardini, P.Milazzo. A High-Level Model Checking Language with Compile-time Pruning of Local Variables. 5th International Symposium “From Data to Models and Back (DataMod)”, (Vienna, 8 July 2016). Accepted for publication.
  • P.Milazzo, G.Pardini, D.Sestini, P.Bove. Case Studies of Application of Probabilistic and Statistical Model Checking in Game Design. Fourth International Workshop on Games and Software Engineering (GAS 2015), (Florence, Italy, 18 May 2015). IEEE Computer Society, pages 29-35, 2015. draft @ieeexplore

Components and modular pathway verification

  • G.Pardini, P.Milazzo, A.Maggiolo-Schettini. Component identification in biochemical pathways. Theoretical Computer Science, Volume 587, pages 104-124, 2015. @elsevier
  • G.Pardini, P.Milazzo, A.Maggiolo-Schettini. Identification of components in biochemical pathways: extensive application to SBML models. Natural Computing, Volume 13, Issue 3, pages 351-365, 2014. @springer
  • P.Drábik, A.Maggiolo-Schettini, P.Milazzo, G.Pardini. Modular Verification of Qualitative Pathway Models with Fairness. Scientific Annals of Computer Science, Volume XXIII, Issue 1, pages 75-117, 2013.
  • G.Pardini, P.Milazzo, A.Maggiolo-Schettini. An Algorithm for the Identification of Components in Biochemical Pathways. CS2Bio 2013, 4th International Workshop on Interactions between Computer Science and Biology, (Florence, Italy, June 6, 2013). ENTCS, Volume 299, pages 69-84, 2013. draft @springer
  • A.Maggiolo-Schettini, P.Milazzo and G.Pardini. Application of a Semi-automatic Algorithm for Identification of Molecular Components in SBML Models. Wivace 2013, Italian Workshop on Artificial Life and Evolutionary Computation, (Milan, Italy, July 1-2, 2013), EPTCS 130, pages 43-52, 2013.

Formal methods in systems biology

  • NEW R.Barbuti, P.Bove, P.Milazzo, G.Pardini. Minimal probabilistic P systems for modelling ecological systems. Theoretical Computer Science 608(1), pages 36-56, 2015. @elsevier
  • R.Barbuti, A.Maggiolo-Schettini, P.Milazzo, G.Pardini, S.Tini. Systolic automata and P systems. Chapter in: C.S. Calude, R. Freivalds, I. Kazuo (Eds.), Gruska Festschrift, Computing with New Resources, LNCS 8808, pages 17-31, 2014. @springer
  • G.Pardini, R.Barbuti, A.Maggiolo-Schettini, P.Milazzo, S.Tini. Compositional Semantics and Behavioural Equivalences for Reaction Systems with Restriction. Theoretical Computer Science, Volume 551, pages 1-21, 2014. @elsevier
  • R.Barbuti, P.Bove, A.Maggiolo-Schettini, P.Milazzo, G.Pardini. A computational formal model of the invasiveness of eastern species in European water frog populations. 2nd International Symposium on Modelling and Knowledge Management for Sustainable Development (MoKMaSD 2013), (Madrid, Spain, 24 September 2013), Springer LNCS, Volume 8368, pages 329-344, 2014. @springer
  • G.Pardini, R.Barbuti, A.Maggiolo-Schettini, P.Milazzo, S.Tini. A Compositional Semantics of Reaction Systems with Restriction. Computability in Europe 2013 (CiE 2013), (Milan, Italy, July 1-5, 2013), Springer LNCS, Volume 7921, pages 330-339, 2013. @springer
    • Full proofs of theorems are available.
  • R.Barbuti, A.Maggiolo-Schettini, P.Milazzo and G.Pardini. Spatial Calculus of Looping Sequences. Theoretical Computer Science, Volume 412, Issue 43, pages 5976-6001, 2011. @elsevier
  • R.Barbuti, A.Maggiolo-Schettini, P.Milazzo, G.Pardini and A.Rama. A Process Calculus for Molecular Interaction Maps. 3rd Int. Meeting on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC'09), Bologna, Italy, September 2009, EPTCS 11, pages 33-49, 2009. @eptcs
  • R.Barbuti, D.Lepri, A.Maggiolo-Schettini, P.Milazzo, G.Pardini and A.Rama. Simulation of Kohn's Molecular Interaction Maps Through Traslation into Stochastic CLS+. 7th Int. Conference Perspectives of System Informatics, Novosibirsk, Russia, June 2009, Springer LNCS, Volume 5947, pages 58-69, 2010. draft @springer
  • R.Barbuti, A.Maggiolo-Schettini, P.Milazzo and G.Pardini. Spatial Calculus of Looping Sequences. Int. Workshop From Biology to Concurrency and Back (FBTC'08), Elsevier ENTCS, Volume 229, Number 1, pages 21-39, Reykjavik, Iceland, July, 2008. draft @elsevier
  • R. Barbuti, G. Caravagna, A. Maggiolo-Schettini, P. Milazzo and G. Pardini. The Calculus of Looping Sequences. Chapter in: M.Bernardo, P.Degano and G.Zavattaro (Eds.): Formal Methods for Computational Systems Biology (SFM 2008), Springer LNCS 5016, pages 387-423, 2008. draft @springer

Membrane computing

  • V. Manca, G.Pardini. Morphogenesis through moving membranes. Natural Computing, Volume 13, Issue 3, pages 403-419, 2014. draft @springer
  • R.Barbuti, A.Maggiolo-Schettini, P.Milazzo, G.Pardini. Simulation of Spatial P system models. Theoretical Computer Science, Volume 529, pages 11-45, 2013. @elsevier
  • R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, G. Pardini and L. Tesei. Spatial P Systems. Natural Computing, Volume 10, Issue 1, pages 3-16, 2011. draft @springer

Lazy Monitoring (formal methods in security)

  • G.Caravagna, G.Costa, G.Pardini. Lazy Security Controllers. STM 2012 - 8th International Workshop on Security and Trust Management, (Pisa, Italy, September 13-14, 2012), LNCS 7783, pages 33-48, 2013. @springer
    • Full proofs of theorems are available.
  • G.Caravagna, G.Costa, G.Pardini, L.Wiegand. Log-based Lazy Monitoring of OSGi Bundles. BYTECODE 2012 - Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Tallinn, Estonia, pages 1-8, 2012. pdf
  • G.Caravagna, G.Costa, L.Wiegand, G.Pardini. Lazy Monitoring for Distributed Computing Environments. Sixth International Conference on Innovative Mobile and Internet Services in Ubiquitous Computing, IMIS 2012 (Palermo, Italy, July 4-6, 2012). IEEE Computer Society, pages 259–265, 2012. @ieee
  • G.Caravagna, G.Costa, G.Pardini. Lazy Security Controllers. Technical Report IIT-CNR TR-28/2011. @cnr


  • G. Pardini. Formal Modelling and Simulation of Biological Systems with Spatiality. University of Pisa, June 2011. PhD Thesis. @etd
  • G. Pardini. Topological Calculus of Looping Sequences. University of Pisa, October 2007. MSc Thesis @etd