The Village Telephone System: A Case Study in Formal Software Engineering. - Karthikeyan Bhargavan; Carl A. Gunter; Elsa L. Gunter; Michael Jackson 001; Davor Obradovic; Pamela Zave (TPHOLs, 1998)

Fault origin adjudication. - Karthikeyan Bhargavan; Carl A. Gunter; Davor Obradovic (FMSP, 2000)

Routing Information Protocol in HOL/SPIN. - Karthikeyan Bhargavan; Carl A. Gunter; Davor Obradovic (TPHOLs, 2000)

Real-time Model and Convergence Time of BGP. - Davor Obradovic (INFOCOM, 2002)

Formal verification of standards for distance vector routing protocols. - Karthikeyan Bhargavan; Davor Obradovic; Carl A. Gunter (J. ACM, 2002)

Verisim: Formal Analysis of Network Simulations. - Karthikeyan Bhargavan; Carl A. Gunter; Moonjoo Kim 001; Insup Lee 001; Davor Obradovic; Oleg Sokolsky; Mahesh Viswanathan 001 (IEEE Trans. Software Eng., 2002)