our.bib

@UNPUBLISHED{BhargavanG02ow,
  AUTHOR = {Karthikeyan Bhargavan and Carl A. Gunter},
  TITLE = {Network Event Recognition for Packet-Mode Surveillance},
  NOTE = {Submitted for publication},
  YEAR = {2002}
}

@INPROCEEDINGS{BhargavanG02,
  AUTHOR = {Karthikeyan Bhargavan and Carl A. Gunter},
  TITLE = { Requirements for a Practical Network Event Recognition Language},
  OPTCROSSREF = {},
  OPTKEY = {},
  BOOKTITLE = {Proceedings of the Runtime Verification Workshop},
  OPTPAGES = {},
  YEAR = {2002},
  OPTEDITOR = {},
  OPTVOLUME = {},
  OPTNUMBER = {},
  OPTSERIES = {},
  OPTADDRESS = {},
  MONTH = {July},
  OPTORGANIZATION = {},
  OPTPUBLISHER = {},
  OPTNOTE = {},
  OPTANNOTE = {}
}

@INPROCEEDINGS{Obradovic02,
  AUTHOR = {Davor Obradovic},
  TITLE = {Real-time Model and Convergence Time of BGP},
  OPTCROSSREF = {},
  OPTKEY = {},
  BOOKTITLE = {Proceedings of IEEE Infocom},
  OPTPAGES = {},
  YEAR = {2002},
  OPTEDITOR = {},
  OPTVOLUME = {},
  OPTNUMBER = {},
  OPTSERIES = {},
  OPTADDRESS = {},
  OPTMONTH = {},
  OPTORGANIZATION = {},
  OPTPUBLISHER = {},
  OPTNOTE = {},
  OPTANNOTE = {}
}

@ARTICLE{BhargavanGKLOSV02,
  AUTHOR = {K. Bhargavan and C.A. Gunter and M. Kim and I. Lee and D. Obradovic and O. Sokolsky and M. Viswanathan },
  TITLE = {{Verisim: Formal Analysis of Network Simulations}},
  JOURNAL = {IEEE Transactions on Software Engineering},
  YEAR = {2002},
  OPTKEY = {},
  VOLUME = {28},
  NUMBER = {2},
  PAGES = {129-145},
  MONTH = {February},
  OPTNOTE = {},
  OPTANNOTE = {}
}

@MISC{BhargavanOG02jacm,
  AUTHOR = {Karthikeyan Bhargavan and Davor Obradovic and Carl A. Gunter},
  TITLE = {Formal Verification of Standards for Distance Vector
Routing Protocols},
  YEAR = 2002,
  NOTE = {Journal of the ACM, to appear.}
}

@MISC{GunterO00,
  AUTHOR = {Davor Obradovic and Elsa Gunter},
  TITLE = {Towards the {I}ntegration of {Model Checking} and
{T}heorem {P}roving: {E}mbedding a {S}ubset of {P}romela into {HOL}},
  YEAR = 2000,
  MONTH = {May},
  NOTE = {submitted for publication}
}

@MISC{BhargavanOG00jacm,
  AUTHOR = {Karthikeyan Bhargavan and Davor Obradovic and Carl A. Gunter},
  TITLE = {Formal Verification of Standards for Distance Vector
Routing Protocols},
  YEAR = 2000,
  NOTE = {Working Paper. Presented in the Recent Research Session at Sigcomm 1999}
}

@MISC{BhargavanOG99,
  AUTHOR = {Karthikeyan Bhargavan and Davor Obradovic and Carl A. Gunter},
  TITLE = {Formal Verification of Standards for Distance Vector
Routing Protocols},
  YEAR = 1999,
  MONTH = {August},
  NOTE = {Presented in the Recent Research Session at Sigcomm 1999}
}

@MISC{BhargavanOG00tphols,
  AUTHOR = {Karthikeyan Bhargavan and Carl A. Gunter and Davor Obradovic},
  TITLE = {{RIP in SPIN/HOL}},
  MONTH = {August},
  YEAR = 2000,
  ADDRESS = {Portland, OR},
  NOTE = {Theorem Provers for Higher-Order Logics}
}

@MISC{BhargavanGKLOSV00,
  AUTHOR = {Karthikeyan Bhargavan and Carl A. Gunter and Moonjoo
Kim and Insup Lee and Davor Obradovic and Oleg Sokolsky and Mahesh Viswanathan},
  TITLE = {Verisim: Formal Analysis of Network Simulations},
  MONTH = {August},
  YEAR = 2000,
  ADDRESS = {Portland, OR},
  NOTE = {International Symposium on Software
Testing and Analysis}
}

@MISC{BhargavanOG00fmsp,
  AUTHOR = {Karthikeyan Bhargavan and Carl A. Gunter and Davor Obradovic},
  TITLE = {Fault Origin Adjudication},
  MONTH = {August},
  YEAR = 2000,
  ADDRESS = {Portland, OR},
  NOTE = {Formal Methods in Software Practice}
}

@MISC{GunterKA00,
  AUTHOR = {Carl A. Gunter and Pankaj Kakkar and Mart\'{\i}n Abadi},
  TITLE = {Reasoning about Secrecy for Active Networks},
  YEAR = 2000,
  MONTH = {July},
  ADDRESS = {Cambridge, England},
  NOTE = {Computer Security Foundations Workshop}
}

@MISC{GunterGJZ99icre,
  AUTHOR = {Carl A. Gunter and Elsa L. Gunter and Michael Jackson and Pamela Zave},
  TITLE = {A Reference Model for Requirements and
Specifications (Abstract)},
  YEAR = 2000,
  MONTH = {June},
  NOTE = {Best Paper for International Conference on
Requirements Engineering.}
}

@INPROCEEDINGS{WangMG00,
  AUTHOR = {Bow-Yaw Wang and Jos\'e Meseguer and Carl A. Gunter},
  TITLE = {Specification and Formal Verification of a {PLAN} Algorithm
in {Maude}},
  YEAR = 2000,
  BOOKTITLE = {Proceedings of the 2000 {ICDCS} workshop on Internet 2000,
Distributed Real-Time Systems, Group Computation and Communications, Wireless
Networks and Mobile Computing, Distributed System Validation and
Verification, Knowledge Discovery and Data Mining in the World Wide
Web},
  PAGES = {E:49-E:56},
  PUBLISHER = {{IEEE} Computer Society},
  MONTH = {April},
  EDITOR = {Tenh Lai}
}

@ARTICLE{GunterGJZ00iee,
  AUTHOR = {Carl A. Gunter and Elsa L. Gunter and Michael Jackson and Pamela Zave},
  TITLE = {A Reference Model for Requirements and Specifications},
  YEAR = 2000,
  MONTH = {May},
  JOURNAL = {{IEEE} Software},
  VOLUME = 17,
  NUMBER = 3,
  PAGES = {37-43}
}

@INPROCEEDINGS{BhargavanGGJOZ98,
  AUTHOR = {Karthikeyan Bhargavan and Carl A. Gunter and Elsa L. Gunter and Michael Jackson and Davor Obradovic and Pamela Zave},
  TITLE = {The {Village Telephone System}: A Case Study in Formal Software Engineering},
  BOOKTITLE = {Theorem Proving in Higher Order Logics 11th International Conference {TPHOLs} '98},
  YEAR = 1998,
  MONTH = {September},
  EDITOR = {Jim Grundy and Malcolm Newey},
  ADDRESS = {Canberra, Australia},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1479,
  PAGES = {49-66},
  PUBLISHER = {Springer}
}

@INPROCEEDINGS{BhargavanCMG01,
  AUTHOR = {Karthikeyan Bhargavan and Satish Chandra and Peter J. McCann and
      Carl A. Gunter },
  TITLE = {What Packets May Come: Automata for Network Monitoring},
  BOOKTITLE = {Proceedings of the Symposium on Principles of Programming Languages (POPL'01)},
  PAGES = {206-219},
  YEAR = {2001},
  MONTH = {January},
  PUBLISHER = {ACM Press}
}