Peter Zeller

"Tool Supported Specification and Verification of Highly Available Applications"

Today, information systems are often distributed to achieve high availability and low latency. These systems can be realized by building on a highly available database to manage the distribution of data. However, it is well known that high availability and low latency are not compatible with strong consistency guarantees. For application developers, the lack of strong consistency on the database layer can make it difficult to reason about their programs and ensure that applications work as intended.We address this problem from the perspective of formal verification. We present a specification technique, which allows to specify functional properties of the application. In addition to data invariants, we support history properties, which allows to relate past events including invocations of the application API and operations on the database.To address the verification problem, we have developed a proof technique that handles concurrency using invariants and otherwise reduces the problem to sequential verification. The system semantics, technique and its soundness proof are all formalized in Isabelle/HOL. Additionally, we have developed a tool named Repliss which uses the proof technique to enable partially automated verification and testing of applications. For verification, Repliss generates verification conditions via symbolic execution and then uses an SMT solver to discharge them.