{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T18:12:27Z","timestamp":1757700747508,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540929949"},{"type":"electronic","value":"9783540929956"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-92995-6_5","type":"book-chapter","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T14:02:58Z","timestamp":1231509778000},"page":"61-75","source":"Crossref","is-referenced-by-count":20,"title":["Declarative Network Verification"],"prefix":"10.1007","author":[{"given":"Anduo","family":"Wang","sequence":"first","affiliation":[]},{"given":"Prithwish","family":"Basu","sequence":"additional","affiliation":[]},{"given":"Boon Thau","family":"Loo","sequence":"additional","affiliation":[]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"P2: Declarative Networking, http:\/\/p2.cs.berkeley.edu"},{"key":"5_CR2","unstructured":"Archer, M., Vito, B.D., Mu\u00f1oz, C.: Developing user strategies in PVS: A tutorial. In: STRATA 2003, NASA\/CP-2003-212448 (2003)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development. coq\u2019art: The calculus of inductive constructions (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"4","key":"5_CR4","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1145\/581771.581775","volume":"49","author":"K. Bhargavan","year":"2002","unstructured":"Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM\u00a049(4), 538\u2013576 (2002)","journal-title":"J. ACM"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Cardell-Oliver, R.: On the use of the hol system for protocol verification. In: TPHOLs, pp. 59\u201362 (1991)","DOI":"10.1109\/HOL.1991.596272"},{"key":"5_CR6","unstructured":"DNV use cases for protocol verification, http:\/\/www.seas.upenn.edu\/~anduo\/dnv.html"},{"key":"5_CR7","unstructured":"Engler, D., Musuvathi, M.: Model-checking large network protocol implementations. In: NSDI (2004)"},{"key":"5_CR8","unstructured":"Rodriguez, A., et al.: MACEDON: Methodology for Automatically Creating, Evaluating, and Designing Overlay Networks. In: NSDI (2004)"},{"key":"5_CR9","unstructured":"Feamster, N., Balakrishnan, H.: Correctness Properties for Internet Routing. In: Allerton Conference on Communication, Control, and Computing (2005)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028764","volume-title":"Computer Aided Verification","author":"A.P. Felty","year":"1998","unstructured":"Felty, A.P., Howe, D.J., Stomp, F.A.: Protocol verification in nuprl. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Griffin, T.G., Sobrinho, J.L.: Metarouting. In: ACM SIGCOMM (2005)","DOI":"10.1145\/1080091.1080094"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"FME \u201996: Industrial Benefit and Advances in Formal Methods","author":"K. Havelund","year":"1996","unstructured":"Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol.\u00a01051. Springer, Heidelberg (1996)"},{"key":"5_CR13","unstructured":"Killian, C., Anderson, J., Jhala, R., Vahdat, A.: Life, death, and the critical transition: Finding liveness bugs in systems code. In: NSDI (2007)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.M.: Mace: language support for building distributed systems. In: PLDI (2007)","DOI":"10.1145\/1250734.1250755"},{"key":"5_CR15","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: PDPTA (1999)"},{"key":"5_CR16","unstructured":"Liu, X., Guo, Z., Wang, X., Chen, F., Tang, X.L.J., Wu, M., Kaashoek, M.F., Zhang, Z.: D3S: Debugging Deployed Distributed Systems. In: NSDI (2008)"},{"key":"5_CR17","unstructured":"Loo, B.T.: The Design and Implementation of Declarative Networks (Ph.D. Dissertation). Technical Report UCB\/EECS-2006-177, UC Berkeley (2006)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Condie, T., Garofalakis, M., Gay, D.E., Hellerstein, J.M., Maniatis, P., Ramakrishnan, R., Roscoe, T., Stoica, I.: Declarative Networking: Language, Execution and Optimization. In: ACM SIGMOD (2006)","DOI":"10.1145\/1142473.1142485"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Condie, T., Hellerstein, J.M., Maniatis, P., Roscoe, T., Stoica, I.: Implementing Declarative Overlays. In: ACM SOSP (2005)","DOI":"10.1145\/1095810.1095818"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Loo, B.T., Hellerstein, J.M., Stoica, I., Ramakrishnan, R.: Declarative Routing: Extensible Routing with Declarative Queries. In: ACM SIGCOMM (2005)","DOI":"10.1145\/1080091.1080126"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"5_CR22","unstructured":"Owre, S., Shankar, N.: Writing PVS proof strategies. In: STRATA 2003 (2003)"},{"key":"5_CR23","volume-title":"Computer Networks: A Systems Approach","author":"L. Peterson","year":"2007","unstructured":"Peterson, L., Davie, B.: Computer Networks: A Systems Approach, 4th edn. Morgan Kaufmann, San Francisco (2007)","edition":"4"},{"key":"5_CR24","unstructured":"Peterson, L., Shenker, S., Turner, J.: Overcoming the Internet Impasse Through Virtualization. In: HotNets-III (2004)"},{"issue":"2","key":"5_CR25","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0743-1066(94)00039-9","volume":"23","author":"R. Ramakrishnan","year":"1993","unstructured":"Ramakrishnan, R., Ullman, J.D.: A Survey of Research on Deductive Database Systems. Journal of Logic Programming\u00a023(2), 125\u2013149 (1993)","journal-title":"Journal of Logic Programming"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Raman, S., McCanne, S.: A model, analysis, and protocol framework for soft state-based communication. In: SIGCOMM, pp. 15\u201325 (1999)","DOI":"10.1145\/316194.316202"},{"key":"5_CR27","unstructured":"Reynolds, P., Killian, C., Wiener, J.L., Mogul, J.C., Shah, M.A., Vahdat, A.: Pip: Detecting the Unexpected in Distributed Systems. In: NSDI (2006)"},{"issue":"2","key":"5_CR28","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Commun.\u00a015(2), 91\u2013110 (2002)","journal-title":"AI Commun."},{"key":"5_CR29","unstructured":"Rushby, J.: Specification, proof checking, and model checking for protocols and distributed systems with PVS. In: Tutorial FORTE X\/PSTV XVII 1997 (1997)"},{"key":"5_CR30","volume-title":"Foundations of Databases","author":"S. Abiteboul","year":"1995","unstructured":"Abiteboul, S., et al.: Foundations of Databases. Addison-Wesley, Reading (1995)"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Stoica, I., Morris, R., Karger, D., Kaashoek, M.F., Balakrishnan, H.: Chord: A Scalable P2P Lookup Service for Internet Applications. In: SIGCOMM (2001)","DOI":"10.1145\/383059.383071"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Wang, A., Basu, P., Loo, B.T., Sokolsky, O.: Declarative Network Verification. University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-CIS-08-34 (2008)","DOI":"10.1007\/978-3-540-92995-6_5"},{"key":"5_CR33","unstructured":"Yices, http:\/\/yices.csl.sri.com"},{"key":"5_CR34","unstructured":"Z3, http:\/\/research.microsoft.com\/projects\/Z3\/"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-92995-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T22:12:43Z","timestamp":1738879963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92995-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540929949","9783540929956"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92995-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}