Rewriting-based symbolic methods for distributed system verification

As computer system complexity increases, new methods and logics are needed to scale up to the complexity of practical systems without sacrificing logical precision and ease of specification. To that end, the goal of this research project is to develop rewriting-based symbolic analysis methods that (1) can analyze systems which need an unbounded amount of time and/or space (2) may be highly distributed (3) use modular specification techniques so that work is never wasted (4) are generic across a possibly infinite number of domain theories. Towards this goal, we present our research on theory-generic satisfiability and rewrite-theory-generic specification and analysis methods, discuss prototype implementations, and consider future directions.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2020

Author dc:creator

• Skeirik, Stephen

Contributors dc:contributor

• Meseguer, José
• Agha, Gul
• Roșu, Grigore
• Ölveczky, Peter

• rewriting logic
• verification
• reachability logic

Statement dc:rights

• Copyright 2019 Stephen Skeirik

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/106224

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/106224