{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:02:32Z","timestamp":1760043752795,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["DGE-1256082"],"award-info":[{"award-number":["DGE-1256082"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006831","name":"USAF","doi-asserted-by":"crossref","award":["FA8750-15-C-0010"],"award-info":[{"award-number":["FA8750-15-C-0010"]}],"id":[{"id":"10.13039\/100006831","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100006602","name":"AFRL","doi-asserted-by":"crossref","award":["FA8750-16-2-0032"],"award-info":[{"award-number":["FA8750-16-2-0032"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Automated verification can ensure that a web page satisfies accessibility, usability, and design properties regardless of the end user's device, preferences, and assistive technologies. However, state-of-the-art verification tools for layout properties do not scale to large pages because they rely on whole-page analyses and must reason about the entire page using the complex semantics of the browser layout algorithm.<\/jats:p>\n          <jats:p>This paper introduces and formalizes modular layout proofs. A modular layout proof splits a monolithic verification problem into smaller verification problems, one for each component of a web page. Each component specification can use rely\/guarantee-style preconditions to make it verifiable independently of the rest of the page and enabling reuse across multiple pages. Modular layout proofs scale verification to pages an order of magnitude larger than those supported by previous approaches.<\/jats:p>\n          <jats:p>We prototyped these techniques in a new proof assistant, Troika. In Troika, a proof author partitions a page into components and writes specifications for them. Troika then verifies the specifications, and uses those specifications to verify whole-page properties. Troika also enables the proof author to verify different component specifications with different verification tools, leveraging the strengths of each. In a case study, we use Troika to verify a large web page and demonstrate a speed-up of 13--1469x over existing tools, taking verification time from hours to seconds. We develop a systematic approach to writing Troika proofs and demonstrate it on 8 proofs of properties from prior work to show that modular layout proofs are short, easy to write, and provide benefits over existing tools.<\/jats:p>","DOI":"10.1145\/3360577","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Modular verification of web page layout"],"prefix":"10.1145","volume":"3","author":[{"given":"Pavel","family":"Panchekha","sequence":"first","affiliation":[{"name":"University of Utah, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael D.","family":"Ernst","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoaib","family":"Kamil","sequence":"additional","affiliation":[{"name":"Adobe, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"volume-title":"Modular Verification for Computer Security. IEEE 29th Computer Security Foundations Symposium (CSF)","year":"2016","author":"Appel Andrew W.","key":"e_1_2_2_1_1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/320719.322588"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642918.2647357"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/266180.266361"},{"key":"e_1_2_2_6_1","unstructured":"Browserling. 2018. https:\/\/www.browserling.com\/  Browserling. 2018. https:\/\/www.browserling.com\/"},{"key":"e_1_2_2_7_1","unstructured":"Browsershots. 2018. http:\/\/browsershots.org\/  Browsershots. 2018. http:\/\/browsershots.org\/"},{"key":"e_1_2_2_8_1","unstructured":"Browserstack. 2018. https:\/\/www.browserstack.com\/screenshots  Browserstack. 2018. https:\/\/www.browserstack.com\/screenshots"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.97"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908103"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"volume-title":"Selenium 2 Testing Tools: Beginner\u2019s Guide","author":"David Burns","key":"e_1_2_2_13_1"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884012"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290379"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"volume-title":"Anthony Widjaja Lin, and Luke Ong","year":"2014","author":"Hague Matthew","key":"e_1_2_2_18_1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1983.1095720"},{"volume-title":"Verification and Validation (ICST), 2015 IEEE 8th International Conference on. IEEE, IEEE","year":"2015","author":"Hall\u00e9 Sylvain","key":"e_1_2_2_20_1"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/142621.142635"},{"key":"e_1_2_2_22_1","unstructured":"ITU. 2015. ITU releases 2015 ICT figure. http:\/\/www.itu.int\/net\/pressoffice\/press_releases\/2015\/17.aspx  ITU. 2015. ITU releases 2015 ICT figure. http:\/\/www.itu.int\/net\/pressoffice\/press_releases\/2015\/17.aspx"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. ACM 256\u2013269.  Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. ACM 256\u2013269.","DOI":"10.1145\/3022670.2951943"},{"volume-title":"Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. ACM, 637\u2013650.","year":"2015","author":"Jung Ralf","key":"e_1_2_2_24_1"},{"volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness (LPAR\u201910)","year":"2010","author":"Leino K. Rustan M.","key":"e_1_2_2_25_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2501988.2502006"},{"volume-title":"Automated Repair of Mobile Friendly Problems in Web Pages. In International Conference on Software Engineering (ICSE","year":"2018","author":"Mahajan Sonal","key":"e_1_2_2_28_1"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092726"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2018.00030"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1054972.1054979"},{"volume-title":"Extracting Client-side Web Application Code. In World Wide Web Conference","year":"2012","author":"Maras Josip","key":"e_1_2_2_32_1"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2648620"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985870"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1772690.1772763"},{"volume-title":"ESOP (LNCS)","author":"Nanevski Aleksandar","key":"e_1_2_2_36_1"},{"key":"e_1_2_2_37_1","unstructured":"National Federation for the Blind. 2016. Blindness Statistics. https:\/\/nfb.org\/blindness- statistics  National Federation for the Blind. 2016. Blindness Statistics. https:\/\/nfb.org\/blindness- statistics"},{"key":"e_1_2_2_38_1","unstructured":"Mark Otto and Jacob Thornton. 2015. Bootstrap: the world\u2019s most popular mobile-first and responsive front-end framework. http:\/\/getbootstrap.com\/  Mark Otto and Jacob Thornton. 2015. Bootstrap: the world\u2019s most popular mobile-first and responsive front-end framework. http:\/\/getbootstrap.com\/"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192407"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984010"},{"volume-title":"ESOP (LNCS)","author":"Raad Azalea","key":"e_1_2_2_41_1"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2010.5609723"},{"key":"e_1_2_2_43_1","unstructured":"Joel Spolsky. 2018. Joel on Software. https:\/\/joelonsoftware.com  Joel Spolsky. 2018. Joel on Software. https:\/\/joelonsoftware.com"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/646823.706907"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/800265.810742"},{"volume-title":"ESOP (LNCS)","author":"Svendsen Kasper","key":"e_1_2_2_46_1"},{"key":"e_1_2_2_47_1","unstructured":"Array Themes. 2018. https:\/\/arraythemes.com  Array Themes. 2018. https:\/\/arraythemes.com"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Aaron Turon Viktor Vafeiadis and Derek Dreyer. 2014. GPS: navigating weak memory with ghosts protocols and separation. In OOPSLA\u201914. ACM 691\u2013707.  Aaron Turon Viktor Vafeiadis and Derek Dreyer. 2014. GPS: navigating weak memory with ghosts protocols and separation. In OOPSLA\u201914. ACM 691\u2013707.","DOI":"10.1145\/2714064.2660243"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Aaron Joseph Turon Jacob Thamsborg Amal Ahmed Lars Birkedal and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL\u201913. ACM 343\u2013356.  Aaron Joseph Turon Jacob Thamsborg Amal Ahmed Lars Birkedal and Derek Dreyer. 2013. Logical relations for fine-grained concurrency. In POPL\u201913. ACM 343\u2013356.","DOI":"10.1145\/2480359.2429111"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/357299.357303"},{"key":"e_1_2_2_51_1","unstructured":"W3C. 2011. Cascading Style Sheets Level 2 Revision 1 (CSS 2.1) Specification. https:\/\/www.w3.org\/TR\/2011\/REC- CSS2-20110607\/  W3C. 2011. Cascading Style Sheets Level 2 Revision 1 (CSS 2.1) Specification. https:\/\/www.w3.org\/TR\/2011\/REC- CSS2-20110607\/"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092712"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.31"},{"volume-title":"The Grammar of Graphics (Statistics and Computing)","author":"Wilkinson Leland","key":"e_1_2_2_54_1"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/108844.109005"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360577","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360577","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360577"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":55,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360577"],"URL":"https:\/\/doi.org\/10.1145\/3360577","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}