@inProceedings{
 title = {A Theorem Proving Approach Towards Declarative Networking},
 type = {inProceedings},
 year = {2009},
 websites = {http://www.cis.upenn.edu/~boonloo/papers/formaldn_tphol09.pdf},
 city = {Munich, Germany},
 id = {337280a6-40e0-3e8c-a2a0-44907718d67a},
 created = {2011-04-01T15:33:17.000Z},
 file_attached = {true},
 profile_id = {2834d4fc-14a3-3cd2-ad99-1eef34b88927},
 group_id = {d14f7e13-b2b1-3278-8a95-a430f57d0ad3},
 last_modified = {2016-02-29T21:21:39.000Z},
 read = {false},
 starred = {false},
 authored = {false},
 confirmed = {true},
 hidden = {false},
 citation_key = {Wang2009},
 abstract = {We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative net- working, a recent innovation that enables network protocols to be con- cisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Net- work Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, net- work designer can supply a component-based model of their routing de- sign, automatically generate PVS specifications for verification and sub- sequent compilation into verified declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying a variety of well-known network routing protocols.},
 bibtype = {inProceedings},
 author = {Wang, Anduo and Loo, Boon Thau and Liu, Changbin and Sokolsky, Oleg and Basu, Prithwish},
 booktitle = {22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs) emerging trends proceedings}
}

{"_id":"JRdRn9E2awpubxc8e","bibbaseid":"wang-loo-liu-sokolsky-basu-atheoremprovingapproachtowardsdeclarativenetworking-2009","downloads":0,"creationDate":"2016-08-26T19:08:51.129Z","title":"A Theorem Proving Approach Towards Declarative Networking","author_short":["Wang, A.","Loo, B., T.","Liu, C.","Sokolsky, O.","Basu, P."],"year":2009,"bibtype":"inProceedings","biburl":null,"bibdata":{"title":"A Theorem Proving Approach Towards Declarative Networking","type":"inProceedings","year":"2009","websites":"http://www.cis.upenn.edu/~boonloo/papers/formaldn_tphol09.pdf","city":"Munich, Germany","id":"337280a6-40e0-3e8c-a2a0-44907718d67a","created":"2011-04-01T15:33:17.000Z","file_attached":"true","profile_id":"2834d4fc-14a3-3cd2-ad99-1eef34b88927","group_id":"d14f7e13-b2b1-3278-8a95-a430f57d0ad3","last_modified":"2016-02-29T21:21:39.000Z","read":false,"starred":false,"authored":false,"confirmed":"true","hidden":false,"citation_key":"Wang2009","abstract":"We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative net- working, a recent innovation that enables network protocols to be con- cisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Net- work Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, net- work designer can supply a component-based model of their routing de- sign, automatically generate PVS specifications for verification and sub- sequent compilation into verified declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying a variety of well-known network routing protocols.","bibtype":"inProceedings","author":"Wang, Anduo and Loo, Boon Thau and Liu, Changbin and Sokolsky, Oleg and Basu, Prithwish","booktitle":"22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs) emerging trends proceedings","bibtex":"@inProceedings{\n title = {A Theorem Proving Approach Towards Declarative Networking},\n type = {inProceedings},\n year = {2009},\n websites = {http://www.cis.upenn.edu/~boonloo/papers/formaldn_tphol09.pdf},\n city = {Munich, Germany},\n id = {337280a6-40e0-3e8c-a2a0-44907718d67a},\n created = {2011-04-01T15:33:17.000Z},\n file_attached = {true},\n profile_id = {2834d4fc-14a3-3cd2-ad99-1eef34b88927},\n group_id = {d14f7e13-b2b1-3278-8a95-a430f57d0ad3},\n last_modified = {2016-02-29T21:21:39.000Z},\n read = {false},\n starred = {false},\n authored = {false},\n confirmed = {true},\n hidden = {false},\n citation_key = {Wang2009},\n abstract = {We present the DRIVER system for designing, analyzing and implementing network protocols. DRIVER leverages declarative net- working, a recent innovation that enables network protocols to be con- cisely specified and implemented using declarative languages. DRIVER takes as input declarative networking specifications written in the Net- work Datalog (NDlog) query language, and maps that automatically into logical specifications that can be directly used in existing theorem provers to validate protocol correctness. As an alternative approach, net- work designer can supply a component-based model of their routing de- sign, automatically generate PVS specifications for verification and sub- sequent compilation into verified declarative network implementations. We demonstrate the use of DRIVER for synthesizing and verifying a variety of well-known network routing protocols.},\n bibtype = {inProceedings},\n author = {Wang, Anduo and Loo, Boon Thau and Liu, Changbin and Sokolsky, Oleg and Basu, Prithwish},\n booktitle = {22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs) emerging trends proceedings}\n}","author_short":["Wang, A.","Loo, B., T.","Liu, C.","Sokolsky, O.","Basu, P."],"urls":{"Paper":"http://bibbase.org/service/mendeley/2a5aa585-ad83-3b8c-9373-0fad35bf58e0/file/4ee118e4-f399-2691-1b80-cc5de502e33c/2009-A_Theorem_Proving_Approach_Towards_Declarative_Networking.pdf.pdf","Website":"http://www.cis.upenn.edu/~boonloo/papers/formaldn_tphol09.pdf"},"bibbaseid":"wang-loo-liu-sokolsky-basu-atheoremprovingapproachtowardsdeclarativenetworking-2009","role":"author","downloads":0},"search_terms":["theorem","proving","approach","towards","declarative","networking","wang","loo","liu","sokolsky","basu"],"keywords":[],"authorIDs":[]}