Major Publications

Follow the links for Postscript or PDF versions of some papers.

Important Notice

These are preliminary versions of appeared (or going to appear) papers. For final versions, please see cited journals or proceedings.
Most of the papers available from this document appear in print, and the corresponding copyright is held by the publisher.
The papers can be downloaded for personal use, but redistribution or reprinting for commercial purposes is prohibited.

Recent conference and journal publications (2001-today)

  1. Z. Dang, P. San Pietro, R. Kemmerer, On Presburger Liveness of Discrete Timed Automata, in STACS2001, 18th Symposium on Theoretical Aspects of Computer Science, Dresden, February 15-17th, 2001, pp. 132-143, LNCS 2010, Springer-Verlag, New York

  2. J. Berstel, S. Crespi Reghizzi, G. Roussel, P. San Pietro, A scalable formal method for Design and Automatic Checking of User Interfaces, ICSE 2001, Int. Conference on Software Engineering, Toronto, Ontario, Canada, May 12-19, 2001, pp 453-462, IEEE Press, New York., 2001.

  3. V. Martena, P. San Pietro, Alias Analysis by means of a Model Checker, in CC2001, International Conference on Compiler Construction, Genova, Italia, 2 - 6 April, 2001, pp 3-20, LNCS 2027, Springer-Verlag, New York.

  4. A. Cherubini, S. Crespi Reghizzi, P. San Pietro, Some structural properties of Associative Language Descriptions, ICTCS 2001, Seventh Italian Conference on Theoretical Computer Science. Torino, Italy, October 4th - 6th, 2001, pp 172-183, LNCS 2202, Springer Verlag. New York.

  5. Z. Dang, O. Ibarra, P. San Pietro, Liveness Verification of Reversal-bounded Multicounter Machines with a Free Counter, FSTTCS 2001, 21st Foundations Of Software Technology And Theoretical Computer Science, December 13--15, 2001, Bangalore, India.In LNCS 2245, pp. 132-143, 6th November 2001, Springer Verlag, New York.

  6. U.Foschi, M. Giuliani, A. Morzenti, M. Pradella, P. San Pietro: Software procurement and methods for specification and validation in the railway transportation industry, in IEEE Conference on Systems, Man and Cybernetics SMC02, Hammamet (Tunisia), Oct 4-6 2002.

  7. O. Ibarra, Z. Dang, P. San Pietro, Verification in Loosely Synchronous Queue-Connected Discrete Timed Automata, Theoretical Computer Science. vol 290 (30 Jan 2003), pp. 1713 –1735. Elsevier Publishing, Amsterdam.

  8. M. Verdicchio, P. San Pietro, Model Checking the Secure Electronic Transaction Protocol, DASD 2003 (Design, Analysis and Simulation of Distributed Systems), Mar 30 – Apr 4, 2003, Orlando, FL, USA.

  9. Z. Dang, P. San Pietro, R. Kemmerer, On Presburger Liveness of Discrete Timed Automata, Theoretical Computer Science, Vol. 299, Issue 1, 18 April 2003, pp. 413-438. Elsevier Publishing, Amsterdam.

  10. Umberto Foschi, Mauro Giuliani, Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro: The Role of Formal Methods in Software Procurement for the Railway Transportation Industry, in FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems. 15-16 May 2003, Budapest, Hungary.

  11. Gaoyan Xie, Zhe Dang, Oscar Ibarra, and Pierluigi San Pietro, Dense counter machines and verification problems, in CAV03: 15th Computer-Aided Verification Conference. Boulder, Colorado, USA, July 8 -- 12, 2003.

  12. P. San Pietro and Z. Dang, Automatic verification of multi-queue discrete timed automata, in COCOON 03: 9th International Computing and Combinatorics Conference, July 25-28, 2003, Big Sky, MT, USA.

  13. A. Cherubini, S. Crespi Reghizzi, P. San Pietro, Associative Language Descriptions, Theoretical Computer Science, 270, Issue 1-2, 6 January 2002, pp. 463-491.

  14. A. Morzenti, M. Pradella, P. San Pietro, P. Spoletini, Model Checking TRIO specifications in SPIN, in FM 03: Formal Methods Europe Conference, Pisa, September 2003.

  15. A. Morzenti, M. Pradella, P. San Pietro, P. Spoletini, Practical Model Checking of LTL with Past, in ATVA03: 1st Workshop on Automated Technology for Verification and Analysis, Taipei, Taiwan, 2003, p 135-146. 10-13 December 2003.

  16. A. Campi, E. Martinez, P. San Pietro, Experiences with a Formal Method for Design and Automatic Checking of User Interfaces, Position paper in IUI/CADUI'2004 Workshop on Making Model-Based UI Design Practical: usable and open methods and tools, Madeira, Portugal, 13th January, 2004.

  17. M. Verdicchio, P. San Pietro, Model Checking-Aided Design of Secure Distributed Systems, SE 2004: IASTED International Conference on Software Engineering, February 17-19, 2004, Innsbruck, Austria.

  18. Marcella Anselmo, Alessandra Cherubini, Pierluigi San Pietro, Regular Languages and Associative Language Descriptions, in JM2004: Journées Montoises d'Informatique Théorique à Liège, 8-11 Septembre 2004 .

  19. Zhe Dang, Oscar Ibarra, Pierluigi San Pietro, Gaoyan Xie. Real-Counter Automata and Applications to Verification, in FSTTCS 2004, 24th Foundations Of Software Technology And Theoretical Computer Science, December 16--18, 2004, Chennai, India.

  20. J. Berstel, S. Crespi Reghizzi, G. Roussel, P. San Pietro, A scalable formal method for Design and Automatic Checking of User Interfaces, ACM TOSEM, Volume 14, Number 2 (April 2005).

  21. P. San Pietro, Potenza e limiti del calcolo automatico: problemi intrattabili, Mondo Digitale, pp. 63-70, vol. 4, Dec. 2005.

  22. Alessandra Cherubini, Stefano Crespi-Reghizzi, Matteo Pradella, Pierluigi San Pietro: Picture languages: Tiling systems versus tile rewriting grammars. Theor. Comput. Sci. 356(1-2): 90-103 (2006).

  23. Beletska A., San Pietro P., Extracting Coarse-Grained Parallelism with the Affine Transformation Framework and its Limitations. Electronic Modelling, no.5, 2006.

  24. Ciapessoni E, Mandrioli D., Morzenti A., San Pietro P., The defense of electric power systems: an approach exploiting formal methods. : SIXTH INTERNATIONAL WORLD ENERGY SYSTEM CONFERENCE, Torino, Jul. 10-12 2006, pp. 98-105.

  25. D. Bianculli, P. Spoletini, A. Morzenti, M. Pradella, P. San Pietro, Model checking temporal metric specifications with Trio2Promela, IPM International Symposium on Fundamentals of Software Engineering (FSEN 2007), April 17-19 Teheran, Iran. LNCS 4767, pp 388-395, 2007.

  26. D. Bianculli, A. Morzenti, M. Pradella, P. San Pietro, P. Spoletini, Trio2Promela: a model checker for temporal metric specifications, 29th Int. Conference on Software Engineering (ICSE 2007), Research Demonstrations Track, Minneapolis, MN, USA, May 10-19, 2006. In ICSE 2007 Companion, pp 61-62, IEEE Computer Society Press , New York, 2007.

  27. Beletska A., Bielecki W., San Pietro P., Extracting Coarse-Grained Parallelism in Program Loops with the Slicing Framework. In Proceedings of ISPDC 2007, 6th International Symposium on Parallel and Distributed Computing. July 5–8, Hagenberg, Austria, IEEE Computer Society Press..

  28. Bielecki W., Beletska A., Palkowski M., San Pietro P., Extracting Synchronization-free chains of dependent iterations in non-uniform loops. In Proceedings of International Conference on Advanced Computer Systems ACS'2007, Miedzyzdroje, Poland, 17-19 October 2007. Vol 2 pp. 189-198.

  29. Beletska A., Bielecki W., San Pietro P., Extracting Synchronization-Free Slices of Operations in Perfectly-Nested Loops. In Proceedings of the 19th International Conference on Parallel and Distributed Computing and Systems PDCS'2007, November 19 – 21, 2007, Cambridge, Massachusetts, USA.

  30. M. Pradella, A. Morzenti, P. San Pietro, The Symmetry of the Past and of the Future: Bi-infinite Time in the Verification of Temporal Properties, Proceedings of The 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007), Dubrovnik, Croatia, September 3-7, 2007.

  31. Marcella Anselmo, Alessandra Cherubini, Pierluigi San Pietro, Regular Languages and Associative Language Descriptions, DISCRETE MATHEMATICS AND THEORETICAL COMPUTER SCIENCE. vol. 9(2) 2007, pp. 153-174 ISSN: 1462-7264.

  32. Bielecki W., Beletska A., Palkowski M., San Pietro P., Finding synchronization-free parallelism represented with trees of dependent operations, ICA3PP 2008, International Conference on Algorithms and Architectures 2008, Cyprus 9-11 June 2008, in Lecture Notes on Computer Science, Springer Verlag.

  33. A. Beletska, W. Bielecki, K. Siedlecki, P. San Pietro, Finding synchronization-free slices of operations in arbitrarily nested loops. ICCSA 2008, International Conference on Computational Science and Its Applications. University of Perugia, Perugia, June 30th -July 3rd, 2008

  34. S.Crespi Reghizzi and P. San Pietro, Consensual Definition of Languages by Regular Sets. LATA 2008 (Language and Automata Theory and Applications), Tarragona (Spain), April 2008. LNCS Volume 5196/2008, Sprinter Verlag.

  35. M. Pradella, A. Morzenti, P. San Pietro, Benchmarking Model- and Satisfiability-Checking on bi-infinite time, ICTAC 2008, volume 5160 of Lecture Notes in Computer Science, pages 290-304. Springer-Verlag, Sep. 2008.

  36. M. Pradella, A. Morzenti, P. San Pietro, Refining Real-Time System Specifications through Bounded Model- and Satisfiability-Checking, ASE 2008 (23rd IEEE/ACM Conference on Automated Software Engineering), L'Aquila, 15-19 Sept. 2008. IEEE Computer Society Press, New York, pp. 119 – 127. ISBN: 978-1-4244-2187-9.

