{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/45526"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/45526","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Building abstractions for fast, secure, reliable computer systems","abstract":"Modern computer systems play important roles in our society and everyday lives. Their performance, security and reliability are of critical importance. Real-world computer systems, however, occasionally suffer from performance degradation, security exploits, and poor reliability, because of the lack of efficient automatic analyses. This dissertation introduces a new methodology for building efficient automatic analyses for real-world computer systems through identifying and designing proper abstractions. It demonstrates the methodology within the context of three real-world computer systems: detecting net- work defects at the data plane level, exploiting data parallelism in web pages, and formally verifying security invariants in operating system kernels. This dissertation presents the design, implementation, and evaluation of the above systems, and shows that choosing the proper set of abstractions is an essential step to constructing efficient automatic analyses for real-world computer systems. Moreover, these analyses can become valuable tools to improve the performance, security and reliability of computer systems.","abstract_html":"Modern computer systems play important roles in our society and everyday lives. Their performance, security and reliability are of critical importance. Real-world computer systems, however, occasionally suffer from performance degradation, security exploits, and poor reliability, because of the lack of efficient automatic analyses. This dissertation introduces a new methodology for building efficient automatic analyses for real-world computer systems through identifying and designing proper abstractions. It demonstrates the methodology within the context of three real-world computer systems: detecting net- work defects at the data plane level, exploiting data parallelism in web pages, and formally verifying security invariants in operating system kernels. This dissertation presents the design, implementation, and evaluation of the above systems, and shows that choosing the proper set of abstractions is an essential step to constructing efficient automatic analyses for real-world computer systems. Moreover, these analyses can become valuable tools to improve the performance, security and reliability of computer systems.","abstract_has_math":false,"creators":["Mai, Haohui"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["King, Samuel T.","Godfrey, Philip B.","Caesar, Matthew C.","Zeldovich, Nickolai"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2013,"date_issued":"2013-08-22T16:43:11Z","date_published":"2013-08-22T16:43:11Z","updated_at":"2026-07-22T22:25:36Z","subjects":["computer system","data plane analysis","network troubleshooting","Boolean satisfiability","parallel Web browser","Web page decomposition","multi core","mobile security","microkernel","programming by contracts","automatic theorem proving"],"languages":["en"],"rights":["Copyright 2013 Haohui Mai"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/45526","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["King, Samuel T.","Godfrey, Philip B.","Caesar, Matthew C.","Zeldovich, Nickolai"]},{"key":"dc:creator","label":"Author","values":["Mai, Haohui"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2013-08-22T16:43:11Z","2013-08"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer system","data plane analysis","network troubleshooting","Boolean satisfiability","parallel Web browser","Web page decomposition","multi core","mobile security","microkernel","programming by contracts","automatic theorem proving"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2013 Haohui Mai"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/45526"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Modern computer systems play important roles in our society and everyday lives. Their performance, security and reliability are of critical importance. Real-world computer systems, however, occasionally suffer from performance degradation, security exploits, and poor reliability, because of the lack of efficient automatic analyses. This dissertation introduces a new methodology for building efficient automatic analyses for real-world computer systems through identifying and designing proper abstractions. It demonstrates the methodology within the context of three real-world computer systems: detecting net- work defects at the data plane level, exploiting data parallelism in web pages, and formally verifying security invariants in operating system kernels. This dissertation presents the design, implementation, and evaluation of the above systems, and shows that choosing the proper set of abstractions is an essential step to constructing efficient automatic analyses for real-world computer systems. Moreover, these analyses can become valuable tools to improve the performance, security and reliability of computer systems.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2013-07-06T16:45:57Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Mai_Haohui.pdf: 1610289 bytes, checksum: 608bbe1600d996edfbb1b44eaa499b4c (MD5)","Made available in DSpace on 2013-08-22T16:43:11Z (GMT). No. of bitstreams: 2 Haohui_Mai.pdf: 1610285 bytes, checksum: a93efcebc0b96eeab509e94f06b2daa2 (MD5) license.txt: 4056 bytes, checksum: 1b59da9d7083c81be01ec5b074792a78 (MD5)"]},{"key":"dc:title","label":"Title","values":["Building abstractions for fast, secure, reliable computer systems"]}]}],"canonical_facts":{"dc:contributor":["King, Samuel T.","Godfrey, Philip B.","Caesar, Matthew C.","Zeldovich, Nickolai"],"dc:creator":["Mai, Haohui"],"dc:date":["2013-08-22T16:43:11Z","2013-08"],"dc:description":["Modern computer systems play important roles in our society and everyday lives. Their performance, security and reliability are of critical importance. Real-world computer systems, however, occasionally suffer from performance degradation, security exploits, and poor reliability, because of the lack of efficient automatic analyses. This dissertation introduces a new methodology for building efficient automatic analyses for real-world computer systems through identifying and designing proper abstractions. It demonstrates the methodology within the context of three real-world computer systems: detecting net- work defects at the data plane level, exploiting data parallelism in web pages, and formally verifying security invariants in operating system kernels. This dissertation presents the design, implementation, and evaluation of the above systems, and shows that choosing the proper set of abstractions is an essential step to constructing efficient automatic analyses for real-world computer systems. Moreover, these analyses can become valuable tools to improve the performance, security and reliability of computer systems.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2013-07-06T16:45:57Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Mai_Haohui.pdf: 1610289 bytes, checksum: 608bbe1600d996edfbb1b44eaa499b4c (MD5)","Made available in DSpace on 2013-08-22T16:43:11Z (GMT). No. of bitstreams: 2 Haohui_Mai.pdf: 1610285 bytes, checksum: a93efcebc0b96eeab509e94f06b2daa2 (MD5) license.txt: 4056 bytes, checksum: 1b59da9d7083c81be01ec5b074792a78 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/45526"],"dc:language":["en"],"dc:rights":["Copyright 2013 Haohui Mai"],"dc:subject":["computer system","data plane analysis","network troubleshooting","Boolean satisfiability","parallel Web browser","Web page decomposition","multi core","mobile security","microkernel","programming by contracts","automatic theorem proving"],"dc:title":["Building abstractions for fast, secure, reliable computer systems"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:36Z"}