@Article(milner.parrow.ea:calculus-mobile
  ,author       = {Robin Milner and Joachim Parrow and David Walker}
  ,title        = {A Calculus of Mobile Processes, Part {I/II}}
  ,journal      = {Journal of Information and Computation}
  ,year         = 1992
  ,volume       = 100
  ,pages        = {1--77}
  ,note          = {http://www.lfcs.informatics.ed.ac.uk/reports/89/ECS-LFCS-89-85/}
  ,month        = sep
)

@Book(milner:communicating-mobile
  ,author       = {Robin Milner}
  ,title        = {Communicating and Mobile Systems: the $\pi$-Calculus}
  ,publisher    = {Cambridge University Press}
  ,year         = 1999
  ,isbn         = {0 521 64320 1 (hc), 0 521 65869 1 (pbk)}
  ,month        = may
)

@book{milner:comconcurrency,
 author = {Robin Milner},
 title = {Communication and concurrency},
 year = {1989},
 isbn = {0-13-114984-9},
 publisher = {Prentice Hall},
 address = {Hertfordshire, UK},
 }

@inproceedings{stirlingwalker:local,
 author = {Colin Stirling and David Walker},
 title = {Local model checking in the modal mu-calculus},
 booktitle = {TAPSOFT '89: 2nd international joint conference on Theory and practice of software development},
 year = {1991},
 pages = {161--177},
 location = {Barcelona, Spain},
 doi = {http://dx.doi.org/10.1016/0304-3975(90)90110-4},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands},
 }

@Article(milner.parrow.ea:modal-logics
  ,author       = {Robin Milner and Joachim Parrow and David Walker}
  ,title        = {Modal logics for mobile processes}
  ,journal      = tcs
  ,volume       = 114
  ,year         = 1993
  ,pages        = {149--171}
  ,note          = {\\http://www.it.kth.se/\~{}joachim/modmob.ps.gz}
  ,abstract     = {In process algebras, bisimulation equivalence is typically
                  defined directly in terms of the operational rules of
                  action; it also has an alternative characterization in
                  terms of a simple modal logic (sometimes called
                  Hennessy-Milner logic). This paper first defines two forms
                  of bisimulation equivalence for the pi-calculus, a process
                  algebra which allows dynamic reconfiguration among
                  processes; it then explores a family of possible logics,
                  with different modal operators. It is proven that two of
                  these logics characterize the two bisimulation
                  equivalences. Also, the relative expressive power of all
                  the logics is exhibited as a lattice. The results are
                  applicable to most value-passing process algebras.}
)

@InProceedings(dam:proof-systems
  ,author       = {Mads Dam}
  ,title        = {Proof Systems for pi-Calculus Logics}
  ,booktitle    = {Logic for Concurrency and Synchronisation}
  ,year         = {2001}
  ,editor       = {R. de Queiroz}
  ,series       = {Studies in Logic and Computation}
  ,note          = {\\http://www.imit.kth.se/\~{}mfd/Papers/pspcl.pdf}
  ,publisher    = {Oxford University Press}
  ,abstract     = {In this paper we study the problem of verifying general
                  temporal and functional properties of mobile and dynamic
                  process networks, cast in terms of the pi-calculus. Much of
                  the expressive power of this calculus derives from the
                  combination of name generation and communication (to handle
                  mobility) with dynamic process creation. In the paper we
                  introduce the $\pi$-$\mu$-calculus, an extension of the
                  modal mu-calculus with name equality, inequality,
                  first-order universal and existential quantification, and
                  primitives for name input and output as an appropriate
                  temporal logic for the pi-calculus. A compositional proof
                  system is given with the scope of verifying dynamic
                  networks of pi-calculus agents against properties specified
                  in this logic. The proof system consists of a local part
                  based, roughly, on the classical sequent calculus extended
                  with data structures for private names, and rules to
                  support process structure dependent reasoning. In addition
                  the proof system contains a rule of discharge to close
                  well-founded cycles in the proof graph. The proof system is
                  shown to be sound in general and weakly complete for the
                  non-recursive fragment of the specification logic. We also
                  obtain a weak completeness result for recursive formulas
                  against finite-control calculus processes. Two examples are
                  considered. The first example is based on Milner's encoding
                  of data types into the pi-calculus, specifically the
                  natural numbers. This encoding is interesting from the
                  point of view of verification, since it makes essential use
                  of all the distinguishing features of the pi-calculus,
                  including dynamic process creation. Corresponding to the
                  encoding of natural numbers into the $\pi$-calculus we
                  propose an encoding of the type of natural numbers into the
                  $\pi$-$\mu$-calculus and establish some type correctness
                  properties. As the second example we consider a
                  garbage-collecting unbounded buffer (which dynamically
                  create and destroy buffer cells) and show how to establish
                  absence of spurious output of such a system.}
)

@Article(dam:model-checking
  ,author       = {Mads Dam}
  ,title        = {Model Checking Mobile Processes}
  ,journal      = {Journal of Information and Computation}
  ,year         = 1996
  ,volume       = 129
  ,number       = 1
  ,pages        = {35--51}
  ,note         = {Also available as Research Report R94:01, SICS, Sweden. A
                  summary appeared in {\em Proceedings of CONCUR '93\/}, LNCS
                  715. http://web.it.kth.se/\~{}mfd/Papers/mcmpiac.pdf}
)

@InProceedings(parrow:csma
  ,author       = {Joachim Parrow}
  ,title        = {Verifying a {CSMA/CD}-protocol with {CCS}}
  ,booktitle    = {Proceedings of the IFIP WG6.1 Eighth International Symposium on Protocol Specification, Testing, and Verification}
  ,pages        = {373--384}
  ,month        = jun
  ,year         = 1988
  ,note         = {\\http://www.imit.kth.se/courses/2G1516/Docs05/CCS/CSMA-CD-Parrow.pdf}
)

@article{hoare:csp,
 author = {C. A. R. Hoare},
 title = {Communicating sequential processes},
 journal = {Commun. ACM},
 volume = {26},
 number = {1},
 year = {1983},
 issn = {0001-0782},
 pages = {100--106},
 doi = {http://doi.acm.org/10.1145/357980.358021},
 publisher = {ACM Press},
 address = {New York, USA}
 }

@inbook{parrow:intropi,
 author = {Joachim Parrow},
 title = {Handbook of Process Algebra},
 chapter = {An introduction to the pi-Calculus},
 pages = {479--543},
 publisher = {Elsevier},
 year = 2001,
 note = {\\http://user.it.uu.se/\~{}joachim/intro.ps}
}

@book{sanwalker:pitheory,
 author = {Davide Sangiorgi and David Walker},
 title = {The Pi-Calculus: A Theory of Mobile Processes},
 publisher = {Cambridge University Press},
 year = 2001
}

@book{winskel:intro,
 author = {Glynn Winskel},
 title = {The Formal Semantics of Programming Languages},
 publisher = {MIT Press},
 year = 1993
}


@book{peled:reliability,
 author = {Doron A. Peled},
 title = {Software reliability methods},
 year = {2001},
 isbn = {0-387-95106-7},
 publisher = {Springer-Verlag New York},
 address = {Secaucus, NJ, USA},
 }

@book{holzmann:protocol,
 author = {Gerard J. Holzmann},
 title = {Design and validation of computer protocols},
 year = {1991},
 isbn = {0-13-539925-4},
 publisher = {Prentice-Hall},
 address = {Upper Saddle River, NJ, USA},
 note = {\\http://spinroot.com/spin/Doc/Book91.html}
 }

@inbook{bradfieldstirling:modal,
  author = {J. Bradfield and C. Stirling},
  title = {Handbook of Process Algebra},
  chapter = {Modal logics and mu-calculi: an introduction},
  publisher = {Elsevier},  
  year = 2001,
  note = {\\http://www.dcs.ed.ac.uk/home/jcb/Research/bradfield-stirling-HPA-mu-intro.ps.gz}
}

@Article(kozen:mu
  ,author       = {Dexter Kozen}
  ,title        = {Results on the propositional $\mu$-calculus}
  ,journal      = {Theoret. Comput. Sci.}
  ,year         = 1983
  ,number       = 27
  ,volume       = 1
  ,pages        = {333--354}
)

@book{holzmann:spin,
 author = {Gerard J. Holzmann},
 title = {The SPIN Model Checker},
 year = {2003},
 isbn = {0-321-22862-6},
 publisher = {Addison-Wesley},
 note = {\\http://spinroot.com/spin/Doc/Book\_extras/index.html}
 }

@Misc{RFC2002,
  author =       "C. Perkins",
  title =        "{RFC 2002}: {IP} Mobility Support",
  month =        oct,
  year =         "1996",
  bibdate =      "Sat Mar 21 15:53:14 1998",
  note =         "Updated by RFC2290 \cite{RFC2290}. Status: PROPOSED
                 STANDARD.",
  URL =          "ftp://ftp.internic.net/rfc/rfc2002.txt,
                 ftp://ftp.internic.net/rfc/rfc2290.txt,
                 ftp://ftp.math.utah.edu/pub/rfc/rfc2002.txt,
                 ftp://ftp.math.utah.edu/pub/rfc/rfc2290.txt",
  acknowledgement = ack-nhfb,
  format =       "TXT=193103 bytes",
  online =       "yes",
  status =       "PROPOSED STANDARD",
  updatedby =    "Updated by RFC2290 \cite{RFC2290}.",
}

@Misc{RFC2290,
  author =       "J. Solomon and S. Glass",
  title =        "{RFC 2290}: Mobile-{IPv4} Configuration Option for
                 {PPP IPCP}",
  month =        feb,
  year =         "1998",
  bibdate =      "Wed Mar 4 13:58:32 MST 1998",
  note =         "Updates RFC2002 \cite{RFC2002}. Status: PROPOSED
                 STANDARD.",
  URL =          "ftp://ftp.internic.net/rfc/rfc2002.txt,
                 ftp://ftp.internic.net/rfc/rfc2290.txt,
                 ftp://ftp.math.utah.edu/pub/rfc/rfc2002.txt,
                 ftp://ftp.math.utah.edu/pub/rfc/rfc2290.txt",
  acknowledgement = ack-nhfb,
  format =       "TXT=39421 bytes",
  online =       "yes",
  status =       "PROPOSED STANDARD",
  updates =      "Updates RFC2002 \cite{RFC2002}.",
}

@Article(ismailov:slm
  ,author       = {B. Landfeldt and T. Larsson and Y. Ismailov and A. Seneviratne}
  ,title        = {{SLM}, A Framework for Session Layer Mobility Management}
  ,journal      = {ICCCN99}
  ,month        = Oct 
  ,year         = 1999
)

@Mastersthesis(wang:rebind
  ,author       = {YaoShuang Wang}
  ,title        = {Mobility Support for Networked Applications built in the {TCP/IP} Stack}
  ,school       = {KTH}
  ,year         = 2006
)

@article{San96acta,
   author = {Sangiorgi, D.},
   title = {A Theory of Bisimulation for  the $\pi$-calculus},   
   journal = {Acta Informatica},
   year = {1996},
   volume = {33},
    pages =   {69--97},
   note = {An extract  appeared in  {\em {P}roc. {CONCUR} '93},
		 Lecture Notes in Computer Science 715, 
                 Springer Verlag}
}

@Article{promtrans,
   author = {Hosung Song and Kevin J. Compton},
   title = {Verifying $\pi$-calculus processes by {Promela} translation},
   journal = {Technical Report 472, University of Michigan},
   year = 2003,
   note = {\\http://www.eecs.umich.edu/techreports/cse/03/CSE-TR-472-03.pdf}
}

@PhDThesis(victor:verification-tool
  ,author       = {Bj{\"o}rn Victor}
  ,title        = {A Verification Tool for the Polyadic $\pi$-Calculus}
  ,school       = {Department of Computer Systems, Uppsala University,
                  Sweden}
  ,year         = {1994}
  ,month        = {May}
  ,type         = {Licentiate thesis}
  ,note         = {Available as report {DoCS 94/50}. \\http://www.docs.uu.se/\~{}victor/tr/docs-tr-94-50.html}
  ,abstract     = {This thesis describes the polyadic version of the Mobility
                  Workbench (MWB), an automated tool for manipulating and
                  analyzing mobile concurrent systems (those with evolving
                  connectivity structures) described in the polyadic
                  pi-calculus. The main feature of this version of the MWB is
                  checking open bisimulation equivalences, and doing so with
                  efficiency in mind.
                  
                  The open bisimulation equivalences are described in a
                  polyadic setting, and efficient characterisations of both
                  the strong and the weak equivalences are presented and
                  proven to coincide with their standard formulations.
                  
                  The equivalence checking algorithm, which by necessity
                  generates the state space ``on-the-fly'', is presented in
                  detail and proven correct. Aspects of the implementation of
                  the tool are described in some detail, for example the
                  representation of pi-calculus agents using de Bruijn
                  indices.
                  
                  We illustrate the MWB with an example automated analysis of
                  a handover protocol for a mobile telephone system.}
)

@Article(sprengerdam:globalinduction
  ,author       = {C. Sprenger and M. Dam}
  ,title        = {A note on global induction mechanisms in $\mu$-calculus with explicit approximations.}
  ,journal    = {Theoretical Informatics and Applications}
  ,pages        = {365--399}
  ,volume       = 1
  ,number       = 37
  ,year         = 2003
  ,note         = {\\http://www.imit.kth.se/\~{}mfd/Papers/ITA-final.pdf}
)

@Misc(beste:prover
  ,author       = {Fredrick B. Beste}
  ,title        = {The Model Prover --- a sequent-calculus based modal $\mu$-calculus model checker tool for finite control $\pi$-calculus agents}
  ,year         = 1998
  ,note         = {\\http://www.it.uu.se/profundis/mwb-dist/x4.ps.gz}
)
@Misc(mitchell:cryptoanalysis
  ,author       = {J. C. Mitchell and M. Mitchell and U. Stern}
  ,title        = {Automated analysis of cryptographic protocols using Murphi}
  ,year         = 1997
  ,note         = {\\http://sprout.stanford.edu/dill/PAPERS/verification/MMS97.ps}
)

@article{milner:interaction,
 author = {Robin Milner},
 title = {Elements of interaction: Turing award lecture},
 journal = {Commun. ACM},
 volume = {36},
 number = {1},
 year = {1993},
 issn = {0001-0782},
 pages = {78--89},
 doi = {http://doi.acm.org/10.1145/151233.151240},
 publisher = {ACM Press},
 address = {New York, USA},
 }

@book{baeten:procalg,
 author = {J. C. M. Baeten and W. P. Weijland},
 title = {Process algebra},
 year = {1990},
 isbn = {0-521-40043-0},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@article{parrow:cwb,
 author = {Rance Cleaveland and Joachim Parrow and Bernhard Steffen},
 title = {The concurrency workbench: a semantics-based tool for the verification of concurrent systems},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {15},
 number = {1},
 year = {1993},
 issn = {0164-0925},
 pages = {36--72},
 doi = {http://doi.acm.org/10.1145/151646.151648},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@Article(walker:mutex
  ,author       = {David Walker}
  ,title        = {Analysing Mutax Exclusion Algorithms Using CCS}
  ,journal      = {Formal Aspects of Computing}
  ,pages        = {273--292}
  ,volume       = 1
  ,year         = 1989
)

@INPROCEEDINGS{blanchet:proverif,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Automatic {V}erification of {C}ryptographic {P}rotocols:
{A} {L}ogic {P}rogramming {A}pproach (invited talk)},
  BOOKTITLE = {5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03)},
  PAGES = {1--3},
  YEAR = {2003},
  ADDRESS = {Uppsala, Sweden},
  MONTH = AUG,
  PUBLISHER = {ACM},
  note = {\\http://www.di.ens.fr/\~{}blanchet/publications/BlanchetPPDP03.pdf}
}

@article{oravaparrow:algebraic,
    author = "Fredrik Orava and Joachim Parrow",
    title = "An Algebraic Verification of a Mobile Network",
    journal = "Journal of Formal Aspects of Computing",
    volume = "4",
    pages = "497--543",
    year = "1992",
    note = "http://citeseer.ist.psu.edu/orava91algebraic.html" 
}

@PhDThesis(sangiorgi:expressing-mobility
  ,author       = {Davide Sangiorgi}
  ,title        = {Expressing Mobility in Process Algebras: First-Order and
                  Higher-Order Para\-digms}
  ,school       = {University of Edinburgh}
  ,note         = {CST-99-93 (also published as ECS-LFCS-93-266)}
  ,year         = 1993
)

@inproceedings{berry:chem,
 author = {Gerard Berry and Gerard Boudol},
 title = {The chemical abstract machine},
 booktitle = {POPL '90: Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 year = {1990},
 isbn = {0-89791-343-4},
 pages = {81--94},
 location = {San Francisco, California, United States},
 doi = {http://doi.acm.org/10.1145/96709.96717},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@techreport{engberg.nielsen:calculus,
    author = "U. Engberg and M. Nielsen",
    title = "A Calculus of Communicating Systems with Label-Passing",
    year = "1986",
    note = "http://citeseer.ist.psu.edu/engberg86calculus.html" 
}

@Article(nestmann.victor:calculi-mobile
  ,author       = {Uwe Nestmann and Bj{\"o}rn Victor}
  ,title        = {Calculi for Mobile Processes: Bibliography and Web Pages}
  ,journal      = {Bulletin of the EATCS}
  ,year         = 1998
  ,volume       = 64
  ,pages        = {139--144}
  ,month        = feb
  ,url          = {http://move.to/mobility}
)

@Mastersthesis(widell.arvidsson:session
  ,author       = {Micael Widell and Petter Arvidsson}
  ,title        = {Design of the Session Layer Supporting Mobile, Delay and Disconnection Tolerant Communication}
  ,school       = {KTH}
  ,year         = 2006
  ,note         = {To appear}
)

@Book(paulson:logic
  ,author       = {Lawrence C. Paulson}
  ,title        = {Logic and Computation}
  ,publisher    = {Cambridge University Press}
  ,year         = 1987
  ,isbn         = {0 521 34632 0}
)

@article{tennent:denotational,
 author = {R. D. Tennent},
 title = {The denotational semantics of programming languages},
 journal = {Commun. ACM},
 volume = {19},
 number = {8},
 year = {1976},
 issn = {0001-0782},
 pages = {437--453},
 doi = {http://doi.acm.org/10.1145/360303.360308},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{plotkin:powerdomain,
 author = {Gordon D. Plotkin},
 title = {A Powerdomain Construction},
 journal = {SIAM J. Comput.},
 volume = {5},
 number = {3},
 year = {1976},
 pages = {452--487},
 }

@article{owicki.gries:axiomaticparallel,
   author = {Susan Owicki and David Gries},
   title = {An Axiomatic Proof Technique of Parallel Programs I},   
   journal = {Acta Informatica},
   year = {1976},
   volume = {6},
   pages =   {319--340}
}

@article{stirling:joysbisim,
    author = "Colin Stirling",
    title = "The Joys of Bisimulation",
    journal = "Lecture Notes in Computer Science",
    volume = "1450",
    pages = "142--152",
    year = "1998",
    url = "http://citeseer.ist.psu.edu/stirling98joy.html" 
}

@inproceedings{milner:funproc,
 author = {Robin Milner},
 title = {Functions as processes},
 booktitle = {Proceedings of the seventeenth international colloquium on Automata, languages and programming},
 year = {1990},
 isbn = {0-387-52826-1},
 pages = {167--180},
 location = {Warwick University, England},
 publisher = {Springer-Verlag New York, Inc.},
 address = {New York, NY, USA},
 }

@inproceedings{ekwall:robusttcp,
  author = "R. Ekwall and P. Urban and A. Schiper",
  title = "Robust {TCP} connections for fault tolerant computing",
  booktitle = "Proceedings of the ninth international conference on Parallel and Distributed Systems (ICPADS)",
  location = "Chung-li, Taiwan",
  month = "dec",
  year = "2002",
  url = "http://citeseer.ist.psu.edu/ekwall03robust.html" 
}

@misc{iso-osi,
 author = {{International Organization for Standardization}},
 title = {{ISO} standard 7498-1, {"Information Processing Systems - OSI Reference Model. The Basic Model"}}, 
 note =  {http://www.acm.org/sigcomm/standards/iso\_stds/\\OSI\_MODEL/ISO\_IEC\_7498-1.TXT}
}

@inproceedings{maltz:msocks,
  author = "David A. Maltz and Pravin Bhagwat",
  title = "MSOCKS: An architecture for transport layer mobility",
  booktitle = "Proceedings of {IEEE INFOCOM} 1998 - The Conference on Computer Communications",
  month = "apr",
  year = "1998",
  pages = "1037--1045"
}

@inproceedings{nikander:hip,
  author = "P. Nikander and J. Ylitalo and J. Wall",
  title = "Integrating security, mobility, and multi-homing in a {HIP} way",
  booktitle = "Proceedings of the Network and Distributed Systems Security Symposium (NDSS)",
  month = "feb",
  year = "2003",
  pages = "87--99",
  publisher = "Ericsson Research NomadicLab"
}

@inproceedings{snoeren:reconsidering,
   author =       "Alex Snoeren and Hari Balakrishnan and Frans Kaashoek",
   title =        "{Reconsidering Internet Mobility}",
   booktitle =    {8th Workshop on Hot Topics in Operating Systems},
   year =         {2001},
   month =        {May},
   address =      {Elmau/Oberbayern, Germany}
}

@inproceedings{stoica:internet,
  author = "I. Stoica and D. Adkins and S. Zhuang and S. Shenker and S. Surana",
  title = "Internet indirection infrastructure",
  text = "Proceedings of the ACM SIGCOMM Conference (SIGCOMM)",
  month = "aug",
  year = "2002",
  pages = "73--88",
  url = "http://citeseer.ist.psu.edu/stoica02internet.html" 
}

@article{eddy:belong,
    author = "Wesly M. Eddy",
    title = "At What Layer Does Mobility Belong?",
    journal = "IEEE Communications Magazine",
    month = "oct",
    year = "1998"
}

@inproceedings{qu:mobilesock,
  author = "X. Qu and J. X. Yu and R. P. Brent",
  title = "A Mobile {TCP} Socket",
  booktitle = "Proceedings of the International Conference on Software Engineering (SE)",
  month = "nov",
  year = "1997",
  location = "San Francisco, USA"
}

@inproceedings{zandy:reliablenet,
  author = "Victor C. Zandy and Barton P. Miller",
  title = "Reliable Network Connections",
  booktitle = "Proceedings of the 8th annual international conference on Mobile computing and networking",
  year = "2002"
}

@inproceedings{barendregt:lambda,
    author = "H. P. Barendregt",
    title = "Introduction to Lambda Calculus",
    booktitle = "Aspen{\ae}s Workshop on Implementation of Functional Languages, G{\"o}teborg",
    publisher = "Programming Methodology Group, University of G{\"o}teborg and Chalmers University of Technology",
    year = "1988",
    url = "http://citeseer.ist.psu.edu/barendregt94introduction.html" 
}

@inproceedings{turing:computable,
    author = "Alan Turing",
    title = "On Computable Numbers, With an Application to the Entscheidungsproblem",
    booktitle = "Proceedings of the London Mathematical Society",
    volume = 42,
    series = 2,
    year = "1936",
    url = "http://www.abelard.org/turpap2/tp2-ie.asp" 
}

@article{church:unsolvable,
    author = "Alonzo Church",
    title = "An unsolvable problem of elementary number theory",
    journal = "American Journal of Mathematics",
    volume = 58,
    year = "1936",
    pages = "345--363"
}

@article{cerf:archmodel,
    author = "Vinton G. Cerf and E. Cain",
    title = "The {DoD} Internet architecture model",
    journal = "Computer Networks",
    volume = 7,
    year = "1983",
    month = oct,
    pages = "307--318"
}

@inproceedings{ismailov:endsys,
author = {Yuri Ismailov and Jan Holler and Stephen Herborn and Aruna Seneviratne},
title = {Internet Mobility: An Approach to Mobile End-System Design},
booktitle = {International Conference on Networking, International Conference on Systems and International Conference on Mobile Communications and Learning Technologies (ICNICONSMCL)},
volume = {0},
year = {2006},
isbn = {0-7695-2552-0},
pages = {124--131},
doi = {http://doi.ieeecomputersociety.org/10.1109/ICNICONSMCL.2006.129},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}

@book{clarke.peled:modelcheck,
 author = {Edmund M. Clarke and Orna Grumberg and Doron A. Peled},
 title = {Model Checking},
 year = {1999},
 isbn = {0-262-03270-8},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
 }

@article{hoare:axiomatic,
 author = {C. A. R. Hoare},
 title = {An axiomatic basis for computer programming},
 journal = {Commun. ACM},
 volume = {26},
 number = {1},
 year = {1983},
 issn = {0001-0782},
 pages = {53--56},
 doi = {http://doi.acm.org/10.1145/357980.358001},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@unpublished{dijkstra:cruelty,
   author = "Edsger W. Dijkstra",
   title = "On the cruelty of really teaching computing science",
   month = dec,
   year = "1988",
   note = "Circulated privately",
   url = "http://www.cs.utexas.edu/users/EWD/ewd10xx/EWD1036.PDF"
}

@unpublished{dijkstra:bug,
   author = "Edsger W. Dijkstra",
   title = "Notes on {S}tructured {P}rogramming",
   month = apr,
   year = "1970",
   note = "Circulated privately",
   url = "http://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF"
}


@inbook{glabbeek:lineari,
  author = "R. J. van Glabbeek",
  chapter = "The Linear Time -- Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes",
  title = "Handbook of Process Algebra",
  publisher = "Elsevier",
  address = "Amsterdam, The Netherlands",
  year = 2001,
  url = "http://citeseer.ist.psu.edu/328833.html" 
}