{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/42200"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/42200","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Symbolic reachability analysis for rewrite theories","abstract":"This dissertation presents a significant step forward in automatic and semi-automatic reasoning for reachability properties of rewriting logic specifications, a major research goal in the current state of the art. In particular, this work develops deductive techniques for reasoning symbolically about specifications with initial model semantics, including: (i) new constructor-based notions for reachability analysis, (ii) a proof system for the task of proving safety properties, and (iii) a novel method for symbolic reachability analysis of rewrite theories with constrained built-ins. These three new techniques are not just theoretical developments: each of them has been implemented in freely available tools for the automated reasoning presented in this thesis and are validated through case studies. These case studies include: (i) a reliable communication protocol, (ii) a secure-by-design browser system, and (iii) a NASA language for robotic machines. One main characteristic of the methods developed in this dissertation is that they are suitable for wide classes of rewrite theories and are highly generic, so that they can be used over many different instance languages and application domains.","abstract_html":"This dissertation presents a significant step forward in automatic and semi-automatic reasoning for reachability properties of rewriting logic specifications, a major research goal in the current state of the art. In particular, this work develops deductive techniques for reasoning symbolically about specifications with initial model semantics, including: (i) new constructor-based notions for reachability analysis, (ii) a proof system for the task of proving safety properties, and (iii) a novel method for symbolic reachability analysis of rewrite theories with constrained built-ins. These three new techniques are not just theoretical developments: each of them has been implemented in freely available tools for the automated reasoning presented in this thesis and are validated through case studies. These case studies include: (i) a reliable communication protocol, (ii) a secure-by-design browser system, and (iii) a NASA language for robotic machines. One main characteristic of the methods developed in this dissertation is that they are suitable for wide classes of rewrite theories and are highly generic, so that they can be used over many different instance languages and application domains.","abstract_has_math":false,"creators":["Rocha, Camilo"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","Roşu, Grigore","Viswanathan, Mahesh","Futatsugi, Kokichi","Munoz, Cesar A."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2013,"date_issued":"2013-02-03T19:27:41Z","date_published":"2013-02-03T19:27:41Z","updated_at":"2026-07-22T22:25:33Z","subjects":["rewriting logic","symbolic reachability analysis","deadlock freedom","inductive invariants","constrained rewriting","theorem proving","propositional tree automata","smt solving"],"languages":["en"],"rights":["All rights reserved - 2012 - Hernan Camilo Rocha Nino"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/42200","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","Roşu, Grigore","Viswanathan, Mahesh","Futatsugi, Kokichi","Munoz, Cesar A."]},{"key":"dc:creator","label":"Author","values":["Rocha, Camilo"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2013-02-03T19:27:41Z","2012-12"]},{"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":["rewriting logic","symbolic reachability analysis","deadlock freedom","inductive invariants","constrained rewriting","theorem proving","propositional tree automata","smt solving"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["All rights reserved - 2012 - Hernan Camilo Rocha Nino"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/42200"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This dissertation presents a significant step forward in automatic and semi-automatic reasoning for reachability properties of rewriting logic specifications, a major research goal in the current state of the art. In particular, this work develops deductive techniques for reasoning symbolically about specifications with initial model semantics, including: (i) new constructor-based notions for reachability analysis, (ii) a proof system for the task of proving safety properties, and (iii) a novel method for symbolic reachability analysis of rewrite theories with constrained built-ins. These three new techniques are not just theoretical developments: each of them has been implemented in freely available tools for the automated reasoning presented in this thesis and are validated through case studies. These case studies include: (i) a reliable communication protocol, (ii) a secure-by-design browser system, and (iii) a NASA language for robotic machines. One main characteristic of the methods developed in this dissertation is that they are suitable for wide classes of rewrite theories and are highly generic, so that they can be used over many different instance languages and application domains.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-11-28T19:30:29Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 3 main.pdf: 1560759 bytes, checksum: 3390168a093d6d23295c9c1c2094f682 (MD5) RochaNino_Hernan.zip: 2556370 bytes, checksum: 6193f3363685565ecc6223cbad5a57d0 (MD5) RochaNino_Hernan.pdf: 1560759 bytes, checksum: 3390168a093d6d23295c9c1c2094f682 (MD5)","Made available in DSpace on 2013-02-03T19:27:41Z (GMT). No. of bitstreams: 3 Hernan_Rocha Nino.pdf: 1560759 bytes, checksum: 3390168a093d6d23295c9c1c2094f682 (MD5) RochaNino_Hernan.zip: 2556370 bytes, checksum: 6193f3363685565ecc6223cbad5a57d0 (MD5) license.txt: 4067 bytes, checksum: a2dbe436a5a93aa9a0b34818542a74bf (MD5)"]},{"key":"dc:title","label":"Title","values":["Symbolic reachability analysis for rewrite theories"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","Roşu, Grigore","Viswanathan, Mahesh","Futatsugi, Kokichi","Munoz, Cesar A."],"dc:creator":["Rocha, Camilo"],"dc:date":["2013-02-03T19:27:41Z","2012-12"],"dc:description":["This dissertation presents a significant step forward in automatic and semi-automatic reasoning for reachability properties of rewriting logic specifications, a major research goal in the current state of the art. In particular, this work develops deductive techniques for reasoning symbolically about specifications with initial model semantics, including: (i) new constructor-based notions for reachability analysis, (ii) a proof system for the task of proving safety properties, and (iii) a novel method for symbolic reachability analysis of rewrite theories with constrained built-ins. These three new techniques are not just theoretical developments: each of them has been implemented in freely available tools for the automated reasoning presented in this thesis and are validated through case studies. These case studies include: (i) a reliable communication protocol, (ii) a secure-by-design browser system, and (iii) a NASA language for robotic machines. One main characteristic of the methods developed in this dissertation is that they are suitable for wide classes of rewrite theories and are highly generic, so that they can be used over many different instance languages and application domains.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-11-28T19:30:29Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 3 main.pdf: 1560759 bytes, checksum: 3390168a093d6d23295c9c1c2094f682 (MD5) RochaNino_Hernan.zip: 2556370 bytes, checksum: 6193f3363685565ecc6223cbad5a57d0 (MD5) RochaNino_Hernan.pdf: 1560759 bytes, checksum: 3390168a093d6d23295c9c1c2094f682 (MD5)","Made available in DSpace on 2013-02-03T19:27:41Z (GMT). No. of bitstreams: 3 Hernan_Rocha Nino.pdf: 1560759 bytes, checksum: 3390168a093d6d23295c9c1c2094f682 (MD5) RochaNino_Hernan.zip: 2556370 bytes, checksum: 6193f3363685565ecc6223cbad5a57d0 (MD5) license.txt: 4067 bytes, checksum: a2dbe436a5a93aa9a0b34818542a74bf (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/42200"],"dc:language":["en"],"dc:rights":["All rights reserved - 2012 - Hernan Camilo Rocha Nino"],"dc:subject":["rewriting logic","symbolic reachability analysis","deadlock freedom","inductive invariants","constrained rewriting","theorem proving","propositional tree automata","smt solving"],"dc:title":["Symbolic reachability analysis for rewrite theories"],"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:33Z"}