Publications before 2001:

International Conferences and Workshops

  1. A. Cherubini, S. Crespi, P. San Pietro, Languages Based on Structural Local Testability, in C.S. Calide, M.J.Dinneen, Proceedings of DMTCS’99, Auckland, New Zealand, 18-21, January 1999, Springer, Singapore.

  2. A. Cherubini, P. San Pietro, A Polynomial-Time Parsing Algorithm for a Class of non-deterministic two-Stack Automata, Proceedings of the 4-th Italian Conference on Theoretical Computer Science, (A. Marchetti-Spaccamela, P. Mentrasti, M. Venturini-Zilli eds.), L’Aquila, Italia, pp.150-164, World Scientific Publishing, Singapore, October 1992.

  3. A. Cherubini, P. San Pietro, A Polynomial-Time Parsing Algorithm for k-depth Languages, in G. Pighizzini, P. San Pietro (eds.), Proceedings of the ASMICS Workshop on Parsing Theory, Milano, October 1994.

  4. A. Cherubini, P. San Pietro, The word problem for k-depth grammars, pp. 29-39, in J. Almeida, G.M.S. Gomes, P. Silva (eds.), Semigroups, Automata and Languages, World Scientific Publishing, Singapore, 1996.

  5. A. Cherubini, P. San Pietro, Multi-Depth Grammars and Label-Distinguished Control Grammars , 1st Int. Conference on Semigroups and Algebraic Engineering (AE97), Aizu-Wakamatsu, Japan, March 24-28, 1997.

  6. A. Cherubini, P. San Pietro, Tree-Adjoining Grammars and k-depth Grammars, 8th Conference on Automata and Formal Languages (AFL’96), Salgotarjan, Hungary, 29 July - 2 August, 1996.

  7. A. Coen-Porisini, M. Pradella, P. San Pietro, A Finite-domain Semantics for Executing Temporal Logic Specifications , in Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRFT'98), Lyngby, Denmark, Sept 16-18, 1998, Spinger-Verlag LNCS 1486, pp. 41-54.

  8. S. Crespi-Reghizzi, M. Pradella, P. San Pietro, Conciseness of Associative Language Descriptions, Int. Workshop on Descriptional Complexity of Automata, Grammars and Related Structures, Magdeburg, Germany, July 20-23, pp. 99-108, 1999.

  9. A. Morzenti, P. San Pietro, S. Morasca, A tool for automated system analysis based on modular specifications, in 13th IEEE International Conference on Automated Software Engineering (ASE98), Honolulu, Hawaii, USA, October 13-16, 1998, pp. 2-11.

  10. A. Morzenti, P. San Pietro, TRIO+, An Object Oriented Logic Language for Modular System Specification, in P. America (ed.), ECOOP ‘91, 5th European Conference on Object-Oriented Programming, Geneve, LNCS 512 Springer Verlag, July 1991.

  11. E. Corsetti, D. Mandrioli, A.Montanari, A. Morzenti, P. San Pietro, Dealing with Different Time Scales in Formal Specifications , Sixth IEEE-ACM SIGSOFT Int. Workshop on Software Specification and Design, Como, 25-26 October 1991.

  12. G. Pighizzini, P. San Pietro (eds.), Proceedings of the ASMICS Workshop on Parsing Theory, Milano, October 1994.

  13. M. Basso, E.Ciapessoni, E.Crivelli, D.Mandrioli, A.Morzenti, E.Ratto, P.San Pietro, "Experimenting a Logic-Based Approach to the Specification and Design of the Control System of a Pondage Power Plant", in M. Wirsing (ed.) Proceedings of the ICSE-17 Workshop on Industrial Application of Formal Methods, Seattle, WA, USA, April 1995.

  14. M. Felder and P. San Pietro, Finite time semantics for executable logic specifications, (poster), in W. Halang, A. Stoyenko (eds), Real-Time Computing, Proceedings of the NATO ASI, Saint Martin, Dutch Antille, 5-17 October 1992, Series F, Vol. 127, Springer Verlag, New York,1992.

  15. M. Felder and P. San Pietro, Testing by executing logical specifications (poster), in W. Halang, A. Stoyenko (eds), Real-Time Computing, Proceedings of the NATO ASI, Saint Martin, Dutch Antille, 5-17 October 1992, Series F, Vol. 127, Springer Verlag, New York,1992.

  16. S. Castano, V. De Antonellis, P. San Pietro, Reuse of Object-Oriented Requirements Specifications, ER 93, 12th Int. Conference on the Entity-Relationship Approach, Dallas, USA, LNCS 823, Springer Verlag, New York, December 1993.

  17. S. Morasca, A. Morzenti, P. San Pietro, Generating Functional Test Cases in-the-large for Time-critical Systems from Logic-based Specifications , Proc. of ISSTA 1996, ACM-SIGSOFT International Symposium on Software Testing and Analysis, San Diego, California, January 1996.

  18. A. Casazza, D. Comini, A. Morzenti, M. Pradella, P. San Pietro, F. Schreiber, Specification and Test Case Generation for the Safety Kernel of the Naples Subway, in N. Callaos, A. Cherif (eds), Proceedings of Int. Conf. on Information Systems Analysis and Synthesis '99, Orlando Florida, July 31-August 4, 1999

