{"id":{"repo_id":"buffalo","oai_identifier":"oai:ubir.buffalo.edu:10477/84058"},"canonical_url":"https://search.dev.ndltd.org/etd/buffalo/oai:ubir.buffalo.edu:10477/84058","repository":{"repo_id":"buffalo","name":"Buffalo","base_url":"https://ubir.buffalo.edu/oai/request"},"display":{"title":"Coupled Relational Symbolic Execution","abstract":"Ph.D.","abstract_html":"Ph.D.","abstract_has_math":false,"creators":["Farina, Gian Pietro; 0000-0001-7823-1536"],"institution":"State University of New York at Buffalo","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Gaboardi, Marco","Computer Science and Engineering"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-06-21T15:47:29Z","date_published":"2022-06-21T15:47:29Z","updated_at":"2026-07-27T19:05:30Z","subjects":["computer science"],"languages":["eng"],"rights":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/10477/84058","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gaboardi, Marco","Computer Science and Engineering"]},{"key":"dc:creator","label":"Author","values":["Farina, Gian Pietro; 0000-0001-7823-1536"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-06-21T15:47:29Z","2020"]},{"key":"dc:publisher","label":"Institution","values":["State University of New York at Buffalo"]},{"key":"dc:type","label":"Dc Type","values":["Text","Dissertation"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/10477/84058"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Ph.D.","The goal of this work is to lay down a theoretical foundation for the use of symbolic execution to verify and refute relational properties. Relational properties are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. Standard (unary) symbolic execution has already been used to verify and refute relational properties of programs. Usually, this is done by reducing the relational property to a unary one for a modified program. Relational symbolic execution instead relies on a relational semantics. It allows the user to reason about pairs of programs without the need to modify the program or the specification. The first part of this manuscript will show examples of deterministic relational properties, and strategies to reduce the set of possible setof states. The result, Relational Symbolic Execution, or RSE, is a sound and (relatively) complete verification (and refutation) system for relational deterministic properties. The second part of this manuscript will concern a specific relational probabilistic property: Differential privacy. Differential privacy is a gold standard for privacy in statistical analysis that can be satisfied by algorithms and hence programs.","**To request an accessible version of the file(s) associated with this item, contact library@buffalo.edu. Please include the item's persistent URL [http://hdl.handle.net/. . .] in your request.**"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Coupled Relational Symbolic Execution"]}]}],"canonical_facts":{"dc:contributor":["Gaboardi, Marco","Computer Science and Engineering"],"dc:creator":["Farina, Gian Pietro; 0000-0001-7823-1536"],"dc:date":["2022-06-21T15:47:29Z","2020"],"dc:description":["Ph.D.","The goal of this work is to lay down a theoretical foundation for the use of symbolic execution to verify and refute relational properties. Relational properties are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. Standard (unary) symbolic execution has already been used to verify and refute relational properties of programs. Usually, this is done by reducing the relational property to a unary one for a modified program. Relational symbolic execution instead relies on a relational semantics. It allows the user to reason about pairs of programs without the need to modify the program or the specification. The first part of this manuscript will show examples of deterministic relational properties, and strategies to reduce the set of possible setof states. The result, Relational Symbolic Execution, or RSE, is a sound and (relatively) complete verification (and refutation) system for relational deterministic properties. The second part of this manuscript will concern a specific relational probabilistic property: Differential privacy. Differential privacy is a gold standard for privacy in statistical analysis that can be satisfied by algorithms and hence programs.","**To request an accessible version of the file(s) associated with this item, contact library@buffalo.edu. Please include the item's persistent URL [http://hdl.handle.net/. . .] in your request.**"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/10477/84058"],"dc:language":["eng"],"dc:publisher":["State University of New York at Buffalo"],"dc:rights":["Users of works found in University at Buffalo Institutional Repository (UBIR) are responsible for identifying and contacting the copyright owner for permission to reuse. University at Buffalo Libraries do not manage rights for copyright-protected works and cannot assist with permissions.","Copyright retained by author."],"dc:subject":["computer science"],"dc:title":["Coupled Relational Symbolic Execution"],"dc:type":["Text","Dissertation"]},"updated_at":"2026-07-27T19:05:30Z"}