The Verinet group at Penn investigates methodology and tool support for the formal analysis of Network Protocols. We are interested in all aspects of the formal analysis, including Specification of network protocols, Formal Proofs of correctness, Simulation and Testing.

People

Carl Gunter, Professor
Karthikeyan Bhargavan, PhD Student
Davor Obradovic, PhD Student

Current Projects

Recent Papers

[1] 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 Download PS. Download PDF.
[2] Karthikeyan Bhargavan and Carl A. Gunter. Network event recognition for packet-mode surveillance. Submitted for publication, 2002.
BibTeX entry Download PS. Download PDF.
[3] 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 Download PS. Download PDF.
[4] 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 Download PS. Download PDF.
[5] Davor Obradovic. Real-time Model and Convergence Time of BGP, INFOCOM, 2002.
BibTeX entry. Download PS.
[6] Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, and Carl A. Gunter. What Packets May Come: Automata for Network Monitoring, Principles of Programming Languages, January 2001.
BibTeX entry. Download PS. Download PDF.
[7] Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, and Mahesh Viswanathan. Verisim: Formal analysis of network simulations, International Symposium on Software Testing and Analysis, August 2000.
BibTeX entry. Download PS.
[8] Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic. Fault origin adjudication Formal Methods in Software Practice, August 2000.
BibTeX entry. Download PS.
[9] Karthikeyan Bhargavan, Carl A. Gunter, and Davor Obradovic. RIP in SPIN/HOL, Theorem Proving and Higher Order Logics, August 2000.
BibTeX entry. Download PS.
[10] Davor Obradovic and Elsa Gunter. Towards the Integration of Model Checking and Theorem Proving: Embedding a Subset of Promela into HOL, Category B paper, Theorem Proving and Higher Order Logics, August 2000.
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. Download PS.

Complete List

Links