{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/100599"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/100599","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Efficient and proven verification of unreliable hardware executions of classic algorithms","abstract":"Lowering voltage and frequency guardbands of CPU, DRAM, cache, or interconnect lowers power and latency, but increases the risk of silent data corruptions in even formally verified hardware and software. Researchers have been developing systems that use unreliable hardware, combined with software checkers executed on reliable hardware, to gain high performance with no risk. Deterministic checkers for many important algorithms are asymptotically and practically more efficient than the original problem solvers, e.g. for systems of linear equations, satisfiability, linear programming, sorting, 3SUM, graph matching and others. Writing a correct checker is hard, since often intricate corner cases get overlooked. Our system, SOUNDCHECK, helps reduce burden on programmers by automatically proving soundness and completeness of checkers with bounded verification in the Sketch program synthesis language. Verified checkers are emitted as efficient C++ code and shown to have low overhead which results in a net performance improvement with no risk.","abstract_html":"Lowering voltage and frequency guardbands of CPU, DRAM, cache, or interconnect lowers power and latency, but increases the risk of silent data corruptions in even formally verified hardware and software. Researchers have been developing systems that use unreliable hardware, combined with software checkers executed on reliable hardware, to gain high performance with no risk. Deterministic checkers for many important algorithms are asymptotically and practically more efficient than the original problem solvers, e.g. for systems of linear equations, satisfiability, linear programming, sorting, 3SUM, graph matching and others. Writing a correct checker is hard, since often intricate corner cases get overlooked. Our system, SOUNDCHECK, helps reduce burden on programmers by automatically proving soundness and completeness of checkers with bounded verification in the Sketch program synthesis language. Verified checkers are emitted as efficient C++ code and shown to have low overhead which results in a net performance improvement with no risk.","abstract_has_math":false,"creators":["Gyurova, Yoana G"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.","school":null,"contributors":[],"advisors":["Saman Amarasinghe."],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015","date_published":"2015","updated_at":"2026-07-22T22:21:36Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/100599","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Saman Amarasinghe."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Gyurova, Yoana G"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2016-01-04T19:57:26Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2016-01-04T19:57:26Z"]},{"key":"dc:date.issued","label":"Date","values":["2015"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/100599"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 59-61)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Lowering voltage and frequency guardbands of CPU, DRAM, cache, or interconnect lowers power and latency, but increases the risk of silent data corruptions in even formally verified hardware and software. Researchers have been developing systems that use unreliable hardware, combined with software checkers executed on reliable hardware, to gain high performance with no risk. Deterministic checkers for many important algorithms are asymptotically and practically more efficient than the original problem solvers, e.g. for systems of linear equations, satisfiability, linear programming, sorting, 3SUM, graph matching and others. Writing a correct checker is hard, since often intricate corner cases get overlooked. Our system, SOUNDCHECK, helps reduce burden on programmers by automatically proving soundness and completeness of checkers with bounded verification in the Sketch program synthesis language. Verified checkers are emitted as efficient C++ code and shown to have low overhead which results in a net performance improvement with no risk."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Efficient and proven verification of unreliable hardware executions of classic algorithms"]}]}],"canonical_facts":{"dc:contributor.advisor":["Saman Amarasinghe."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Gyurova, Yoana G"],"dc:date.accessioned":["2016-01-04T19:57:26Z"],"dc:date.available":["2016-01-04T19:57:26Z"],"dc:date.issued":["2015"],"dc:description":["Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2015.","This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 59-61)."],"dc:description.abstract":["Lowering voltage and frequency guardbands of CPU, DRAM, cache, or interconnect lowers power and latency, but increases the risk of silent data corruptions in even formally verified hardware and software. Researchers have been developing systems that use unreliable hardware, combined with software checkers executed on reliable hardware, to gain high performance with no risk. Deterministic checkers for many important algorithms are asymptotically and practically more efficient than the original problem solvers, e.g. for systems of linear equations, satisfiability, linear programming, sorting, 3SUM, graph matching and others. Writing a correct checker is hard, since often intricate corner cases get overlooked. Our system, SOUNDCHECK, helps reduce burden on programmers by automatically proving soundness and completeness of checkers with bounded verification in the Sketch program synthesis language. Verified checkers are emitted as efficient C++ code and shown to have low overhead which results in a net performance improvement with no risk."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/100599"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Efficient and proven verification of unreliable hardware executions of classic algorithms"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:21:36Z"}