Ugo Montanari and Software Verification

  • Gian-Luigi Ferrari
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5065)


The great honour of introducing the Chapter on Software Verification for the Festschrift dedicated to Ugo Montanari brings to mind a very personal memory. I was a young Ph.D. student and I was discussing something with Ugo, or better I was learning something from Ugo about how one could apply the abstract notions of category theory in order to understand better the problems raised from concurrency and synchronization. At a certain point Ugo wanted to interrupt our talk because a seminar by Jaco de Bakker on the denotational semantics of concurrency by metric spaces was about to begin. I was very familiar with the works of de Bakker having studied them for my Laurea thesis under Ugo’s supervision. Following my request to continue our discussion, Ugo replied, “Let’s go to the seminar. We can always learn something listening to de Bakker”.


Label Transition System Cryptographic Protocol Leak Detection Denotational Semantic Mobile Process 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148(1), 1–70 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Boreale, M., Bruni, R., Caires, L., Nicola, R.D., Lanese, I., Loreti, M., Martins, F., Montanari, U., Ravara, A., Sangiorgi, D., Vasconcelos, V.T., Zavattaro, G.: SCC: A service centered calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  3. 3.
    Bouali, A., Gnesi, S., Larosa, S.: The integration project for the jack environment. EATCS Bulletin, Centrum voor Wiskunde en Informatica (CWI) 54, 207–223 (1994)zbMATHGoogle Scholar
  4. 4.
    Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FC2TOOLS set. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 441–445. Springer, Heidelberg (1996)Google Scholar
  5. 5.
    Ciancia, V., Montanari, U.: A name abstraction functor for named sets. In: Coalgebraic Methods in Computer Science 2008 (to appear, 2008)Google Scholar
  6. 6.
    Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)CrossRefGoogle Scholar
  7. 7.
    Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems. ACM Transactions on Programming Languages and Systems 15(1), 36–72 (1993)CrossRefGoogle Scholar
  8. 8.
    Ferrari, G.L., Ferro, G., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: An Automata Based Verification Environment for Mobile Processes. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 275–289. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  9. 9.
    Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Trans. Softw. Eng. Methodol. 12(4), 440–473 (2003)CrossRefGoogle Scholar
  10. 10.
    Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: Verifying Mobile Processes in the HAL Environment. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 511–515. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  11. 11.
    Ferrari, G.L., Montanari, U., Pistore, M.: Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 129–143. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Ferrari, G.L., Montanari, U., Tuosto, E.: Coalgebraic minimization of HD-automata for the pi-calculus using polymorphic types. Theor. Comput. Sci. 331(2-3), 325–365 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Ferrari, G.L., Montanari, U., Tuosto, E., Victor, B., Yemane, K.: Modelling fusion calculus using HD-automata. In: Fiadeiro, J.L., Harman, N.A., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 142–156. Springer, Heidelberg (2005)Google Scholar
  14. 14.
    Focardi, R., Gorrieri, R.: A classification of security properties. Journal of Computer Security 3(1) (1995)Google Scholar
  15. 15.
    Gabbay, M., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Asp. Comput. 13(3-5), 341–363 (2002)zbMATHCrossRefGoogle Scholar
  16. 16.
    Gadducci, F., Miculan, M., Montanari, U.: About permutation algebras (pre)sheaves and named sets. Higher-Order and Symbolic Computation 19(2-3), 283–304 (2006)zbMATHCrossRefGoogle Scholar
  17. 17.
    Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I and II. Information and Computation 100(1), 1–40,41–77 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Montanari, U., Buscemi, M.: A First Order Coalgebraic Model of π-Calculus Early Observational Equivalence. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 449–465. Springer, Heidelberg (2002)Google Scholar
  19. 19.
    Montanari, U., Pistore, M.: Checking Bisimilarity for Finitary π-Calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 42–56. Springer, Heidelberg (1995)Google Scholar
  20. 20.
    Montanari, U., Pistore, M.: Finite state verification for the asynchronous pi-calculus. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 255–269. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  21. 21.
    Montanari, U., Pistore, M.: Structured coalgebras and minimal HD-automata for the pi-calculus. Theor. Comput. Sci. 340(3), 539–576 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Montanari, U., Pistore, M., Yankelevich, D.: Efficient minimization up to location equivalence. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol. 1058, pp. 265–279. Springer, Heidelberg (1996)Google Scholar
  23. 23.
    Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)CrossRefGoogle Scholar
  24. 24.
    Pistore, M.: History Dependent Automata. PhD Thesis, Dipartimento di Informatica, Università di Pisa (1999)Google Scholar
  25. 25.
    Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Sangiorgi, D., Walker, D.: The π-Calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Gian-Luigi Ferrari
    • 1
  1. 1.Dipartimento di InformaticaUniversity of PisaItaly

Personalised recommendations