Beyond Symbolic Model Checking through Deep Modelling

Formal verification of software, developed from a highly successful field of hardware verification, is currently facing an explosion in the number of safety critical applications written in programming languages that are increasingly far from hardware. For instance, the emergence of large-scale distributed consensus algorithms and their applications to smart contracts have not only created wholly new research questions but also challenged the way in which verification is currently being done, due to their use of high bit-widths and application-specic languages. In this proposal we outline deep modelling, a new approach that integrates symbolic modelling and the decision procedures used for solving the models. Our goal is to go beyond the traditional approaches originating from hardware model checking by introducing a rigorous system that is built from the beginning to support software verification. The outlined approach requires a deep understanding of both model checking and decision procedures due to it being fundamentally two-fold:we take information from the domain to obtain more efficient abstractions; and we study changes to the decision procedures so that they can better adjust to the model being solved.