Rewriting-based symbolic methods for distributed system verification

rewriting logic;verification;reachability logic

Skeirik, Stephen

关键词: rewriting logic;    verification;    reachability logic;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/106224/SKEIRIK-DISSERTATION-2019.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

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.