Tags:automated reasoning, formal methods, smart contracts and verification
Abstract:
One of the most difficult aspects in formally verifying infinite state systems is reasoning about quantifiers. In this paper, we introduce a novel interactive approach to quantifier reasoning using an SMT solver. We automatically abstract the verification condition in a way that eliminates function cycles. The user refines this abstraction in response to spurious counterexamples by proposing ground terms to instantiate quantifiers. In applying this approach to the verification of Byzantine and non-Byzantine fault tolerance protocols, we found that few manual instantiations were needed. Moreover, the counterexamples provided valuable guidance for the user, in contrast to the timeouts produced by the traditional approach.
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols