| [1] | Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, and Carl A. Gunter.
What packets may come: Automata for network monitoring.
In Proceedings of the Symposium on Principles of Programming
Languages (POPL'01), pages 206-219. ACM Press, January 2001. BibTeX entry |
| [2] | Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor
Obradovic, and Pamela Zave.
The Village Telephone System: A case study in formal software
engineering.
In Jim Grundy and Malcolm Newey, editors, Theorem Proving in
Higher Order Logics 11th International Conference TPHOLs '98, volume 1479
of Lecture Notes in Computer Science, pages 49-66, Canberra,
Australia, September 1998. Springer. BibTeX entry |
| [3] | Carl A. Gunter, Elsa L. Gunter, Michael Jackson, and Pamela Zave.
A reference model for requirements and specifications.
IEEE Software, 17(3):37-43, May 2000. BibTeX entry |
| [4] | Bow-Yaw Wang, José Meseguer, and Carl A. Gunter.
Specification and formal verification of a PLAN algorithm in
Maude.
In Tenh Lai, editor, 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. IEEE Computer Society, April 2000. BibTeX entry |
| [5] | Carl A. Gunter, Elsa L. Gunter, Michael Jackson, and Pamela Zave.
A reference model for requirements and specifications (abstract),
June 2000.
Best Paper for International Conference on Requirements Engineering. BibTeX entry |
| [6] | Carl A. Gunter, Pankaj Kakkar, and Martín Abadi.
Reasoning about secrecy for active networks, July 2000.
Computer Security Foundations Workshop. BibTeX entry |
| [7] | Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic.
Fault origin adjudication, August 2000.
Formal Methods in Software Practice. BibTeX entry |
| [8] | Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic,
Oleg Sokolsky, and Mahesh Viswanathan.
Verisim: Formal analysis of network simulations, August 2000.
International Symposium on Software Testing and Analysis. BibTeX entry |
| [9] | Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic.
RIP in SPIN/HOL, August 2000.
Theorem Provers for Higher-Order Logics. BibTeX entry |
| [10] | Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter.
Formal verification of standards for distance vector routing
protocols, August 1999.
Presented in the Recent Research Session at Sigcomm 1999. BibTeX entry |
| [11] | Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter.
Formal verification of standards for distance vector routing
protocols, 2000.
Working Paper. Presented in the Recent Research Session at Sigcomm
1999. BibTeX entry |
| [12] | Davor Obradovic and Elsa Gunter.
Towards the Integration of Model Checking and Theorem
Proving: Embedding a Subset of Promela into HOL, May 2000.
submitted for publication. BibTeX entry |
| [13] | Karthikeyan Bhargavan, Davor Obradovic, and Carl A. Gunter.
Formal verification of standards for distance vector routing
protocols, 2002.
Journal of the ACM, to appear. BibTeX entry |
| [14] | K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, and
M. Viswanathan.
Verisim: Formal Analysis of Network Simulations.
IEEE Transactions on Software Engineering, 28(2):129-145,
February 2002. BibTeX entry |
| [15] | Davor Obradovic.
Real-time model and convergence time of bgp.
In Proceedings of IEEE Infocom, 2002. BibTeX entry |
| [16] | Karthikeyan Bhargavan and Carl A. Gunter.
Requirements for a practical network event recognition language.
In Proceedings of the Runtime Verification Workshop, July 2002. BibTeX entry |
| [17] | Karthikeyan Bhargavan and Carl A. Gunter.
Network event recognition for packet-mode surveillance.
Submitted for publication, 2002. BibTeX entry |