PROFUNDIS: Proofs of Functionality for Mobile Distributed Systems

[ Overview | Meetings | Visits | Events | Publications | Tools | Internal information ]

Publications of the PROFUNDIS project

Years 1-4 (2002-2005)

The list below is also available in BibTeX format.

(You can also see the publication list year-by-year: Year 1, Year 2, Year 3, and Year 4.)

1. R. Amadio and W. Charatonik, On name generation and set-based analysis in Dolev-Yao model (Extended Abstract).
   In Proc. CONCUR'02, LNCS 2421, Springer Verlag. 2002.
2. R. Amadio, D. Lugiez, and V. Vanackere, On the symbolic reduction of processes with cryptographic functions.
   Theoretical Computer Science, 290(1), pp 695-740. 2002.
3. R. Amadio and C. Meyssonnier, On decidability of the control reachability problem in the asynchronous pi-calculus.
   Nordic Journal of Computing, 9(2), pp 70-101. 2002.
4. Roberto M. Amadio, Gérard Boudol, and Cédric Lhoussaine, On Message Deliverability and Non-Uniform Receptivity.
   Fundamenta Informaticae, 53(2), pp 105-129. 2002.
5. Roberto M. Amadio, Gérard Boudol, and Cédric Lhoussaine, On message deliverability and non-uniform receptivity.
   Technical report 05-2002, LIF. May 2002.
6. Roberto M. Amadio and Silvano Dal Zilio, Resource Control for Synchronous Cooperative Threads.
   In CONCUR 2004 - 15th International Conference on Concurrency Theory, Lecture Notes in Computer Science 3170, Springer-Verlag. August 2004.
7. Michael Baldamus, Jesper Bengtson, Gianluigi Ferrari, and Roberto Raggi, Web Services as a New Approach to Distributing and Coordinating Semantics-Based Verification Toolkits.
   In Proceedings of the First International Workshop on Web Services and Formal Methods (WSFM 2004), ENTCS 105, Elsevier. February 2004.
8. M. Baldamus, R. Mayr, and G. Schneider, A Backward/Forward Strategy for Verifying Safety Properties of Infinite-State Systems.
   Technical report 2003-065, Department of Information Technology, Uppsala University, Sweden. 2003.
9. Michael Baldamus, Joachim Parrow, and Björn Victor, A Fully Abstract Encoding of the pi-Calculus with Data Terms.
   In Proceedings of ICALP'05, LNCS , Springer. 2005.
10. Michael Baldamus, Joachim Parrow, and Björn Victor, Spi Calculus Translated to pi-Calculus Preserving May-Tests.
    In Proceedings of LICS'04, Computer Society Press. July 2004.
11. M. Baldamus, J. Parrow, and B. Victor, Spi Calculus Translated to \largepi-Calculus Preserving May Testing.
    Technical report 2003-063, Department of Information Technology, Uppsala University, Sweden. 2003.
12. M. Baldamus, A Fully-Abstract Model for the Fusion Calculus.
    Preliminary Draft. 2003.
13. Giacomo Baldi, Andrea Bracciali, Gianluigi Ferrari, and Emilio Tuosto, A Coordination-based Methodology for Security Protocol Verification.
    In WISP'04, ENCTS 121, Elsevier. 2005.
14. G. Baldi, A. Bracciali, G. Ferrari, and E. Tuosto, ASPASyA: an Automated Tool for Security Protocol Analysis based on a Symbolic Approach.
    Submitted for publication. 2003.
15. G. Barthe, A. Basu, and T. Rezk, Security Types Preserving Compilation.
    In Proc. of VMCAI'04, Lecture Notes in Computer Science 2937, Springer Verlag. 2004.
16. G. Barthe, A. Basu, and T. Rezk, Security Types Preserving Compilation.
    Journal of Computer Languages, Systems and Structures. 2005. To appear.
17. G. Barthe, P. D'Argenio, and T. Rezk, Secure Information Flow by Self-Composition.
    In Proceedings of CSFW'04, IEEE Press. 2004.
18. G. Barthe and L. Prensa-Nieto, Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems.
    In Proceedings of FMSE'04, ACM Press. 2004.
19. G. Barthe and L. Prensa Nieto, Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems.
    manuscript.
20. G. Barthe and T. Rezk, Non-interference for a JVM-like language.
    In Proceedings of TLDI'05, ACM Press. 2005.
21. G. Barthe and T. Rezk, Secure Information Flow for the JVM.
    Manuscript.
22. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Enforcing Secure Service Composition.
    In IEEE Computer Security Foundation Workshop. 2005.
23. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, History-based Access Control with Local Policies.
    In FOSSACS 2005, Lectures Notes in Computer Science 3441, Springer. 2005.
24. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Method Inlining in Presence of Stack Inspection.
    In Workshop on Issues in the Theory of Security (WITS'04). 2004.
25. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Policy Framings for Access Control.
    In Workshop on Issues in the Theory of Security (WITS'05). 2005.
26. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Program Transformations under Dynamic Security Policies.
    In MEPHISTO Final Workshop, Electronic Notes in Computer Science 99, Elsevier. 2004.
27. M. Bartoletti, P. Degano, and G. Ferrari, Stack Inspection and Secure Program Transformations.
    International Journal of Information Security, 2(3-4), pp 187-217. 2004.
28. Jesper Bengtsson, http://www.it.uu.se/research/reports/2004-041">Generic Implementations of Process Calculi in Isabelle.
    In Proceedings of the 16th Nordic Workshop on Programming Theory, IT Technical Reports . October 2004.
29. L.Bettini, V.Bono, R.De Nicola, G.Ferrari, D.Gorla, M.Loreti, E.Moggi, R.Pugliese, E.Tuosto, and B.Venneri, The KLAIM Project: Theory and Practice.
    In Global Computing: Programming Environments, Languages, Security and Analysis of Systems, LNCS . 2003.
30. M. Boreale, M. Buscemi, and U. Montanari, D-Fusion: a Distinctive Fusion Calculus.
    In Proc. of the Second Asian Symposium on Programming Languages and Systems (APLAS 2004), Lecture Notes in Computer Science 3302, Springer Verlag. 2004.
31. Michele Boreale, Marzia Buscemi, and Ugo Montanari, A General Name Binding Mechanism.
    In Proc. of Symposium on Trustworthy Global Computing (TGC '05), Lecture Notes in Computer Science , Springer Verlag. 2005. To appear.
32. M. Boreale and M. Buscemi, A Framework for the Analysis of Security Protocols.
    In Proc. CONCUR'02, LNCS 2421, Springer Verlag. 2002.
33. Michele Boreale and Marzia Buscemi, A Framework for the Analysis of Security Protocols.
    Theoretical Computer Science. 2005. To appear.
34. M. Boreale and M. Buscemi, STA, a Tool for the Analysis of Cryptographic Protocols (Online version).
    Dipartimento di Sistemi ed Informatica, Università di Firenze, and Dipartimento di Informatica, Università di Pisa,. 2002.
35. M. Boreale and M. Buscemi, Symbolic Analysis of Crypto-Protocols based on Modular Exponentiation.
    In Proc. of MFCS 2003, Lecture Notes in Computer Science 2747 , Springer-Verlag. 2003. An extended version appears in Proc. of FCS'03.
36. A. Bracciali, A. Brogi, G. Ferrari, and E. Tuosto, Security and dynamic composition of open systems.
    In Proc. Int. Conference on Parallel and Distributed Techniques and applications, CSREA Press. 2002.
37. A. Bracciali, A. Brogi, G. Ferrari, and E. Tuosto, Security and dynamic composition of WEB services.
    In Proc. Int. Conference on Parallel and Distributed Techniques and applications, CSREA Press, USA. 2002.
38. Marzia Buscemi and Ugo Montanari, A Compositional Coalgebraic Model of Monadic Fusion Calculus.
    Submitted for publication. 2005.
39. Marzia Buscemi and Ugo Montanari, A congruence result for process calculi with structural axioms.
    Submitted for publication. 2005.
40. M. Buscemi and U. Montanari, A First Order Coalgebraic Model of Pi-Calculus Early Observational Equivalence.
    In Proc. CONCUR'02, LNCS 2421, Springer Verlag. 2002. Full version in Technical Report TR-02-14, Dipartimento di Informatica, Universitá di Pisa, August 2002.
41. M. Buscemi, Models and Security Verification of Mobile Systems.
    PhD thesis, Dipartimento di Matematica, University of Neaples ``Federico II''. 2003.
42. Palamidessi C., Saraswat V., F. Valencia, and B. Victor, Linearity vs Persistency in the Pi-Calculus.
    Manuscript.
43. L. Caires and L. Cardelli, A Spatial Logic for Concurrency (Part I).
    Information and Computation, 186(2), pp 194--235. 2003.
44. L. Caires and L. Cardelli, A Spatial Logic for Concurrency (Part II).
    In CONCUR 2002: Concurrency Theory (13th International Conference), Lecture Notes in Computer Science. Springer-Verlag. 2002. Also as Technical Report 3/2002/DI/PLM/FCTUNL.
45. L. Caires and L. Cardelli, A spatial logic for concurrency-II.
    Theoretical Computer Science, 322(3), pp 517--565. 2004.
46. L. Caires and E. Lozes, Elimination of quantifiers and undecidability in spatial logics for concurrency.
    In Proc. of CONCUR'04, Lecture Notes in Computer Science , Springer Verlag. 2004.
47. L. Caires and E. Lozes, Elimination of quantifiers and undecidability in spatial logics for concurrency.
    Theoretical Computer Science. 2005. Accepted for publication.
48. L. Caires, Behavioral and Spatial Properties in a Logic for the Pi-Calculus.
    In Proc. of Foundations of Software Science and Computation Structures'2004, Lecture Notes in Computer Science , Springer Verlag. 2004.
49. L. Caires, Model-Checking of Spatial Properties in the pi-calculus.
    Research report 3, DI/FCT/UNL. December 2002.
50. Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, and Jean-Marc Talbot, Model Checking Mobile Ambients.
    Theoretical Computer Science, 308(1), pp 277--331. November 2003.
51. Silvano Dal Zilio and Denis Lugiez, A Logic you Can Count On.
    In POPL 2004 - 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2004.
52. Silvano Dal Zilio and Denis Lugiez, XML Schema, Tree Logic and Sheaves Automata.
    In RTA 2003 - 14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 2706, Springer. June 2003.
53. S. Dantchev and F.D. Valencia, On infinite CSP's.
    In Proc. Third International CP'05 Workshop on Modelling and Reformulating CSP's. 2005.
54. Yuxin Deng and Catuscia Palamidessi, Axiomatizations for probabilistic finite-state behaviors.
    In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science 3441, Springer. 2005.
55. Yuxin Deng and Davide Sangiorgi, Ensuring termination by typability.
    In Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science, Kluwer. 2004.
56. Y. Deng and D. Sangiorgi, Ensuring termination by typability.
    Submitted. 2005.
57. Yuxin Deng and Davide Sangiorgi, Towards an algebraic theory of typed mobile processes.
    In Proceedings of the 31th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 3142, Springer. 2004.
58. Yuxin Deng and Davide Sangiorgi, Towards an algebraic theory of typed mobile processes.
    Theoretical Computer Science. 2005. To appear.
59. Rocco DeNicola, Gianluigi Ferrari, Ugo Montanari, Rosario Pugliese, and Emilio Tuosto, A Process Calculus for QoS-Aware Applications.
    In Coordination 2005, Lectures Notes in Computer Science 3454, Springer. 2005.
60. M. Miculan F. Gadducci and U. Montanari, Some Characterization Results for Permutation Algebras.
    In Workshop COMETA, ENTCS 104, Elsevier. 2003.
61. G. Ferrari, S. Gnesi, U. Montanari, and M. Pistore, A model checking verification environment for mobile processes.
    ACM Transactions on Software Engineering and Methodologies (TOSEM), 12(4), pp 440-473. 2004.
62. Gianluigi Ferrari, Stefania Gnesi, Ugo Montanari, Roberto Raggi, Gianluca Trentanni, and Emilio Tuosto, Verification on the WEB.
    In Verification and Validation of Enterprise Information Systems, INSTICC Press. April 2004.
63. Gianluigi Ferrari and Alberto Lluch-Lafuente, A Logic for Graphs with QoS.
    In First International Workshop on Views On Designing Complex Architectures, Electronic Notes in Computer Science , Elsevier. September 2004.
64. G. Ferrari, E. Moggi, and R. Pugliese, Guardians for Ambient Based Monitoring.
    In Proc. Foundations of Wide Area Network Programming, ENTCS , Elseviers. 2002.
65. G. Ferrari, E. Moggi, and R. Pugliese, MetaKlaim: A type safe multi-stage language for Global computing.
    Mathematical Structures in Computer Science, 14(3), pp 367-395. 2004.
66. G. Ferrari, U. Montanari, and E. Tuosto, Coalgebraic Minimization of HD-automa in a polymorphic lambda-calculus.
    Theoretical Computer Science, 331(2-3), pp 325-365. 2005.
67. G. Ferrari, U. Montanari, R. Raggi, and E. Tuosto, From Co-algebraic Specifications to Implementation: The MIHDA toolkit.
    In First International Symposium on Formal Methods for Components and Objects (FMCO), Springer Lecture Notes in Computer Science , Springer. 2003.
68. G. Ferrari, U. Montanari, R. Raggi, and E. Tuosto, From Coalgebraic Specification to Toolkit Development.
    Technical report TR-02-19, Technical Report, Dipartimento di Informatica Universita' di Pisa. 2002.
69. G. Ferrari, U. Montanari, and M. Pistore., Minimizing Transition Systems for Name-passing Calculi: A Co-algbraic Formulation.
    In Proc. FOSSACS'02, LNCS 2303, Springer Verlag. 2002.
70. Gianluigi Ferrari, Ugo Montanari, and Emilio Tuosto, Model Checking for Nominal Calculi.
    In FOSSACS, LNCS 3441, Springer. 2005.
71. Gianluigi Ferrari, Ugo Montanari, Emilio Tuosto, Björn Victor, and Kidane Yemane, Modelling Fusion calculus using HD-automata.
    In To appear in in First Conference on Algebra and Coalgebra in Computer Science CALCO'05, LNCS , Springer. 2005.
72. G. Ferrari, U. Montanari, E. Tuosto, B. Victor, and K. Yemane, Modelling and Minimising the Fusion Calculus using HD-automata.
    Technical report, University of Pisa. 2003.
73. Gianluigi Ferrari, Ugo Montanari, and Emilio Tuosto, Verification on the WEB of Name-Passing Process Calculi.
    In Workshop on Software Engineering Tools: Compatibility and Integration, Monterey Workshop Series, LNCS . 2004. To appear.
74. Fabio Gadducci, Marino Miculan, and Ugo Montari, About permutation algebras, (pre)sheaves and named sets.
    Submitted for publication, International Journal on Higher-Order and Symbolic Computation. 2004.
75. S. Gay, V. T. Vasconcelos, and A. Ravara, Session types for inter-process communication.
    Technical report , Department of Computer Science, University of Lisbon. 2002.
76. Simon Gay, Vasco T. Vasconcelos, and Ant\'onio Ravara, Session Types for Inter-Process Communication.
    Technical report 2003--133, Department of Computing, University of Glasgow. March 2003.
77. Neil Ghani, Kidane Yemane, and Björn Victor, Relationally Staged Computations in Calculi of Mobile Processes.
    In Proceedings of CMCS 2004 (7th International Workshop on Coalgebraic Methods in Computer Science), ENTCS 106, Elsevier. 2004.
78. P. Giambiagi, G. Schneider, and F. Valencia, On the Expressiveness of CCS-like Calculi.
    In In Proceedings of FOSSACS'04, LNCS, Springer-Verlag. 2004.
79. P. Giannini, D. Sangiorgi, and A. Valente, A distributed abstract machine for Safe Ambients.
    Extended and refined version of a paper appeared in ICALP'01. 2002.
80. D. Hirschkoff, E. Lozes, and D. Sangiorgi, Minimality Results for the Spatial Logics.
    In Proc. of FSTTCS'2003, LNCS , Springer Verlag. 2003.
81. D. Hirschkoff, E. Lozes, and D. Sangiorgi, Separability, Expressiveness and Decidability in the Ambient Logic.
    In Proc. of LICS'02, IEEE Computer Society. 2002.
82. D. Hirschkoff, D. Pous, and D. Sangiorgi, An Efficient Abstract Machine for Safe Ambients.
    In Proc. of COORDINATION '05, Lecture Notes in Computer Science 3454, Springer Verlag. 2005.
83. D. Hirschkoff, An Extensional Spatial Logic for Mobile Processes.
    In Proc. of CONCUR'04, 3170, Springer Verlag. 2004.
84. I. Lanese and U. Montanari, Mapping Fusion and Synchronized Hyper-edge Replacement into Logic Programming.
    Theory and Practice of Logic Programming. 2005. To appear.
85. Francesca Levi and Davide Sangiorgi, Mobile Safe Ambients.
    ACM Transactions on Programming Languages and Systems (TOPLAS), 25(1), pp 1-69. January 2003.
86. Alberto Lluch-Lafuente and Ugo Montanari, Quantitative mu-calculus and CTL defined over constraint semirings.
    In QAPL (2004), Electronic Notes in Computer Science 112, Elsevier. 2005.
87. E. Lozes, Adjunct elimination in the static Ambient Logic.
    In Proc. of EXPRESS'2003, Electronic Notes in Computer Science 96. 2003.
88. E. Lozes, Expressivité des logiques d'espaces.
    PhD thesis, École Doctorale MathInf, ENS Lyon. 2004.
89. E. Lozes, Separation logic preserves the expressive power of classical logic.
    In Proc. Workshop Space'04. 2004. Electronic publication.
90. Denis Lugiez and Silvano Dal Zilio, Multitrees Automata, Presburger's Constraints and Tree Logics.
    Technical report 08-2002, LIF. June 2002. http://www.lim.univ-mrs.fr/Rapports/08-2002-Lugiez-DalZilio.html.
91. Denis Lugiez and Silvano Dal Zilio, XML Schema, Tree Logic and Sheaves Automata.
    Technical report 4631, INRIA. November 2002. http://www.inria.fr/rrrt/rr-4631.html.
92. I. Scagnetto M. Miculan, A Framework for Typed HOAS and Semantics.
    In Proc. of PPDP 2003, Uppsala, Lecture Notes in Computer Science 2747 , ACM. 2003.
93. F. Martins and A. Ravara, Controling migration in lsdpi.
    Technical report , Section of Computer Science, Department of Mathematics, Instituto Superior Técnico. 2002.
94. F. Martins and A. Ravara, Typing Migration Control in Lsdpi.
    In Proceedings of FCS'04, 31, Turku Centre for Computer Science. 2004.
95. F. Martins and A. Ravara, Typing migration control in lsdpi.
    Technical report , CLC, Department of Mathematics, Instituto Superior Técnico. 2003.
96. Marino Miculan and Kidane Yemane, A Unifying Model of Variables and Names.
    In Proceedings of FOSSACS'05, LNCS 3441, Springer. 2005.
97. Ugo Montanari, Web Services and Models of Computation.
    In First International Workshop on Web Services and Formal Methods, Electronic Notes in Computer Science 105, Elsevier. 2004.
98. L. Monteiro, A note on models for spatial logic based on transition systems with spatial structure.
    Technical Note, DI-FCT/UNL. 2003.
99. L. Monteiro, A note on a noninterleaving model of concurrency based on transition systems with spatial structure.
    Technical Note, DI-FCT/UNL. 2003.
100. L. Monteiro, Transition Systems with Spatial Structures: A Coalgebraic Framework.
     Manuscript. 2002.
101. Mogens Nielsen and Frank Valencia, Notes on Timed CCP.
     In 4th Advanced Course on Petri Nets ICPN'03, LNCS, Springer-Verlag. 2004.
102. D. Pous, GCPAN Implementation.
     http://perso.ens-lyon.fr/damien.pous/gcpan. 2004.
103. R. Raggi and E. Tuosto, HD-Reducer (Online version).
     Dipartimento di Informatica, Universita' di Pisa. 2002.
104. A. Ravara, A. G. Matos, V. T. Vasconcelos, and L. Lopes, Lexically scoped distribution: what you see is what you get.
     Electronic Notes in Theoretical Computer Science, 85(1). 2003. Presented at FGC'03.
105. A. Ravara, P. Resende, and V. Vasconcelos, An Algebra of Behavioural Types.
     Technical report , Section of Computer Science, Department of Mathematics, Instituto Superior Técnico. 2002.
106. A. Ravara, P. Resende, and V. Vasconcelos, An Algebra of Behavioural Types.
     Technical report , CLC, Department of Mathematics, Instituto Superior Técnico. 2003.
107. A. Ribeiro, L. Caires, and L. Monteiro, Verifying the Arrow Protocol in a Spatial Logic.
     Technical report TR-DI/FCT/UNL-04/2004, Departamento de Informatica, FCT/UNL. 2004.
108. C. Rueda and F. Valencia, Non-Viability Deductions in Arc-Consistency Computation.
     Technical report . 2003.
109. D. Sangiorgi, Types, or: Where's the difference between CCS and pi?.
     In Proc. CONCUR '02, LNCS 2421, Springer Verlag. 2002. Accompanying paper for an invited talk.
110. D. Teller, P. Zimmer, and D. Hirschkoff, Using Ambients to Control Resources.
     In Proceedings of the 13th Int. Conf. in Concurrency Theory (CONCUR'02), LNCS 2421, Springer Verlag. 2002.
111. D. Teller, P. Zimmer, and D. Hirschkoff, Using Ambients to Control Resources (long version).
     International Journal of Information Security, 2(3-4), pp 126-144. 2003.
112. David Teller, Formalisms for Mobile Resource Control.
     Electronic Notes in Theoretical Computer Science, 85(1). 2003. Presented at FGC'03.
113. D. Teller, Recovering resources in the pi-calculus.
     In Proceedings of IFIP TCS 2004, Kluwer. 2004.
114. D. Teller, Ressources limitées pour la mobilité: utilisation, réutilisation, garanties.
     PhD thesis, École doctorale MathIF, ENS Lyon. 2004.
115. E. Tuosto, B. Victor, and K. Yemane, Polyadic History-Dependent Automata for the Fusion Calculus.
     Technical report 2003-062, Department of Information Technology, Uppsala University. December 2003.
116. Emilio Tuosto and Hugo T. Vieira, An Observational Model for Spatial Logics.
     In First International Workshop on Views On Designing Complex Architectures, ENTCS , Elsevier. September 2004.
117. E. Tuosto, Non Functional Aspects of Wide area Network Programming.
     PhD thesis, Dipartimento di Informatica, Univ. Pisa. 2003.
118. Emilio Tuosto, Tarzan: Communicating and Moving in Wireless Jungles.
     In 2nd Workshop on Quantitative Aspects of Programming Languages, Electronic Notes in Computer Science 112, Elsevier. 2004.
119. F. Valencia, Concurrency, Time and Constraints.
     In Proceedings of the Nineteenth International Conference on Logic Programming (ICLP 2003), Lecture Notes in Computer Science , Springer Verlag. 2003.
120. F. Valencia, On the Decidability of Timed CCP.
     Technical report . December 2003.
121. F. Valencia, Timed Concurrent Constraint Programming: Decidability Results and their Application to LTL.
     In Proceedings of the Nineteenth International Conference on Logic Programming (ICLP 2003), LNCS, Springer-Verlag. 2003.
122. A. Vallecillo, V. T. Vasconcelos, and A. Ravara, Typing the Behavior of Objects and Components using Session Types.
     In Electronic Notes in Theoretical Computer Science, 68, Elsevier Science Publishers. 2002. Presented at FOCLASA'02 - 1st International Workshop on Foundations of Coordination Languages and Software Architectures.
123. Antonio Vallecillo, Vasco T. Vasconcelos, and Ant\'onio Ravara, Typing the Behavior of Software Components using Session Types.
     Technical report . December 2004. Revised and extended version of Typing the Behavior of Objects and Components using Session Types. In Foclasa 2002, 1st International Workshop on Foundations of Coordination Languages and Software Architectures. Electronic Notes in Theoretical Computer Science, 68(3), 2002.
124. V. Vanackere, History-Dependent Scheduling for Cryptographic Processes.
     In Proc. VMCAI 2004, Lecture Notes in Computer Science 2937, Springer Verlag. 2004.
125. V. Vanackère, The TRUST protocol analyser, Automatic and efficient verification of cryptographic protocols.
     In Verification Workshop - Verify02. 2002.
126. V. Vanackère, The TRUST protocol analyser.
     Lab. Informatique de Marseille. 2002.
127. Vincent Vanackere, TRUST: un systeme de verification automatique de protocole cryptographique.
     PhD thesis, Université de Provence. 2005.
128. Vasco T. Vasconcelos, Ant\'onio Ravara, and Simon Gay, Session types for functional multithreading.
     In CONCUR'04, Lecture Notes in Computer Science 3170, Springer Verlag. 2004.
129. H. Vieira and L. Caires, Spatial Model Checker User's Manual.
     Technical report , Departamento de Informatica, FCT/UNL. 2003.

Year 4 (Jan-Apr 2005)

The list below is also available in BibTeX format.

1. Michael Baldamus, Joachim Parrow, and Björn Victor, A Fully Abstract Encoding of the pi-Calculus with Data Terms.
   In Proceedings of ICALP'05, LNCS , Springer. 2005.
2. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Enforcing Secure Service Composition.
   In IEEE Computer Security Foundation Workshop, to appear. 2005.
3. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, History-based Access Control with Local Policies.
   In FOSSACS 2005, Lectures Notes in Computer Science 3441, Springer. 2005.
4. L. Caires and E. Lozes, Elimination of quantifiers and undecidability in spatial logics for concurrency.
   Theor. Comput. Sci.. 2005. Accepted for publication.
5. S. Dantchev and F.D. Valencia, On infinite CSP's.
   In Proc. Third International CP'05 Workshop on Modelling and Reformulating CSP's. 2005.
6. Y. Deng and D. Sangiorgi, Ensuring termination by typability.
   Submitted. 2005.
7. Rocco DeNicola, Gianluigi Ferrari, Ugo Montanari, Rosario Pugliese, and Emilio Tuosto, A Process Calculus for QoS-Aware Applications.
   In Coordination 2005, Lectures Notes in Computer Science 3454, Springer. 2005.
8. Gianluigi Ferrari, Ugo Montanari, Emilio Tuosto, Björn Victor, and Kidane Yemane, Modelling Fusion calculus using HD-automata.
   In To appear in In First Conference on Algebra and Coalgebra in Computer Science CALCO'05, LNCS , Springer. 2005.
9. Alberto Lluch-Lafuente and Ugo Montanari, Quantitative mu-calculus and CTL defined over constraint semirings.
   In QAPL (2005), Electronic Notes in Computer Science , Elsevier. 2005.
10. Marino Miculan and Kidane Yemane, A Unifying Model of Variables and Names.
    In Proceedings of FoSSaCS 2005, Lecture Notes in Computer Science , Springer Verlag. April 2005.

Year 3 (2004)

The list below is also available in BibTeX format.

1. Roberto M. Amadio and Silvano Dal Zilio, Resource Control for Synchronous Cooperative Threads.
   In CONCUR 2004 - 15th International Conference on Concurrency Theory, Lecture Notes in Computer Science 3170, Springer-Verlag. August 2004.
2. Michael Baldamus, Jesper Bengtson, Gianluigi Ferrari, and Roberto Raggi, Web Services as a New Approach to Distributing and Coordinating Semantics-Based Verification Toolkits.
   In Proceedings of the First International Workshop on Web Services and Formal Methods (WSFM 2004), ENTCS 105, Elsevier. February 2004.
3. Michael Baldamus, Joachim Parrow, and Björn Victor, Spi Calculus Translated to pi-Calculus Preserving May-Tests.
   In Proceedings of LICS'04, Computer Society Press. July 2004.
4. Giacomo Baldi, Andrea Bracciali, Gianluigi Ferrari, and Emilio Tuosto, A Coordination-based Methodology for Security Protocol Verification.
   In WISP'04, ENCTS 121, Elsevier. 2005.
5. G. Barthe, A. Basu, and T. Rezk, Security Types Preserving Compilation.
   Journal of Computer Languages, Systems and Structures. 2005. To appear.
6. G. Barthe, P. D'Argenio, and T. Rezk, Secure Information Flow by Self-Composition.
   In Proceedings of CSFW'04, IEEE Press. 2004.
7. G. Barthe and L. Prensa-Nieto, Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems.
   In Proceedings of FMSE'04, ACM Press. 2004.
8. G. Barthe and T. Rezk, Non-interference for a JVM-like language.
   In Proceedings of TLDI'05, ACM Press. 2005.
9. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Method Inlining in Presence of Stack Inspection.
   In Workshop on Issues in the Theory of Security (WITS'04). 2004.
10. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Policy Framings for Access Control.
    In Workshop on Issues in the Theory of Security (WITS'05). 2005.
11. Massimo Bartoletti, Pierpaolo Degano, and Gianluigi Ferrari, Program Transformations under Dynamic Security Policies.
    In MEPHISTO Final Workshop, Electronic Notes in Computer Science 99, Elsevier. 2004.
12. Jesper Bengtsson, http://www.it.uu.se/research/reports/2004-041">Generic Implementations of Process Calculi in Isabelle.
    In Proceedings of the 16th Nordic Workshop on Programming Theory, IT Technical Reports . October 2004.
13. Michele Boreale, Marzia Buscemi, and Ugo Montanari, A general name binding mechanism.
    Submitted for publication. 2005.
14. Michele Boreale and Marzia Buscemi, A Framework for the Analysis of Security Protocols.
    Theoretical Computer Science. 2005. To appear.
15. Marzia Buscemi and Ugo Montanari, A Compositional Coalgebraic Model of Monadic Fusion Calculus.
    Submitted for publication. 2005.
16. Marzia Buscemi and Ugo Montanari, A congruence result for process calculi with structural axioms.
    Submitted for publication. 2005.
17. Palamidessi C., Saraswat V., F. Valencia, and B. Victor, Linearity vs Persistency in the Pi-Calculus.
    Ongoing Work.
18. L. Caires and L. Cardelli, A spatial logic for concurrency-II.
    Theor. Comput. Sci., 322(3), pp 517--565. 2004.
19. Luis Caires and Etienne Lozes, Elimination of Quantifiers and Undecidability in Spatial Logics for Concurrency.
    Theoretical Computer Science. To appear.
20. L. Caires and E. Lozes, Elimination of quantifiers and undecidability in spatial logics for concurrency.
    In Proc. of CONCUR'04, Lecture Notes in Computer Science , Springer Verlag. 2004.
21. L. Caires, Behavioral and Spatial Properties in a Logic for the Pi-Calculus.
    In Proc. of Foundations of Software Science and Computation Structures'2004, Lecture Notes in Computer Science , Springer Verlag. 2004.
22. S. Dantchev and F. Valencia, On Infinite CSP's.
    In In proceedings of the Third International Workshop on Modelling and Reformulating CSPs. 2004.
23. Yuxin Deng and Catuscia Palamidessi, Axiomatizations for probabilistic finite-state behaviors.
    In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science , Springer. 2005. To appear.
24. Yuxin Deng and Catuscia Palamidessi, Axiomatizations for probabilistic finite-state behaviors.
    In Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science , Springer. 2005. To appear.
25. Yuxin Deng and Davide Sangiorgi, Ensuring termination by typability.
    In Proceedings of the 3rd IFIP International Conference on Theoretical Computer Science, Kluwer. 2004.
26. Yuxin Deng and Davide Sangiorgi, Towards an algebraic theory of typed mobile processes.
    In Proceedings of the 31th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 3142, Springer. 2004.
27. Yuxin Deng and Davide Sangiorgi, Towards an algebraic theory of typed mobile processes.
    Theoretical Computer Science. 2005. To appear.
28. Gianluigi Ferrari and Alberto Lluch-Lafuente, A Logic for Graphs with QoS.
    In First International Workshop on Views On Designing Complex Architectures, Electronic Notes in Computer Science , Elsevier. September 2004. To appear.
29. Gianluigi Ferrari, Ugo Montanari, and Emilio Tuosto, Model Checking for Nominal Calculi.
    In FOSSACS, LNCS , Springer. 2005. To appear.
30. Gianluigi Ferrari, Ugo Montanari, and Emilio Tuosto, Verification on the WEB of Name-Passing Process Calculi.
    In Workshop on Software Engineering Tools: Compatibility and Integration, Monterey Workshop Series, LNCS . 2004. To appear.
31. Fabio Gadducci, Marino Miculan, and Ugo Montari, About permutation algebras, (pre)sheaves and named sets.
    Submitted for publication, International Journal on Higher-Order and Symbolic Computation. 2004.
32. Neil Ghani, Kidane Yemane, and Björn Victor, Relationally Staged Computations in Calculi of Mobile Processes.
    In Proceedings of CMCS 2004 (7th International Workshop on Coalgebraic Methods in Computer Science), ENTCS 106, Elsevier. 2004.
33. D. Hirschkoff, D. Pous, and D. Sangiorgi, An Efficient Abstract Machine for Safe Ambients.
    In Proc. of COORDINATION '05. 2005. To appear.
34. D. Hirschkoff, An Extensional Spatial Logic for Mobile Processes.
    In Proc. of CONCUR'04, 3170, Springer Verlag. 2004.
35. E. Lozes, Expressivité des logiques d'espaces.
    PhD thesis, École Doctorale MathInf, ENS Lyon. 2004.
36. E. Lozes, Separation logic preserves the expressive power of classical logic.
    In Proc. Workshop Space'04. 2004. Electronic publication.
37. F. Martins and A. Ravara, Typing Migration Control in Lsdpi.
    In Proceedings of FCS'04, 31, Turku Centre for Computer Science. 2004.
38. Marino Miculan and Kidane Yemane, A Unifying Model of Variables and Names.
    In Proceedings of FOSSACS'05, LNCS , Springer. 2005. To appear.
39. Ugo Montanari, Web Services and Models of Computation.
    In First International Workshop on Web Services and Formal Methods, Electronic Notes in Computer Science 105, Elsevier. 2004.
40. D. Pous, GCPAN Implementation.
    http://perso.ens-lyon.fr/damien.pous/gcpan. 2004.
41. A. Ribeiro, L. Caires, and L. Monteiro, Verifying the Arrow Protocol in a Spatial Logic.
    Technical report TR-DI/FCT/UNL-04/2004, Departamento de Informatica, FCT/UNL. 2004.
42. D. Teller, Recovering resources in the pi-calculus.
    In Proceedings of IFIP TCS 2004, Kluwer. 2004.
43. D. Teller, Ressources limitées pour la mobilité: utilisation, réutilisation, garanties.
    PhD thesis, École doctorale MathIF, ENS Lyon. 2004.
44. Emilio Tuosto and Hugo T. Vieira, An Observational Model for Spatial Logics.
    In First International Workshop on Views On Designing Complex Architectures, ENTCS , Elsevier. September 2004. To appear.
45. Emilio Tuosto, Tarzan: Communicating and Moving in Wireless Jungles.
    In 2nd Workshop on Quantitative Aspects of Programming Languages, Electronic Notes in Computer Science 112, Elsevier. 2004.
46. Antonio Vallecillo, Vasco T. Vasconcelos, and Ant\'onio Ravara, Typing the Behavior of Software Components using Session Types.
    Technical report . December 2004. Revised and extended version of Typing the Behavior of Objects and Components using Session Types. In Foclasa 2002, 1st International Workshop on Foundations of Coordination Languages and Software Architectures. Electronic Notes in Theoretical Computer Science, 68(3), 2002.
47. Vincent Vanackere, TRUST: un systeme de verification automatique de protocole cryptographique.
    PhD thesis, Université de Provence. 2005.
48. Vasco T. Vasconcelos, Ant\'onio Ravara, and Simon Gay, Session types for functional multithreading.
    In CONCUR'04, Lecture Notes in Computer Science 3170, Springer Verlag. 2004.
49. S. Dal Zilio, D. Lugiez, and C. Meyssonnier, A Logic you Can Count On.
    In POPL 2004 - 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press. 2004.

Year 2 (2003)

The list below is also available in BibTeX format.

1. M. Baldamus, J. Bengtson, G. Ferrari, and R. Raggi, Web-Services as a New Approach to Distributing and Coordinating Semantics-Based Verification Toolkits.
   In Web Services and Formal Methods. 2004. WS-FM workshop proceedings, to appear.
2. M. Baldamus, R. Mayr, and G. Schneider, A Backward/Forward Strategy for Verifying Safety Properties of Infinite-State Systems.
   Technical report 2003-065, Department of Information Technology, Uppsala University, Sweden. 2003.
3. M. Baldamus, J. Parrow, and B. Victor, Spi Calculus Translated to \largepi-Calculus Preserving May Testing.
   Technical report 2003-063, Department of Information Technology, Uppsala University, Sweden. 2003.
4. M. Baldamus, A Fully-Abstract Model for the Fusion Calculus.
   Preliminary Draft. 2003.
5. G. Baldi, A. Bracciali, G. Ferrari, and E. Tuosto, ASPASyA: an Automated Tool for Security Protocol Analysis based on a Symbolic Approach.
   Submitted for publication. 2003.
6. G. Barthe, A. Basu, and T. Rezk, Security Types Preserving Compilation.
   In Proc. of VMCAI'04, LNCS , Springer {V}erlag. 2004. to appear.
7. G. Barthe and L. Prensa Nieto, Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems.
   manuscript.
8. G. Barthe and T. Rezk, Secure Information Flow for the JVM.
   manuscript.
9. M. Bartoletti, P. Degano, and G. Ferrari, Stack Inspection and Secure Program Transformations.
   International Journal of Information Security. 2003. To appear.
10. L.Bettini, V.Bono, R.De Nicola, G.Ferrari, D.Gorla, M.Loreti, E.Moggi, R.Pugliese, E.Tuosto, and B.Venneri, The KLAIM Project: Theory and Practice.
    In Global Computing: Programming Environments, Languages, Security and Analysis of Systems, LNCS . 2003.
11. M. Boreale, M. Buscemi, and U. Montanari, The Distinctive Fusion Calculus.
    Unpublished draft. 2003.
12. M. Boreale and M. Buscemi, Symbolic Analysis of Crypto-Protocols based on Modular Exponentiation.
    In Proc. of MFCS 2003, Lecture Notes in Computer Science 2747 , Springer-Verlag. 2003. An extended version appears in Proc. of FCS'03.
13. M. Buscemi and U. Montanari, A Compositional Coalgebraic Model of Explicit Fusions.
    Unpublished draft. 2003.
14. M. Buscemi, Models and Security Verification of Mobile Systems.
    PhD thesis, Dipartimento di Matematica, University of Neaples ``Federico II''. 2003.
15. L. Caires and L. Cardelli, A Spatial Logic for Concurrency (Part I).
    Information and Computation, 186(2), pp 194--235. 2003.
16. L. Caires and L. Cardelli, A Spatial Logic for Concurrency (Part II).
    Theoretical Computer Science. to appear.
17. L. Caires, Behavioral and Spatial Properties in a Logic for the Pi-Calculus.
    In Proc. of Foundations of Software Science and Computation Structures'2004, Lecture Notes in Computer Science , Springer Verlag. 2003.
18. Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, and Jean-Marc Talbot, Model Checking Mobile Ambients.
    Theoretical Computer Science, 308(1), pp 277--331. November 2003.
19. Silvano Dal Zilio and Denis Lugiez, A Logic you Can Count On.
    In POPL 2004 - 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2004.
20. Silvano Dal Zilio and Denis Lugiez, XML Schema, Tree Logic and Sheaves Automata.
    In RTA 2003 - 14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 2706, Springer. June 2003.
21. M. Miculan F. Gadducci and U. Montanari, Some Characterization Results for Permutation Algebras.
    In Workshop COMETA, ENTCS , Elsevier. 2003. to appear.
22. G. Ferrari, S. Gnesi, U. Montanari, and M. Pistore, A model checking verification environment for mobile processes.
    ACM Transactions on Software Engineering and Methodologies (TOSEM), To appear. 2004.
23. G. Ferrari, S. Gnesi, U. Montanari, R. Raggi, G. Trentanni, and E. Tuosto., Verification on the Web of Mobile Processes.
    Submitted for publication. 2003.
24. G. Ferrari, U. Montanari, and E. Tuosto, Co-algebraic Minimization of HD-automa in a polymorphic lambda-calculus.
    Under Revision for Theoretical Computer Science. 2003.
25. G. Ferrari, U. Montanari, R. Raggi, and E. Tuosto, From Co-algebraic Specifications to Implementation: The MIHDA toolkit.
    In First International Symposium on Formal Methods for Components and Objects (FMCO), Springer Lecture Notes in Computer Science , Springer. 2003.
26. G. Ferrari, U. Montanari, E. Tuosto, B. Victor, and K. Yemane, Modelling and Minimising the Fusion Calculus using HD-automata.
    Technical report, University of Pisa. 2003.
27. Simon Gay, Vasco T. Vasconcelos, and Ant\'onio Ravara, Session Types for Inter-Process Communication.
    Technical report 2003--133, Department of Computing, University of Glasgow. March 2003.
28. P. Giambiagi, G. Schneider, and F. Valencia, On the Expressiveness of CCS-like Calculi.
    In In Proceedings of FOSSACS'04, LNCS, Springer-Verlag. 2004.
29. D. Hirschkoff, E. Lozes, and D. Sangiorgi, Minimality Results for the Spatial Logics.
    In Proc. of FSTTCS'2003, LNCS , Springer Verlag. 2003.
30. I. Lanese and U. Montanari, Mapping Fusion and Synchronized Hyper-edge Replacement into Logic Programming.
    Under Revision for Theory and Practice of Logic Programming. 2003.
31. E. Lozes, Adjunct elimination in the static Ambient Logic.
    In Proc. of EXPRESS'2003. 2003. to appear in ENTCS, Elsevier.
32. I. Scagnetto M. Miculan, A Framework for Typed HOAS and Semantics.
    In Proc. of PPDP 2003, Uppsala, Lecture Notes in Computer Science 2747 , ACM. 2003.
33. F. Martins and A. Ravara, Typing migration control in lsdpi.
    Technical report , CLC, Department of Mathematics, Instituto Superior Técnico. 2003. Submitted for publication.
34. L. Monteiro, A note on models for spatial logic based on transition systems with spatial structure.
    Technical Note, DI-FCT/UNL. 2003.
35. L. Monteiro, A note on a noninterleaving model of concurrency based on transition systems with spatial structure.
    Technical Note, DI-FCT/UNL. 2003.
36. Mogens Nielsen and Frank Valencia, Notes on Timed CCP.
    In 4th Advanced Course on Petri Nets ICPN'03, LNCS, Springer-Verlag. 2004.
37. A. Ravara, A. G. Matos, V. T. Vasconcelos, and L. Lopes, Lexically scoped distribution: what you see is what you get.
    Electronic Notes in Theoretical Computer Science, 85(1). 2003. Presented at FGC'03.
38. A. Ravara, P. Resende, and V. Vasconcelos, An Algebra of Behavioural Types.
    Technical report , CLC, Department of Mathematics, Instituto Superior Técnico. 2003. Submitted for publication.
39. A. Ribeiro, L. Caires, and L. Monteiro, Verifying the Arrow Protocol in a Spatial Logic.
    Technical report , Departamento de Informatica, FCT/UNL. 2003.
40. C. Rueda and F. Valencia, Non-Viability Deductions in Arc-Consistency Computation.
    Technical report , . 2003. WP1, Submitted for conference publication.
41. D. Teller, P. Zimmer, and D. Hirschkoff, Using Ambients to Control Resources (long version).
    International Journal of Information Security. 2003. to appear.
42. David Teller, Formalisms for Mobile Resource Control.
    Electronic Notes in Theoretical Computer Science, 85(1). 2003. Presented at FGC'03.
43. E. Tuosto, B. Victor, and K. Yemane, Polyadic History-Dependent Automata for the Fusion Calculus.
    Technical report 2003-062, Department of Information Technology, Uppsala University. December 2003.
44. E. Tuosto, Non Functional Aspects of Wide area Network Programming.
    PhD thesis, Dipartimento di Informatica, Univ. Pisa. 2003.
45. F. Valencia, Concurrency, Time and Constraints.
    In Proceedings of the Nineteenth International Conference on Logic Programming (ICLP 2003), LNCS, Springer-Verlag. 2003. WP2, Invited publication.
46. F. Valencia, On the Decidability of Timed CCP.
    Technical report , . Dec 2003. WP2, Submitted to the Journal of Theoretical Computer Science.
47. F. Valencia, Timed Concurrent Constraint Programming: Decidability Results and their Application to LTL.
    In Proceedings of the Nineteenth International Conference on Logic Programming (ICLP 2003), LNCS, Springer-Verlag. 2003.
48. A. Vallecillo, V. T. Vasconcelos, and A. Ravara, Typing the Behavior of Objects and Components using Session Types.
    Electronic Notes in Theoretical Computer Science, 68(3). 2003. Presented at FOCLASA'02.
49. V. Vanackere, History-Dependent Scheduling for Cryptographic Processes.
    In Proc. VMCAI 2004, Springer Lecture Notes in Computer Science , Springer. 2004. to appear.
50. H. Vieira and L. Caires, Spatial Model Checker User's Manual.
    Technical report , Departamento de Informatica, FCT/UNL. 2003.

Year 1 (2002)

The list below is also available in BibTeX format.

1. R. Amadio and W. Charatonik, On name generation and set-based analysis in Dolev-Yao model (Extended Abstract).
   In Proc. CONCUR'02, LNCS 2421, Springer Verlag. 2002.
2. R. Amadio, D. Lugiez, and V. Vanackere, On the symbolic reduction of processes with cryptographic functions.
   Theoretical Computer Science. To appear.
3. R. Amadio and C. Meyssonnier, On decidability of the control reachability problem in the asynchronous pi-calculus.
   Nordic Journal of Computing, 9(2), pp 70-101. 2002.
4. Roberto M. Amadio, Gérard Boudol, and Cédric Lhoussaine, On message deliverability and non-uniform receptivity.
   Technical report 05-2002, LIF. May 2002. Accepted for pubblication in Fundamenta Informaticae.
5. M. Boreale and M. Buscemi, A Framework for the Analysis of Security Protocols.
   In Proc. CONCUR'02, LNCS 2421, Springer Verlag. 2002.
6. M. Boreale and M. Buscemi, STA, a Tool for the Analysis of Cryptographic Protocols (Online version).
   Dipartimento di Sistemi ed Informatica, Università di Firenze, and Dipartimento di Informatica, Università di Pisa,. 2002.
7. A. Bracciali, A. Brogi, G. Ferrari, and E. Tuosto, Security and dynamic composition of open systems.
   In Proc. Int. Conference on Parallel and Distributed Techniques and applications, CSREA Press. 2002.
8. M. Buscemi and U. Montanari, A First Order Coalgebraic Model of Pi-Calculus Early Observational Equivalence.
   In Proc. CONCUR'02, LNCS 2421, Springer Verlag. 2002. Full version in Technical Report TR-02-14, Dipartimento di Informatica, Universitá di Pisa, August 2002.
9. L. Caires and L. Cardelli., A Spatial Logic for Concurrency (Part I).
   Information and Computation. 2002. Accepted for publication.
10. L. Caires and L. Cardelli, A Spatial Logic for Concurrency (Part II).
    In CONCUR 2002: Concurrency Theory (13th International Conference), Lecture Notes in Computer Science. Springer-Verlag. 2002. Also as Technical Report 3/2002/DI/PLM/FCTUNL.
11. L. Caires, Model-Checking of Spatial Properties in the pi-calculus.
    Research report 3, DI/FCT/UNL. December 2002.
12. G. Ferrari, S. Gnesi, U. Montanari, and M. Pistore, A Model Checking Verification Environment for Mobile Processes.
    Submitted to ACM TOSEM (under revision). 2002.
13. G. Ferrari, S. Gnesi, U. Montanari, R. Raggi, G. Trentanni, and E. Tuosto, Verification on the Web.
    Technical report TR-02-18, Dipartimento di Informatica, Università di Pisa. 2002.
14. G. Ferrari, E. Moggi, and R. Pugliese, Guardians for Ambient Based Monitoring.
    In Proc. Foundations of Wide Area Network Programming, ENTCS , Elseviers. 2002.
15. G. Ferrari, E. Moggi, and R. Pugliese, MetaKlaim: A type safe multi-stage language for Global computing.
    Technical report Under revision for Mathematical Structures in Computer Science, . 2002.
16. G. Ferrari, U. Montanari, R. Raggi, and E. Tuosto, From Coalgebraic Specification to Toolkit Development.
    Technical report TR-02-19, Technical Report, Dipartimento di Informatica Universita' di Pisa. 2002.
17. G. Ferrari, U. Montanari, and M. Pistore., Minimizing Transition Systems for Name-passing Calculi: A Co-algbraic Formulation.
    In Proc. FOSSACS'02, LNCS 2303, Springer Verlag. 2002.
18. S. Gay, V. T. Vasconcelos, and A. Ravara, Session types for inter-process communication.
    Technical report , Department of Computer Science, University of Lisbon. 2002. Submitted for publication.
19. P. Giannini, D. Sangiorgi, and A. Valente, A distributed abstract machine for Safe Ambients.
    Extended and refined version of a paper appeared in Icalp.01. 2002.
20. D. Hirschkoff, E. Lozes, and D. Sangiorgi, Separability, Expressiveness and Decidability in the Ambient Logic.
    In Proc. of LICS'02. 2002.
21. F. Levi and D. Sangiorgi, Mobile Safe Ambients.
    To appear in the TOPLAS journal. Extended and refined version of a paper appeared in Proc. 27th POPL, ACM Press. 2002.
22. Denis Lugiez and Silvano Dal Zilio, Multitrees Automata, Presburger's Constraints and Tree Logics.
    Technical report 08-2002, LIF. June 2002.
23. Denis Lugiez and Silvano Dal Zilio, XML Schema, Tree Logic and Sheaves Automata.
    Technical report 4631, INRIA. November 2002.
24. F. Martins and A. Ravara, Controling migration in lsdpi.
    Technical report , Section of Computer Science, Department of Mathematics, Instituto Superior Técnico. 2002. In preparation.
25. L. Monteiro, Transition Systems with Spatial Structures: A Coalgebraic Framework.
    Manuscript. 2002.
26. R. Raggi and E. Tuosto, HD-Reducer (Online version).
    Dipartimento di Informatica, Universita' di Pisa. 2002.
27. A. Ravara, P. Resende, and V. Vasconcelos, An Algebra of Behavioural Types.
    Technical report , Section of Computer Science, Department of Mathematics, Instituto Superior Técnico. 2002. Submitted for publication.
28. D. Sangiorgi, Types, or: Where's the difference between CCS and pi?.
    In Proc. CONCUR '02, LNCS 2421, Springer Verlag. 2002. accompanying paper for an invited talk.
29. D. Teller, P. Zimmer, and D. Hirschkoff, Using Ambients to Control Resources.
    In Proceedings of the 13th Int. Conf. in Concurrency Theory (CONCUR'02), LNCS 2421, Springer Verlag. 2002.
30. A. Vallecillo, V. T. Vasconcelos, and A. Ravara, Typing the Behavior of Objects and Components using Session Types.
    In Electronic Notes in Theoretical Computer Science, 68, Elsevier Science Publishers. 2002. presented at FOCLASA'02 - 1st International Workshop on Foundations of Coordination Languages and Software Architectures.
31. V. Vanackère, The TRUST protocol analyser, Automatic and efficient verification of cryptographic protocols.
    In Verification Workshop - Verify02. 2002.
32. V. Vanackère, The TRUST protocol analyser.
    Lab. Informatique de Marseille. 2002.

Web page: Björn Victor, latest update Wed, 29-Jun-2005 12:49 MEST