Other International Journals (before 2001)

  1. E. Ciapessoni, E. Corsetti, A.Montanari, P. San Pietro, Embedding Time Granularity in a Logical Specification Language for Synchronous Real-Time Systems, Science of Computer Programming , 20(1993), pp. 141-171, Elsevier Publishing, Amsterdam, 1993.

  2. San Pietro P., Morzenti, A., Morasca, S., Generation of Execution Sequences for Modular Time-Critical Systems , IEEE Trans. on Software Engineering, vol. 26 n. 2, Feb. 2000, pp. 128-149.

  3. A. Morzenti, P. San Pietro, Object-Oriented Logic Specifications of Time Critical Systems, ACM Transactions on Software Engineering Methodologies , January 1994, pp.56-98, ACM, New York, 1994.

  4. A. Cherubini, P. San Pietro, A Polynomial-Time Parsing Algorithm for K-Depth Languages, Journal of Computer and System Sciences, Vol. 52, n. 1, Feb. 1996, pp. 61-79, Academic Press, Orlando, Florida.

  5. A. Cherubini, P. San Pietro, On the relation between multi-depth grammars and tree adjoining grammars, Publ. Math., 51/3-4 (1997), 1-17.

  6. S. Morasca, A. Morzenti, P. San Pietro, An application of a tool for automated system analysis based on modular specifications, Journal of Automated Software Engineering, pp. 125-155,Volume 7, Issue 2, May 2000.

  7. A. Cherubini, P. San Pietro, Tree Adjoining Languages and Multi-Pushdown Languages, Theory of Computing Systems, vol. 33, n.4, pp 257-293, Jul. 2000 . (formerly Mathematical Systems Theory).

  8. S. Crespi Reghizzi, M. Pradella, P. San Pietro, Associative Definition of Programming Languages, Computer Languages 26(2000) 105-123.

