Luca Tesei's Research Activity  -

Research interests, with relative publication indexes (see below)

• Formal methods for modelling and verifying complex systems, in particular real-time systems:
  • automata, timed automata, probabilistic automata  [J1, J2, J3, J4, J5, J9, J10, C1, C2, C3, C5, C7, C11, C12, C16, T1]
  • timed non-interference properties [J2, J4, C3, C5, T1]
  • untimed and timed process algebras  [J3, J12, J13, C13, T2, P1]
  • model checking [J3, J10, C11, P1]
• Abstract Interpretation:
  
  • static analysis of programming languages [J8, C4]
  • verification of security properties [J3, J6, C6]
• Systems Biology:
  • modelling of biological systems, emerging behaviours [J9, J10, J11, J12, J13, C11, C12, C13, C14, C15, C16, C17, C18, C19, T2, P1, P2]
  • simulation of biological systems [J12, J13, C8, C9, C10, C11, C12, C13, C14, C15, C16, C17, C18, C19, T2, P1, P2]
  • membrane computing, ecological models  [J9, J11, C12, C16, C17]
• Digital Services and Quality of Service
  • formal models for digital services [C7]
  • quality assessment [J7]

Projects

• 2008 – Italian national project PRIN 2007: Performability-Aware Computing: Logiche, Modelli e Linguaggi (PaCo). Coordinator Prof. Marco Bernardo – Member of the Research Unit of Camerino as contract researcher, Local Coordinator Prof. Flavio Corradini. Project Web site: http://www.sti.uniurb.it/paco/index.html
• 2008 – Italian national project FIRB 2003: Laboratory for Interdisciplinary Technologies in Bioinformatics (LITBIO). Coordinator Dott. Luciano Milanesi – Collaborator of the Research Unit of Camerino as contract researcher, Local Coordinator Prof. Emanuela Merelli. Project Web site: http://www.litbio.org/main.htm
• 2005 – 2006 Italian national project PRIN 2004: AIDA - Interpretazione Astratta: Progettazione e Applicazioni. Coordinator Prof. Roberto Giacobazzi – Member of the Research Unit of Bologna as Post Doc, Local Coordinator Prof. Maurizio Gabbrielli.
• 2004 Italian national project PRIN 2002: Constraint-based Verification of Reactive Systems (CoVer). Coordinator Prof. Maurizio Gabbrielli – Collaborator of the Unit of Research of Bologna as Post Doc.
• 2002 – 2003 Italian national project PRIN 2001: Metodi Formali per la Sicurezza e il Tempo (MEFISTO). Coordinator Prof. Roberto Gorrieri – Member of the Reserach Unit of Pisa as PhD student.

Recent and Coming Events/Activities

• Invited Talk to 6th Workshop on Computation of Biochemical Pathways and Genetic Networks Date: 16-17 September 2010, Heidelberg, Germany. Presentation: "Space, geometry, motion and interactions in modeling biological systems: the BioShape approach"
• 12th Italian Conference of Theoretical Computer Science (ICTCS 2010) at Camerino. Date: 15-17 September 2010, Camerino, Italy
• Participation to PaCo Italian PRIN Project Meeting, 14-15 September 2010, Camerino, Italy
• Participation to MeCBIC 2010, CMC11, AMCA-POP 2010, 23-27 August 2010, Jena, Germany. Presentation given at MeCBIC 2010: "Multiscale Bone Remodelling with Spatial P Systems". Paper accepted at AMCA-POP: “An Individual-based Probabilistic Model for Fish Stock Simulation”, presented by Federico Buti.
• Visiting the School of Computer Science, Reykjavik University, 16-22 August 2010, Reykjavik, Iceland. Activities: Internationalization, Double Deegre Programme, Research Collaboration. Seminar Given for ICE-TCS: "Space, geometry, motion and interactions in modeling biological systems"
• Participation to MeTTeG 2010, 30 June - 2 July 2010, Olten, Switzerland. 
• Visiting the School of Business of the University of Applied Sciences NorthWerstern Switzerland, 30 June - 4 July 2010, Olten, Switzerland. Activities: Internationalization, Double Degree Programme.
• Visiting the Medical Technology Laboratory of Rizzoli Orthopaedic Institute of Bologna. June 27-28 2010, Bologna, Italy. Research collaboration.
• Participation to CS2Bio 2010, June 10 2010, Amsterdam, The Netherlands. Presentation given: "Bone Remodelling in BioShape"
• 7th International Workshop on Simulation of Multiphysics Multiscale Systems, at ICCS 2010, May 31 - June 2 2010, Amsterdam, The Netherlands. Accepted Paper "BioShape: a spatial shape-based scale-independent simulation environment for biological systems" presented by Diletta Cacciagrano.
• Participation to PaCo Italian PRIN Project Meeting, 2-3 March 2010, L'Aquila, Italy.
• Visiting the Medical Technology Laboratory of Rizzoli Orthopaedic Institute of Bologna. January 15 2010, Bologna, Italy. Research collaboration.

