@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"
}