Chapters in Books

  1. Mandrioli D., Morzenti A., Pezzè M., San Pietro P. Silva S. "A Petri Net and Logic Approach to the Specification and Verification of Real Time Systems" in Formal Methods for Real-Time Computing , Heitmeyer C., Mandrioli D. (editors), John Wiley & Sons, New York, 1996.

  2. G. Finzi, F. Rebucci, P. San Pietro, E. Sanzo, Modelli stocastici con ingressi esterni a scatola nera e grigia, in G. Finzi (ed.), Modelli per la previsione e gestione della qualità dell’aria, CUSL, Milano, 1988.

  3. A. Cherubini, P. San Pietro, On the Relation between Multi-Depth Grammars and Label-Distinguished Control Grammars, in C.L. Nehaniv, M. Ito (eds.), Algebraic Engineering, World Scientific Publ., Singapore, 1999.

  4. M. Basso, E.Ciapessoni, E.Crivelli, D.Mandrioli, A.Morzenti, E.Ratto, P.San Pietro, A Logic-Based Approach to the Specification and Design of the Control System of a Pondage Power Plant, in Colin Tully (ed.) Improving Software Practice: case experiences, John Wiley, New York, 1998.


Books for Students

  1. D. Mandrioli, A. Morzenti, P. San Pietro, Esercizi di Informatica Teorica, Esculapio, Bologna, 1994.

  2. S. Paraboschi, P. San Pietro, Esercizi di Linguaggi e Traduttori , CLUP, Milano, 1994.

  3. A. Morzenti, P. San Pietro, Introduzione al Linguaggio TRIO , Dipartimento di Elettronica e Informazione, Politecnico di Milano,1993.


Ph.D. Dissertation

  1. P. San Pietro, Specifiche logiche object-oriented di sistemi in tempo reale di grandi dimensioni, Tesi di Dottorato di Ricerca, Dipartimento di Elettronica e Informazione, Politecnico di Milano, 1994.


Main Research Reports

  1. P. San Pietro, Two-Stack Automata , Rapporto Interno n. 92-073, Dipartimento Di Elettronica e Informazione, Politecnico di Milano, Milano.

  2. A. Morzenti P. San Pietro, "Manuale di TRIO +", ENEL-CRA Research Report, 1993.

  3. D. Mandrioli, A. Morzenti, P. San Pietro, Time Granularity in Logical Specifications, Rapporto Interno n. 93-019, Dipartimento Di Elettronica e Informazione, Politecnico di Milano, Milano.

  4. A. Morzenti P. San Pietro, "Manuale di TRIO +*", ENEL-CRA Research Report, 1995.

  5. A. Coen-Porisini, R. Kemmer, P. San Pietro, A formal semantics for the ASTRAL specification language, Rapporto Interno n. 96-051, Dipartimento di Elettronica e Informazione, Politecnico di Milano, Milano.

Back to my home page