SHF: Small: Liveness Proofs at Scale

A liveness property states that, under certain assumptions about its input, a system eventually responds with a desired output. Liveness properties are crucial for the correctness of systems. If a system has a liveness error, it may suddenly become unavailable, resulting in loss of critical services or data. It may also be vulnerable to attack by malicious parties that wish to disrupt critical infrastructure. Nonetheless, after decades of research, logically proving the liveness of practical systems remains a challenge that is typically beyond the capability or time constraints of practicing engineers. The goal of this project is to address the fundamental problems that make liveness proofs difficult, create techniques and tools that are accessible to engineers, and allow proof at the scale and complexity of systems encountered in industry. The project's novelty is a new form of liveness proof that is conceptually simple enough to be applied by engineers and provides automated deduction methods that are sufficiently stable and reliable to be applied in industry at scale. The project's impacts are in enabling more rapid design exploration and iteration while preserving design correctness, contributing to industrial competitiveness, and establishing partnerships between academia and industry. The project will provide benefits to industry, defense and consumers by enabling the design of more trustworthy systems, with potential benefits for privacy, security and life safety. Technically, the project will explore a method based on the novel concept of "Relational Rankings". This approach satisfies two key criteria: (1) unlike liveness-to-safety proof approaches based on numerical rankings, it keeps the proof obligations within the range of effectively propositional reasoning (EPR), allowing reliable and scalable automated proof search, and (2) unlike dynamic liveness-to-safety proof approaches based on finite projections, it requires the engineer to reason only about the system state, and not the state of an opaque automated construction. Anticipated advances include: (1) Developing a system for proving liveness by Relational Rankings, based on EPR, and implementing it within the Ivy verification framework, (2) Developing automated techniques to aid liveness proofs, including synthesis of relational rankings and associated invariants and automated diagnosis of proof failures, and (3) Industrial case studies to evaluate the scalability of the approach and its accessibility to engineers, and provide benchmarks for future research. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.