We aim to develop a scalable, mechanized infrastructure for certifying correct and secure execution of reactive routing system implementations through: a generic framework for modeling and specifying systems at a number of abstraction layers; a compositional methodology for mathematically analyzing such models; and developing a suite of tools and techniques to mechanize and automate such analysis within a unified logical foundation. Our research exploits ACL2's general-purpose reasoning engine while augmenting the tool suite with a streamlined modeling and specification methodology. We are developing a collection of targeted tools for verifying safety, liveness, and security properties of such systems while staying within a single logic and proof system.
To facilitate verification of correspondence between protocol layers, we are enhancing ACL2's reasoning engine with automated verification tools based on advances in BDD- and SAT-based techniques. For instance, the invention and proof of inductive invariants is one of the most time-consuming activities in reactive system verification. To address this, we are integrating into ACL2 a predicate abstraction mechnism and a general-purpose symbolic simulation capability; these techniques often obviate the expensive construction of single-step inductive invariants, by making judicious use of rewriting to "mine" effective predicates and applying symbolic simulation over a large number of computation steps to justify their invariance. The expected results will help automate the mechanical verification of reactive systems such as routers and CPSs.
We are also developing a program logic to facilitate reasoning about multiprocessor programs, under weak memory consistency guarantees. The memory model is based on the X86 multiprocessor memory model and the explicit goal is to facilitate reasoning about inherently racey multiprocessor programs (e.g., concurrent data structure updates).
 Any opinions, findings and conclusions or recomendations expressed in this material are those of the authors and do not necessarily reflect the views of the Defense Advanced Research Projects Agency or the National Science Foundation.