%%% Please DO NOT EDIT this file - it was automatically generated.
%%% Publications of the PROFUNDIS project, EU FET-GC contract IST-2001-33100
%%%
%%% ====================================================================
%%%  BibTeX-file{
%%%     author          = "Bj{\"o}rn Victor",
%%%     date            = "18 Feb 2004",
%%%     filename        = "profundis-year2-bib.bib",
%%%     url             = "http://www.it.uu.se/profundis/profundis-year2-bib.bib",
%%%     www-home        = "http://www.it.uu.se/profundis/",
%%%     address         = "Department of Information Technology,
%%%                        Uppsala University,
%%%                        Box 337,
%%%                        SE-751 05 Uppsala, SWEDEN",
%%%     telephone       = "+46 18 471 0000",
%%%     FAX             = "+46 18 511925",
%%%     email           = "Bjorn.Victor at it.uu.se",
%%%     dates           = {2002--},
%%%     keywords        = "",
%%%     supported       = "yes",
%%%     supported-by    = "Bj{\"o}rn Victor",
%%%     abstract        = "Publications of the PROFUNDIS project,
%%%			   EU FET-GC contract IST-2001-33100"
%%%  }
%%% ====================================================================


@InProceedings{	  baldamus.m.bengtson.j.ea:web-services,
  note		= {WS-FM workshop proceedings, to appear},
  year		= {2004},
  author	= {Baldamus, M. and Bengtson, J. and Ferrari, G. and Raggi,
		  R.},
  title		= {Web-Services as a New Approach to Distributing and
		  Coordinating Semantics-Based Verification Toolkits},
  booktitle	= {Web Services and Formal Methods}
}

@TechReport{	  baldamus.m.mayr.r.ea:backwardforward,
  title		= {A Backward/Forward Strategy for Verifying Safety
		  Properties of Infinite-State Systems},
  institution	= {Department of Information Technology, Uppsala University,
		  Sweden},
  number	= {2003-065},
  author	= {Baldamus, M. and Mayr, R. and Schneider, G.},
  year		= {2003}
}

@TechReport{	  baldamus.m.parrow.j.ea:spi,
  institution	= {Department of Information Technology, Uppsala University,
		  Sweden},
  number	= {2003-063},
  title		= {Spi Calculus Translated to {\large$\pi$}-Calculus
		  Preserving May Testing},
  year		= {2003},
  author	= {Baldamus, M. and Parrow, J. and Victor, B.}
}

@Unpublished{	  baldamus.m:fully-abstract,
  author	= {Baldamus, M.},
  note		= {Preliminary Draft},
  year		= {2003},
  title		= {A Fully-Abstract Model for the Fusion Calculus}
}

@Unpublished{	  baldi.g.bracciali.a.ea:aspasya,
  note		= {Submitted for publication},
  year		= {2003},
  title		= {{ASPASyA}: an Automated Tool for Security Protocol
		  Analysis based on a Symbolic Approach},
  author	= {G. Baldi and A. Bracciali and G. Ferrari and E. Tuosto}
}

