Laura Nenzi

Laura Nenzi photo
I am a research collaborator of the research unit SysMA (System Modelling and Analysis), at IMT School for Advanced Studies Lucca. Since April 2013, I'm a member of the European research project QUANTICOL (A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours).
Research Interests
My research interests regard formal methods applied to design and analyse complex systems. Currently, I am working in the development of an original formal framework to validate and optimize the behaviour of complex systems, keeping track of their spatial dynamical properties. In particular, I am designing spatio-temporal logics to express formal requirements on the performance of the system, and developing scalable model checking algorithms to validate them; furthermore, I am working to provide a formal setting for parameter estimation and system design problem for these kind of systems. 
I received my PhD in Computer Decision and Systems Science (XVIII Cycle) from IMT, in 2016.  My thesis supervisors were Prof. Luca Bortolussi (University of Trieste) and Prof. Rocco De Nicola (IMT). From November 2014 to May 2015, I was a visiting student within the group of Modeling and Simulation (MoSi) at the Saarland University, Saarbrücken, Germany. 
I received my master degree in 2012 at the University of Trieste with a thesis on a logic-based approach to determine the connection between biological modules and their behavioral properties. My supervisor was Prof. Luca Bortolussi. During my master I was a visitor at the University of Edinburgh for 3 months. 
I received my bachelor degree in mathematics at the University of Padova in 2010 with a thesis on biomechanical models for pattern formation under the supervision of Prof. Francesco Fassò and Prof. Marco Favretti. During my bachelor I visited, for 9 months, the University of Wariwick, granted by the Erasmus exchange program.
Journal Papers
  • E. Bartocci, L. Bortolussi, L. Nenzi, G. Sanguinetti, System Design of Stochastic Models using Robustness of Temporal Properties, in Theoretical Computer Science, vol. 587, pp. 3-25, 2015.
Conference Papers
  • E. Bartocci, L. Bortolussi, L. Nenzi, D. Milios, G. Sanguinetti, Studying Emergent Behaviours in Morphogenesis using Signal Spatio-Temporal Logic, in Proc. of HSB 2015: the 4nd Intern. Workshop on Hybrid Systems and Biology, Madrid, Spain, 2015.
  • L. Nenzi, L. Bortolussi, V. Ciancia, M. Loreti, M. Massink, Qualitative and Quantita- tive Monitoring of Spatio-Temporal Properties, in Proc. of Runtime Verification 2015: The 15th International Conference on Runtime Verification, Vienna, Austria, 2015.
  • L. Bortolussi, L. Nenzi, Specifying and monitoring properties of stochastic spatio- temporal systems in signal temporal logic, in Proc. of VALUETOOLS 2014: the 8th International Conference on Performance Evaluation Methodologies and Tools, Bratislava, Slovakia, pp. 66-73, 2014.
  • E. Bartocci, L. Bortolussi, L. Nenzi, G. Sanguinetti, On the robustness of temporal properties for stochastic models, in Proc. of HSB 2013: the 2nd Intern. Workshop on Hybrid Systems and Biology, Taormina, Italy, vol. 125(1), pp. 3-19, 2013.
  • E. Bartocci, L. Bortolussi, L. Nenzi, A temporal logic approach to modular design of synthetic biological circuits, in Proceedings of CMSB 2013: the 11th International Conference on Computational Methods in Systems Biology, Austria, Springer-Verlag, Lecture Notes in Computer Science, vol. 8130, pp. 164-178, 2013 .