{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:51:36Z","timestamp":1764053496548,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":29,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,5,7]],"date-time":"2017-05-07T00:00:00Z","timestamp":1494115200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Intel Inc."},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["321174-VSSC"],"award-info":[{"award-number":["321174-VSSC"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,5,7]]},"DOI":"10.1145\/3102980.3102986","type":"proceedings-article","created":{"date-parts":[[2017,7,20]],"date-time":"2017-07-20T17:51:38Z","timestamp":1500573098000},"page":"30-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Verification in the Age of Microservices"],"prefix":"10.1145","author":[{"given":"Aurojit","family":"Panda","sequence":"first","affiliation":[{"name":"UC Berkeley"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University"}]},{"given":"Scott","family":"Shenker","sequence":"additional","affiliation":[{"name":"UC Berkeley and ICSI"}]}],"member":"320","published-online":{"date-parts":[[2017,5,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/945445.945454"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2909480"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2890784"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596574"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_8_1","volume-title":"NSDI","author":"Fonseca R.","year":"2007","unstructured":"Fonseca , R. , Porter , G. , Katz , R. H. , Shenker , S. , and Stoica , I . X-trace: A pervasive network tracing framework . In NSDI ( 2007 ). Fonseca, R., Porter, G., Katz, R. H., Shenker, S., and Stoica, I. X-trace: A pervasive network tracing framework. In NSDI (2007)."},{"key":"e_1_3_2_1_9_1","volume-title":"CONCUR","author":"Gavran I.","year":"2015","unstructured":"Gavran , I. , Niksic , F. , Kanade , A. , Majumdar , R. , and Vafeiadis , V . Rely\/guarantee reasoning for asynchronous programs . In CONCUR ( 2015 ). Gavran, I., Niksic, F., Kanade, A., Majumdar, R., and Vafeiadis, V. Rely\/guarantee reasoning for asynchronous programs. In CONCUR (2015)."},{"key":"e_1_3_2_1_10_1","unstructured":"GRPC\n  : A high performance open-source universal RPC framework. https:\/\/grpc.io retrieved 01\/21\/2017.  GRPC: A high performance open-source universal RPC framework. https:\/\/grpc.io retrieved 01\/21\/2017."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_13_1","volume-title":"NSDI","author":"Jamshed M. A.","year":"2017","unstructured":"Jamshed , M. A. , Moon , Y. , Kim , D. , Han , D. , and Park , K . mOS: A Reusable Networking Stack for Flow Monitoring Middleboxes . In NSDI ( 2017 ). Jamshed, M. A., Moon, Y., Kim, D., Han, D., and Park, K. mOS: A Reusable Networking Stack for Flow Monitoring Middleboxes. In NSDI (2017)."},{"key":"e_1_3_2_1_14_1","volume-title":"IFIP Congress","author":"Jones C. B.","year":"1983","unstructured":"Jones , C. B. Specification and design of (parallel) programs . In IFIP Congress ( 1983 ). Jones, C. B. Specification and design of (parallel) programs. In IFIP Congress (1983)."},{"key":"e_1_3_2_1_15_1","volume-title":"NSDI","author":"Koponen T.","year":"2014","unstructured":"Koponen , T. , Amidon , K. , Balland , P. , Casado , M. , Chanda , A. , Fulton , B. , Ganichev , I. , Gross , J. , Ingram , P. , Jackson , E. J. , Lambeth , A. , Lenglet , R. , Li , S.-H. , Padmanabhan , A. , Pettit , J. , Pfaff , B. , Ramanathan , R. , Shenker , S. , Shieh , A. , Stribling , J. , Thakkar , P. , Wendlandt , D. , Yip , A. , and Zhang , R . Network virtualization in multi-tenant datacenters . In NSDI ( 2014 ). Koponen, T., Amidon, K., Balland, P., Casado, M., Chanda, A., Fulton, B., Ganichev, I., Gross, J., Ingram, P., Jackson, E. J., Lambeth, A., Lenglet, R., Li, S.-H., Padmanabhan, A., Pettit, J., Pfaff, B., Ramanathan, R., Shenker, S., Shieh, A., Stribling, J., Thakkar, P., Wendlandt, D., Yip, A., and Zhang, R. Network virtualization in multi-tenant datacenters. In NSDI (2014)."},{"key":"e_1_3_2_1_16_1","unstructured":"Linux Foundation. networking:bridge. https:\/\/wiki.linuxfoundation.org\/networking\/bridge retrieved 01\/22\/2017.  Linux Foundation. networking:bridge. https:\/\/wiki.linuxfoundation.org\/networking\/bridge retrieved 01\/22\/2017."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_14"},{"key":"e_1_3_2_1_18_1","volume-title":"LogiCal Project","author":"The","year":"2004","unstructured":"The Coq development team. The Coq proof assistant reference manual . LogiCal Project , 2004 . Version 8.0. The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(99)00112-7"},{"key":"e_1_3_2_1_20_1","volume-title":"NSDI","author":"Pfaff B.","year":"2015","unstructured":"Pfaff , B. , Pettit , J. , Koponen , T. , Jackson , E. J. , Zhou , A. , Rajahalme , J. , Gross , J. , Wang , A. , Stringer , J. , Shelar , P. , Amidon , K. , and Casado , M . The design and implementation of open vswitch . In NSDI ( 2015 ). Pfaff, B., Pettit, J., Koponen, T., Jackson, E. J., Zhou, A., Rajahalme, J., Gross, J., Wang, A., Stringer, J., Shelar, P., Amidon, K., and Casado, M. The design and implementation of open vswitch. In NSDI (2015)."},{"key":"e_1_3_2_1_21_1","unstructured":"redis.io. How fast is Redis? https:\/\/redis.io\/topics\/benchmarks retrieved 01\/22\/2017.  redis.io. How fast is Redis? https:\/\/redis.io\/topics\/benchmarks retrieved 01\/22\/2017."},{"key":"e_1_3_2_1_22_1","volume-title":"NSDI","author":"Scott C.","year":"2016","unstructured":"Scott , C. , Panda , A. , Brajkovic , V. , Necula , G. , Krishnamurthy , A. , and Shenker , S . Minimizing Faulty Executions of Distributed Systems . In NSDI ( 2016 ). Scott, C., Panda, A., Brajkovic, V., Necula, G., Krishnamurthy, A., and Shenker, S. Minimizing Faulty Executions of Distributed Systems. In NSDI (2016)."},{"key":"e_1_3_2_1_23_1","volume-title":"Google","author":"Sigelman B. H.","year":"2010","unstructured":"Sigelman , B. H. , Barroso , L. A. , Burrows , M. , Stephenson , P. , Plakal , M. , Beaver , D. , Jaspan , S. , and Shanbhag , C . Dapper, a large-scale distributed systems tracing infrastructure. Tech. rep ., Google , Inc ., 2010 . Sigelman, B. H., Barroso, L. A., Burrows, M., Stephenson, P., Plakal, M., Beaver, D., Jaspan, S., and Shanbhag, C. Dapper, a large-scale distributed systems tracing infrastructure. Tech. rep., Google, Inc., 2010."},{"key":"e_1_3_2_1_24_1","volume-title":"OSDI","author":"Sigurbjarnarson H.","year":"2016","unstructured":"Sigurbjarnarson , H. , Bornholt , J. , Torlak , E. , and Wang , X . Push-button verification of file systems via crash refinement . In OSDI ( 2016 ). Sigurbjarnarson, H., Bornholt, J., Torlak, E., and Wang, X. Push-button verification of file systems via crash refinement. In OSDI (2016)."},{"key":"e_1_3_2_1_25_1","volume-title":"USENIX Conference","author":"Steiner J. G.","year":"1988","unstructured":"Steiner , J. G. , Neuman , C. , and Schiller , J. I . Kerberos: An authentication service for open network systems . In USENIX Conference ( 1988 ). Steiner, J. G., Neuman, C., and Schiller, J. I. Kerberos: An authentication service for open network systems. In USENIX Conference (1988)."},{"key":"e_1_3_2_1_26_1","unstructured":"Apache Thrift. https:\/\/thrift.apache.org\/ retrieved 01\/21\/2017.  Apache Thrift. https:\/\/thrift.apache.org\/ retrieved 01\/21\/2017."},{"key":"e_1_3_2_1_27_1","unstructured":"Todd Hoff. Lessons Learned From Scaling Uber To 2000 Engineers 1000 Services And 8000 Git Repositories. https:\/\/goo.gl\/1MRvoT retrieved 01\/21\/2017.  Todd Hoff. Lessons Learned From Scaling Uber To 2000 Engineers 1000 Services And 8000 Git Repositories. https:\/\/goo.gl\/1MRvoT retrieved 01\/21\/2017."},{"key":"e_1_3_2_1_28_1","unstructured":"Tony Mauro. Adopting Microservices at Netflix: Lessons for Architectural Design. https:\/\/goo.gl\/DyrtvI retrieved 01\/21\/2017.  Tony Mauro. Adopting Microservices at Netflix: Lessons for Architectural Design. https:\/\/goo.gl\/DyrtvI retrieved 01\/21\/2017."},{"key":"e_1_3_2_1_29_1","unstructured":"What is VPP? https:\/\/wiki.fd.io\/view\/VPP\/What_is_VPP%3F retreived 01\/21\/2017.  What is VPP? https:\/\/wiki.fd.io\/view\/VPP\/What_is_VPP%3F retreived 01\/21\/2017."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"event":{"name":"HotOS '17: Workshop on Hot Topics in Operating Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Whistler BC Canada","acronym":"HotOS '17"},"container-title":["Proceedings of the 16th Workshop on Hot Topics in Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3102980.3102986","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3102980.3102986","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:37:06Z","timestamp":1750217826000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3102980.3102986"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,7]]},"references-count":29,"alternative-id":["10.1145\/3102980.3102986","10.1145\/3102980"],"URL":"https:\/\/doi.org\/10.1145\/3102980.3102986","relation":{},"subject":[],"published":{"date-parts":[[2017,5,7]]},"assertion":[{"value":"2017-05-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}