@InProceedings{	  barthe.g.basu.a.ea:security,
  note		= {to appear},
  series	= {LNCS},
  booktitle	= {Proc. of {VMCAI}'04},
  year		= 2004,
  publisher	= {Springer {V}erlag},
  title		= {Security {T}ypes {P}reserving {C}ompilation},
  author	= {G. Barthe and A. Basu and T. Rezk}
}

@Unpublished{	  barthe.g.prensa-nieto.l:formally,
  title		= {Formally {V}erifying {I}nformation {F}low {T}ype {S}ystems
		  for {C}oncurrent and {T}hread {S}ystems},
  author	= {G. Barthe and L. {Prensa Nieto}},
  note		= {manuscript}
}

@Unpublished{	  barthe.g.rezk.t:secure,
  author	= {G. Barthe and T. Rezk},
  note		= {manuscript},
  title		= {Secure {I}nformation {F}low for the {JVM}}
}

@Article{	  bartoletti.m.degano.p.ea:stack,
  note		= {To appear},
  title		= {Stack {I}nspection and {S}ecure {P}rogram
		  {T}ransformations},
  journal	= {International Journal of Information Security},
  year		= 2003,
  author	= {M. Bartoletti and P. Degano and G. Ferrari}
}

@InProceedings{	  bettini.l.bono.v.ea:klaim,
  author	= {L.Bettini and V.Bono and R.De Nicola and G.Ferrari and
		  D.Gorla and M.Loreti and E.Moggi and R.Pugliese and
		  E.Tuosto and B.Venneri},
  booktitle	= {Global Computing: Programming Environments, Languages,
		  Security and Analysis of Systems},
  number	= {2874},
  publishsw	= {Springer-Verlag},
  title		= {The KLAIM Project: Theory and Practice},
  series	= {LNCS},
  editor	= {C.Priami},
  year		= 2003
}

@Unpublished{	  boreale.m.buscemi.m.ea:distinctive,
  title		= {The Distinctive Fusion Calculus},
  author	= {M. Boreale and M. Buscemi and U. Montanari},
  note		= {Unpublished draft},
  year		= {2003}
}

@InProceedings{	  boreale.m.buscemi.m:symbolic,
  series	= {Lecture Notes in Computer Science 2747},
  publisher	= {Springer-Verlag},
  note		= {An extended version appears in Proc. of FCS'03},
  year		= 2003,
  author	= {M. Boreale and M. Buscemi},
  booktitle	= {Proc. of MFCS 2003},
  title		= {Symbolic Analysis of Crypto-Protocols based on Modular
		  Exponentiation}
}

@Unpublished{	  buscemi.m.montanari.u:compositional,
  year		= {2003},
  author	= {M. Buscemi and U. Montanari},
  title		= {A Compositional Coalgebraic Model of Explicit Fusions},
  note		= {Unpublished draft}
}

@PhDThesis{	  buscemi.m:models,
  school	= {Dipartimento di Matematica, University of Neaples
		  ``Federico II''},
  title		= {Models and Security Verification of Mobile Systems},
  year		= {2003},
  author	= {M. Buscemi}
}

@Article{	  caires.l.cardelli.l:spatial,
  volume	= 186,
  year		= {2003},
  title		= {A Spatial Logic for Concurrency ({P}art I)},
  number	= 2,
  journal	= {Information and Computation},
  author	= {L. Caires and L. Cardelli},
  pages		= {194--235}
}

@Article{	  caires.l.cardelli.l:spatial*1,
  title		= {A Spatial Logic for Concurrency ({P}art II)},
  journal	= {Theoretical Computer Science},
  year		= {to appear},
  author	= {L. Caires and L. Cardelli}
}

@InProceedings{	  caires.l:behavioral,
  year		= 2003,
  title		= {Behavioral and Spatial Properties in a Logic for the
		  Pi-Calculus},
  editor	= {Igor Walukiwicz},
  booktitle	= {Proc. of Foundations of Software Science and Computation
		  Structures'2004},
  author	= {L. Caires},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer Verlag}
}

@Article{	  charatonik.w.dal-zilio.s.ea:model,
  title		= {Model Checking Mobile Ambients},
  number	= 1,
  month		= nov,
  pages		= {277--331},
  author	= {Charatonik, Witold and {Dal Zilio}, Silvano and Gordon,
		  Andrew D. and Mukhopadhyay, Supratik and Talbot,
		  Jean-Marc},
  journal	= {Theoretical Computer Science},
  volume	= 308,
  year		= 2003
}

@InProceedings{	  dal-zilio.s.lugiez.d:logic,
  author	= {{Dal Zilio}, Silvano and Lugiez, Denis},
  booktitle	= {{POPL}~2004 -- 31st Annual ACM SIGPLAN-SIGACT Symposium on
		  Principles of Programming Languages},
  title		= {A Logic you Can Count On},
  year		= 2004
}

@InProceedings{	  dal-zilio.s.lugiez.d:xml,
  year		= 2003,
  title		= {{XML} Schema, Tree Logic and Sheaves Automata},
  url		= {http://www.cmi.univ-mrs.fr/~dalzilio/Papers/sheaves-xml.pdf}
		  ,
  month		= jun,
  booktitle	= {{RTA}~2003 -- 14th International Conference on Rewriting
		  Techniques and Applications},
  author	= {{Dal Zilio}, Silvano and Lugiez, Denis},
  pages		= {246--263},
  volume	= 2706,
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer}
}

@InProceedings{	  f-gadducci.mm.montanari.u:some,
  note		= {to appear},
  series	= {ENTCS},
  publisher	= {Elsevier},
  year		= 2003,
  title		= {Some Characterization Results for Permutation Algebras},
  booktitle	= {Workshop COMETA},
  author	= {F. Gadducci, M. Miculan and U. Montanari}
}

@Article{	  ferrari.g.gnesi.s.ea:model,
  year		= {2004},
  author	= {G. Ferrari and S. Gnesi and U. Montanari and M. Pistore},
  volume	= {To appear},
  title		= {A model checking verification environment for mobile
		  processes},
  journal	= {ACM Transactions on Software Engineering and Methodologies
		  (TOSEM)}
}

@Unpublished{	  ferrari.g.gnesi.s.ea:verification,
  title		= {Verification on the Web of Mobile Processes},
  year		= {2003},
  author	= {G.~Ferrari and S.~Gnesi and U.~Montanari and R.~Raggi and
		  G.~Trentanni and E.~Tuosto.},
  note		= {Submitted for publication}
}

@Unpublished{	  ferrari.g.montanari.u.ea:co-algebraic,
  author	= {G. Ferrari and U. Montanari and E. Tuosto},
  note		= {Under Revision for Theoretical Computer Science},
  year		= {2003},
  title		= {Co-algebraic Minimization of HD-automa in a polymorphic
		  $\lambda$-calculus.}
}

@InProceedings{	  ferrari.g.montanari.u.ea:from,
  year		= 2003,
  author	= {G. Ferrari and U. Montanari and R. Raggi and E. Tuosto},
  booktitle	= {First International Symposium on Formal Methods for
		  Components and Objects (FMCO)},
  series	= {Springer Lecture Notes in Computer Science},
  publisher	= {Springer},
  title		= { From Co-algebraic Specifications to Implementation: The
		  MIHDA toolkit}
}

@Unpublished{	  ferrari.g.montanari.u.ea:modelling,
  author	= {G. Ferrari and U. Montanari and E. Tuosto and B. Victor
		  and K. Yemane},
  note		= {Technical report, University of Pisa},
  year		= {2003},
  title		= {Modelling and Minimising the Fusion Calculus using
		  HD-automata}
}

@TechReport{	  gay.s.vasconcelos.vt.ea:session,
  year		= 2003,
  title		= {Session Types for Inter-Process Communication},
  number	= {2003--133},
  url		= {http://www.di.fc.ul.pt/~vv/papers/stipc.pdf},
  type		= {TR},
  month		= mar,
  institution	= {Department of Computing, University of Glasgow},
  author	= {Simon Gay and Vasco T. Vasconcelos and Ant{\'o}nio Ravara}
}

@InProceedings{	  giambiagi.p.schneider.g.ea:on,
  author	= {P. Giambiagi and G. Schneider and F. Valencia},
  year		= {2004},
  publisher	= {LNCS, Springer-Verlag},
  booktitle	= {In Proceedings of FOSSACS'04},
  title		= {On the Expressiveness of CCS-like Calculi}
}

@InProceedings{	  hirschkoff.d.lozes.e.ea:minimality,
  booktitle	= {Proc. of {FSTTCS}'2003},
  year		= 2003,
  author	= {D. Hirschkoff and E. Lozes and D. Sangiorgi},
  publisher	= {Springer Verlag},
  title		= {Minimality Results for the Spatial Logics},
  series	= {LNCS}
}

@Unpublished{	  lanese.i.montanari.u:mapping,
  author	= {I. Lanese and U. Montanari},
  note		= {Under Revision for Theory and Practice of Logic
		  Programming},
  year		= {2003},
  title		= {Mapping Fusion and Synchronized Hyper-edge Replacement
		  into Logic Programming}
}

@InProceedings{	  lozes.e:adjunct,
  title		= {Adjunct elimination in the static {A}mbient {L}ogic},
  note		= {to appear in ENTCS, Elsevier},
  year		= 2003,
  author	= {E. Lozes},
  booktitle	= {Proc. of {EXPRESS}'2003}
}

@InProceedings{	  m-miculan.is:framework,
  author	= {M. Miculan, I. Scagnetto},
  series	= {Lecture Notes in Computer Science 2747},
  publisher	= {ACM},
  year		= 2003,
  title		= {A Framework for Typed HOAS and Semantics},
  booktitle	= {Proc. of PPDP 2003, Uppsala}
}

@TechReport{	  martins.f.ravara.a:typing,
  institution	= {CLC, Department of Mathematics, Instituto Superior
		  T\'ecnico},
  address	= {1049-001 Lisboa, Portugal},
  note		= {Submitted for publication},
  title		= {Typing migration control in lsdpi},
  year		= {2003},
  type		= {Preprint},
  author	= {F. Martins and A. Ravara}
}

@Unpublished{	  monteiro.l:note,
  title		= {A note on models for spatial logic based on transition
		  systems with spatial structure},
  author	= {L.\ Monteiro},
  note		= {Technical Note, DI-FCT/UNL},
  year		= {2003}
}

@Unpublished{	  monteiro.l:note*1,
  note		= {Technical Note, DI-FCT/UNL},
  year		= {2003},
  author	= {L.\ Monteiro},
  title		= {A note on a noninterleaving model of concurrency based on
		  transition systems with spatial structure }
}

@InProceedings{	  nielsen.m.valencia.f:notes,
  author	= {Mogens Nielsen and Frank Valencia},
  booktitle	= {4th Advanced Course on Petri Nets ICPN'03},
  publisher	= {LNCS, Springer-Verlag},
  year		= {2004},
  title		= {Notes on Timed CCP}
}

@Article{	  ravara.a.matos.ag.ea:lexically,
  volume	= {85},
  title		= {Lexically scoped distribution: what you see is what you
		  get},
  journal	= {Electronic Notes in Theoretical Computer Science},
  number	= {1},
  note		= {Presented at FGC'03},
  url		= {http://www.elsevier.com/gej-ng/31/29/23/138/47/29/85.1.007.pdf}
		  ,
  year		= {2003},
  author	= {A. Ravara and A. G. Matos and V. T. Vasconcelos and L.
		  Lopes}
}

@TechReport{	  ravara.a.resende.p.ea:algebra,
  year		= {2003},
  title		= {An Algebra of Behavioural Types},
  address	= {1049-001 Lisboa, Portugal},
  type		= {Preprint},
  institution	= {CLC, Department of Mathematics, Instituto Superior
		  T\'ecnico},
  author	= {A. Ravara and P. Resende and V. Vasconcelos},
  pdf		= {http://www.cs.math.ist.utl.pt/ftp/pub/RavaraA/02-RRV-abt.pdf}
		  ,
  note		= {Submitted for publication}
}

@TechReport{	  ribeiro.a.caires.l.ea:verifying,
  title		= {Verifying the Arrow Protocol in a Spatial Logic},
  year		= 2003,
  author	= {A. Ribeiro and L. Caires and L. Monteiro},
  institution	= {Departamento de Informatica, FCT/UNL}
}

@TechReport{	  rueda.c.valencia.f:non-viability,
  author	= {C. Rueda and F. Valencia},
  note		= {WP1, Submitted for conference publication},
  year		= {2003},
  title		= {Non-Viability Deductions in Arc-Consistency Computation}
}

@Article{	  teller.d.zimmer.p.ea:using,
  year		= 2003,
  title		= {Using {A}mbients to {C}ontrol {R}esources (long version)},
  journal	= {International {J}ournal of {I}nformation {S}ecurity},
  author	= {D. Teller and P. Zimmer and D. Hirschkoff},
  note		= {to appear}
}

@Article{	  teller.d:formalisms,
  volume	= 85,
  note		= {Presented at FGC'03},
  year		= 2003,
  title		= {Formalisms for Mobile Resource Control},
  number	= 1,
  journal	= {Electronic Notes in Theoretical Computer Science},
  author	= {David Teller}
}

@TechReport{	  tuosto.e.victor.b.ea:polyadic,
  author	= {E. Tuosto and B. Victor and K. Yemane},
  title		= {Polyadic History-Dependent Automata for the Fusion
		  Calculus},
  institution	= "Department of Information Technology, Uppsala University",
  year		= 2003,
  number	= {2003-062},
  month		= dec
}

@PhDThesis{	  tuosto.e:non,
  author	= {E. Tuosto},
  year		= {2003},
  school	= {Dipartimento di Informatica, Univ. Pisa},
  title		= {Non Functional Aspects of Wide area Network Programming}
}

@InProceedings{	  valencia.f:concurrency,
  title		= {Concurrency, Time and Constraints},
  year		= {2003},
  author	= {F. Valencia},
  booktitle	= {Proceedings of the Nineteenth International Conference on
		  Logic Programming (ICLP 2003)},
  note		= {WP2, Invited publication},
  publisher	= {LNCS, Springer-Verlag}
}

@TechReport{	  valencia.f:on,
  month		= {Dec},
  note		= {WP2, Submitted to the Journal of Theoretical Computer
		  Science},
  year		= {2003},
  author	= {F. Valencia},
  title		= {On the Decidability of Timed CCP}
}

@InProceedings{	  valencia.f:timed,
  booktitle	= {Proceedings of the Nineteenth International Conference on
		  Logic Programming (ICLP 2003)},
  year		= {2003},
  publisher	= {LNCS, Springer-Verlag},
  title		= {Timed Concurrent Constraint Programming: Decidability
		  Results and their Application to LTL},
  author	= {F. Valencia}
}

@Article{	  vallecillo.a.vasconcelos.vt.ea:typing,
  year		= {2003},
  author	= {A. Vallecillo and V. T. Vasconcelos and A. Ravara},
  title		= {Typing the Behavior of Objects and Components using
		  Session Types},
  volume	= {68},
  journal	= {Electronic Notes in Theoretical Computer Science},
  url		= {http://www.elsevier.com/gej-ng/31/29/23/121/52/39/68.3.012.pdf}
		  ,
  note		= {Presented at FOCLASA'02},
  number	= {3}
}

@InProceedings{	  vanackere.v:history-dependent,
  publisher	= {Springer},
  title		= {History-Dependent Scheduling for Cryptographic Processes},
  author	= {V.~Vanackere},
  note		= {to appear},
  series	= {Springer Lecture Notes in Computer Science},
  booktitle	= { Proc. VMCAI 2004},
  year		= 2004
}

@TechReport{	  vieira.h.caires.l:spatial,
  author	= {H. Vieira and L. Caires},
  year		= {2003},
  title		= {Spatial Model Checker User's Manual},
  institution	= {Departamento de Informatica, FCT/UNL}
}