Automatically constructing objects based on description of their internal state is challenging because available constructors and API calls can manipulate the state in non-trivial ways. This problem is of particular relevance to constraint solver-driven automated testing, where the solver is queried to describe the initial state required for execution of a specific path through the target method. In this work, we focus on the Dafny programming language that supports verification of heap-related properties. Dafny has built-in test generation functionality and we propose to extend it with a technique for synthesizing sequences of API calls that create objects and set their state in such a way that properties required by test generation are respected. The proposed method uses a heuristic-guided search over sequences of API calls, while leaving the task of inferring appropriate primitive arguments to the verifier. By combining domain-specific heuristics with the logics used by the Z3 theorem prover, the proposed method allows synthesizing instances of types defined in various open-source Dafny projects.
Program Display Configuration
Tue 18 Jul
Displayed time zone: Pacific Time (US & Canada)change