![]() The direction of the traversal is determined by the results of the concretisation of an abstract counterexample obtained at the current node. The refinement process is then triggered by the lattice traversal, where in each node the SMT solver uses the subset of SMT summaries stored in this node to search for a satisfying assignment. We extend the approach of user-defined summaries and propose to represent the set of existing summaries for a given library function as a lattice of subsets of summaries, with the meet and join operations defined as intersection and union, respectively. The former approach leads to numerous spurious counter-examples, whereas the later faces the danger of the state-explosion problem, where the resulting formula is too large to be solved by means of modern SMT solvers. ![]() Typically, if the program correctness depends on the output of a library function, the model-checking process either treats this function as an uninterpreted function, or is required to use a theory under which the function in question is fully defined. In this paper we present an algorithm for bounded model checking with SMT solvers of programs with library functions-either standard or user-defined. We evaluate our approach on benchmarks taken from the robotics community, and our experimental results demonstrate that we are able to solve a number of instances that were previously unsolvable by existing SMT solvers. We generalise the method to a number of lattices for functions whose values depend on each other in the program, and we describe a simultaneous traversal algorithm of several lattices, so that a combination of guarded literals from all lattices does not lead to contradictory values of their variables. These subsets are found during the lattice traversal. These lattices are constructed from equations and inequalities of properties of the library functions. Our lightweight theory uses lattices for efficient representation of library functions by a subset of guarded literals. ![]() ![]() The full definition could in most cases lead to instances that are too large to solve efficiently. Common strategies for dealing with library functions include treating them as uninterpreted functions or using the theories under which the functions are fully defined. We present a lattice-based satisfiability modulo theory for verification of programs with library functions, for which the mathematical libraries supporting these functions contain a high number of equations and inequalities. ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |