Files in this item



application/pdfHernan_Rocha Nino.pdf (2MB)
(no description provided)PDF


Title:Symbolic reachability analysis for rewrite theories
Author(s):Rocha, Camilo
Director of Research:Meseguer, José
Doctoral Committee Chair(s):Meseguer, José
Doctoral Committee Member(s):Roşu, Grigore; Viswanathan, Mahesh; Futatsugi, Kokichi; Munoz, Cesar A.
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):rewriting logic
symbolic reachability analysis
deadlock freedom
inductive invariants
constrained rewriting
theorem proving
propositional tree automata
smt solving
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.
Issue Date:2013-02-03
Rights Information:All rights reserved - 2012 - Hernan Camilo Rocha Nino
Date Available in IDEALS:2013-02-03
Date Deposited:2012-12

This item appears in the following Collection(s)

Item Statistics