Construction of Inductive Property Predicates for Mutable Data Structures
Xuejian Li, Jun-Yi Wang · 2022 9th International Conference on Dependable Systems and Their Applications (DSA) · 2022
Program verification is a compelling way to ensure the dependable of software system, but the granularity of verification properties depends on the design of predicates. Definition of formal predicates is one of the prerequisites for automated software verification, the reason why predicate definitions of mutable data structures is relatively difficult, is that the trade-off between expressiveness of predicates and Satisfiability Modulo Theories (SMT) solver's proving capability. In this paper, we propose a method for constructing inductive predicates, which makes predicates more expressive and meanwhile ensures the provability of inductive properties in programs which manipulate mutable data structures through iteration. Furthermore, based on formal description of predicates about mutable data structures, a construction algorithm of complex inductive predicates is provided, which solves the dilemma of complicated programming of inductive property annotations during the verification process, and improves the automation of program verification. Experimental results show that the method can support the verification prototype to describe more complex properties about mutable data structures and alleviate the burden of automated theorem proving.