Laboratory/Tools

• The BioShape simulator @ CosyLab
• FishPass, Fish Stock monitoring tool @ CosyLab 

List of Publications

Disclaimer: Most of the papers available from this document appear in print and the corresponding copyright is held by the publisher. The papers can be used for personal use, but redistribution or reprinting for commercial purposes is prohibited.

Journal Papers:

[J1]

R. Barbuti, N. De Francesco, and L. Tesei, ``Timed Automata with non-Instantaneous Actions,'' Fundamenta Informaticae, vol. 47, no. 3-4, pp. 189-200, 2001.
ISSN: 0169-2968. [Pdf, BibTex]

[J2]

R. Barbuti, N. De Francesco, A. Santone, and L. Tesei, ``A Notion of non-Interference for Timed Automata,'' Fundamenta Informaticae, vol. 51, no. 1-2, pp. 1-11, 2002.
ISSN: 0169-2968. [Pdf, BibTex]

[J3]

N. De Francesco, A. Santone, and L. Tesei, ``Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems,'' Fundamenta Informaticae, vol. 54, no. 2-3, pp. 195-211, 2003.
ISSN: 0169-2968. [Pdf, BibTex]

[J4]

R. Barbuti and L. Tesei, ``A Decidable Notion of Timed non-Interference,'' Fundamenta Informaticae, vol. 54, no. 2-3, pp. 137-150, 2003.
ISSN: 0169-2968. [Pdf, BibTex]

[J5]

R. Barbuti and L. Tesei, ``Timed Automata with Urgent Transitions,'' Acta Informatica, vol. 40, no. 5, pp. 317-347, 2004.
ISSN: 0001-5903. [Pdf, BibTex]

[J6]

R. Barbuti, S. Cataudella, and L. Tesei, ``Abstract Interpretation against Races,'' Fundamenta Informaticae, vol. 60, no. 1-4, pp. 57-79, 2004.
ISSN: 0169-2968. [Pdf, BibTex]

[J7]

F. Corradini, A. Polzonetti, B. Re, and L. Tesei, ``Quality of Service in e-Government underlines the role of information usability,'' International Journal of Information Quality (IJIQ), vol. 2, no. 2, pp. 133-151, 2008.
ISSN: 1751-0457. doi:10.1504/IJIQ.2008.022960   [Pdf]

[J8]

R. Barbuti, N. De Francesco, and L. Tesei, ``An Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier,'' The Computer Journal, vol. 53, no. 6, pp. 679-700, 2010.
First published online: April 23, 2009 - Online ISSN: 1460-2067 - Print ISSN: 0010-4620. doi:10.1093/comjnl/bxp031 [Pdf] 

[J9]

R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, and L. Tesei, ``Timed P Automata,'' Fundamenta Informaticae, vol. 94, no. 1, pp. 1-19, 2009.
ISSN: 0169-2968. doi:10.3233/FI-2009-114 [Pdf] 

[J10]

E. Bartocci, F. Corradini, E. Merelli, and L. Tesei, ``Detecting Synchronisation of Biological Oscillators by Model Checking,'' Theoretical Computer Science, vol. 411, no. 20, pp. 1999-2018, 2010.
ISSN: 0304-3975. doi:10.1016/j.tcs.2009.12.019 [Pdf]

[J11]

R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, G. Pardini, and L. Tesei, ``Spatial P Systems,'' Natural Computing, vol. 10, no. 1, pp. 3-16, 2011.
Received: 26 October 2009 Accepted: 24 February 2010 Published online: 24 March 2010 - ISSN: 1567-7818 (Print) 1572-9796 (Online). doi:10.1007/s11047-010-9187-z [Pdf]

[J12]

E. Bartocci, F. Corradini, M. R. Di Berardini, E. Merelli, and L. Tesei, ``Shape Calculus. A Spatial Mobile Calculus for 3D Shapes,'' Scientific Annals of Computer Science, vol. 20, pp. 1-31, 2010.
ISSN: 1843-8121. [pdf]

[J13]

E. Bartocci, D. Cacciagrano, M. R. Di Berardini, E. Merelli, and L. Tesei, ``Timed Operational Semantics and Well-formedness of Shape Calculus,'' Scientific Annals of Computer Science, vol. 20, pp. 33-52, 2010.
ISSN: 1843-8121. [pdf]

Conference/Workshop Proceedings:

[C1]

R. Barbuti, N. De Francesco, and L. Tesei, ``Timed Automata with non-Instantaneous Actions,'' in Proc. of 9th Concurrency, Specification & Programming Workshop (CS&P'2000) (H. Burkhard, L. Czaja, A. Skowron, and P. Starke, eds.), no. 140 in Informatik-Bericht, (Berlin, Germany), pp. 17-28, Humboldt-Universität Press, October 2000.
ISSN: 0863-095X.

[C2]

R. Barbuti and L. Tesei, ``Timed Automata with Urgent Transitions,'' in Proc. of 2nd Int. Workshop on Models for Time-Critical Systems (MTCS'01) (F. Corradini and W. Vogler, eds.), no. NS-01-5 in BRICS Notes, (Aarhus, Denmark), pp. 3-21, Aarhus University Press, August 2001.
ISSN: 0909-3206.

[C3]

R. Barbuti, N. De Francesco, A. Santone, and L. Tesei, ``A Notion of non-Interference for Timed Automata,'' in Proc. of 10th Concurrency, Specification & Programming Workshop (CS&P'2001) (L. Czaja, ed.), vol. 583/2001, (Warsaw, Poland), pp. 6-15, Warsaw University, Zakad Graficzny UW, October 2001.

[C4]

R. Barbuti, C. Bernardeschi, N. De Francesco, and L. Tesei, ``Fixing the Java bytecode verifier by a suitable type domain,'' in Proc. of 14th Int. Conf. on Software engineering and knowledge engineering (SEKE '02), (New York, NY, USA), pp. 377-382, ACM, July 2002.
ISBN: 1-58113-556-4. [Pdf, BibTex]

[C5]

R. Barbuti and L. Tesei, ``A Decidable Notion of Timed non-Interference,'' in Proc. of 11th Concurrency, Specification & Programming Workshop (CS&P'2002) (H. Burkhard, L. Czaja, G. Lindemann, A. Skowron, and P. Starke, eds.), no. 161 in Informatik-Bericht, (Berlin, Germany), pp. 20-38, Humboldt-Universität Press, October 2002.
ISSN: 0863-095X.

[C6]

R. Barbuti, S. Cataudella, and L. Tesei, ``Abstract Interpretation against Races,'' in Proc. of 12th Concurrency, Specification & Programming Workshop (CS&P'2003) (L. Czaja, ed.), vol. 591/2003, (Czarna, Poland), pp. 55-66, Warsaw University, Zakad Graficzny UW, September 2003.

[C7]

D. Cacciagrano, F. Corradini, R. Culmone, L. Tesei, and L. Vito, ``A model-prover for constrained dynamic conversations,'' in Proc. of 10th Int. Conf. on Information Integration and Web-based Applications & Services (iiWAS '08), (New York, NY, USA), pp. 630-633, ACM, 2008.
ISBN: 978-1-60558-349-5. doi: 10.1145/1497308.1497428 [Pdf]

[C8]

N. Cannata, F. Corradini, E. Merelli, and L. Tesei, ``A Spatial Simulator for Metabolic Pathways,'' in Workshop Notes of Sistemi MultiAgente & Bioinformatica (MAS&BIO 2008), (Cagliari, Italy), pp. 31-46, September 2008. [Pdf]

[C9]

N. Cannata, F. Corradini, E. Merelli, and L. Tesei, ``A spatial model and simulator for metabolic pathways,'' in Proc. of 8th Int. Workshop on Network Tools and Applications in Biology (NETTAB '08), Systems Biology for health Collection, (Varenna (LC), Italy), pp. 40-42, Sysbiohealth, May 2008. [Pdf]

[C10]

R. Alfieri, N. Cannata, E. Merelli, L. Milanesi, and L. Tesei, ``Using SKOS to formalize parameter estimation in systems biology,'' in Proc. of 8th Int. Workshop on Network Tools and Applications in Biology (NETTAB '08), Systems Biology for health Collection, (Varenna (LC), Italy), pp. 13-15, Sysbiohealth, May 2008.

[C11]

E. Bartocci, F. Corradini, E. Merelli, and L. Tesei, ``Model Checking Biological Oscillators,'' Electr. Notes Theor. Comput. Sci., vol. 229, no. 1, pp. 41-58, 2009.
In Proc. of 2nd Int. Workshop From Biology to Concurrency and back (FBTC 2008), Reykjavik, Iceland, July 12, 2008 - ISSN: 1571-0661. doi:10.1016/j.entcs.2009.02.004 [Pdf]

[C12]

R. Barbuti, A. Maggiolo-Schettini, P. Milazzo, and L. Tesei, ``Timed P Automata,'' Electr. Notes Theor. Comput. Sci., vol. 227, pp. 21-36, 2009.
Proc. of 2nd Int. Meeting on Membrane Computing and Biologically Inspired Process Calculi (MecBic 2008), Iasi, Romania, September 3-4, 2008 - ISSN: 1571-0661. doi:10.1016/j.entcs.2008.12.102 [Pdf]

[C13]

E. Bartocci, M. R. Di Berardini, F. Corradini, E. Merelli, and L. Tesei, ``A Shape Calculus for Biological Processes,'' in Proc. of 11th Italian Conference on Theroretical Computer Science (ICTCS '09), (Cremona, Italy), pp. 30-33, September 28-30 2009. [Pdf]

[C14]

F. Buti, D. R. Cacciagrano, F. Corradini, E. Merelli, and L. Tesei, ``BioShape: a spatial shape-based scale-independent simulation environment for biological systems,'' Procedia Computer Science, vol. 1, pp. 827-835, May 2010.
In Proc. of Simulation of 7th Int. Workshop on Multiphysics Multiscale Systems, within (ICCS 2010), Amsterdam, The Netherlands, May 31 - June 2, 2010 - ISSN: 1877-0509. [Pdf]

[C15]

F. Buti, D. Cacciagrano, F. Corradini, E. Merelli, L. Tesei, and M. Pani, ``Bone Remodelling in BioShape,'' Electr. Notes Theor. Comput. Sci. 268:17-19, 2010  In Proc. of 1st Int. Workshop on Interactions between Computer Science and Biology (CS2Bio 2010), Amsterdam, The Netherlands, June 10, 2010 - ISSN: 1571-0661 

[C16]

F. Buti, F. Corradini, E. Merelli, E. Paschini, P. Penna, and L. Tesei, ``An Individual-based Probabilistic Model for Fish Stock Simulation,'' in Proceedings Compendium of the 4th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2010) and of the 1st Workshop on Applications of Membrane Computing, Concurrency, and Agent-based Modelling in Population Biology (AMCA-POP 2010), (Jena, Germany), Friedrich Schiller University Jena, Pro BUSINESS Verlag, August 2010.
Presented at AMCA-POP 2010 - ISBN: 978-3-86805-767-6 [link]

[C17]

D. Cacciagrano, F. Corradini, E. Merelli, and L. Tesei, ``Multiscale Bone Remodelling with Spatial P Systems,'' in Proceedings Compendium of the 4th Workshop on Membrane Computing and Biologically Inspired Process Calculi (MeCBIC 2010) and of the 1st Workshop on Applications of Membrane Computing, Concurrency, and Agent-based Modelling in Population Biology (AMCA-POP 2010), (Jena, Germany), Friedrich Schiller University Jena, Pro BUSINESS Verlag, August 2010.
Presented at MeCBIC 2010 - ISBN: 978-3-86805-767-6 [link]

[C18]

F. Buti, D. Cacciagrano, and L. Tesei, ``BioShape: a uniform multi-scale simulator for biological systems,'' in Proc. of 12th Italian Conference on Theoretical Computer Science (ICTCS 2010), (Camerino, Italy), September 2010.

Invited at Workshops/Conferences

[C19]

L. Tesei, ``Space, Geometry, Motion and Interactions in Modeling Biological Systems: the BioShape Approach,'' in Proc. of 6th Workshop on Computation of Biochemical Pathways and Genetic Networks, (Heidelberg, Germany), pp. 73-79, Logos Verlag, Berlin, September 2010.
ISBN: 978-3-8325-2587 

 

Posters Presented at Workshops/Conferences

[P1]

M. Callisto De Donato, F. Corradini, M. R. Di Berardini, E. Merelli, and L. Tesei, ``Tailoring the Shape Calculus for Quantitative Analysis,'' in Poster at 2nd Metting of ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA 2010), (Edinburgh, UK), July 2010.

[P2]

F. Buti, D. Cacciagrano, F. Corradini, E. Merelli, and L. Tesei, ``Bone Remodelling @ UNICAM,'' in Poster at 8th Conference on Computational Methods in Systems Biology (CMSB 2010), (Trento, Italy), September 2010.

Theses and Technical Reports:

[T1]

Luca Tesei, Specification and Verification using Timed Automata.
PhD thesis, Dipartimento di Informatica, University of Pisa, 2004.
Series TD - 6/04.

Abstract Text	Table of Contents PDF	Full Postscript	Full PDF	Full gzip ps	BibTeX entr

[T2]

E. Bartocci, F. Corradini, M. R. Di Berardini, E. Merelli, and L. Tesei, ``Shape Calculus: A spatial calculus for 3D colliding shapes,'' Tech. Rep. 6, Dipartimento di Matematica e Informatica, University of Camerino, 2009.
Available at http://s1report.cs.unicam.it/6/.

Slides:

1. Luca Tesei. Specification and Verification of real-time Systems with Timed Automata. Talk based on the first part of the Phd Thesis, held at Seminar @ cs.unicam seminar cycle, june 2006.

   PDF

Curriculum Vitae

Available only in Italian: