Better Lemmas with Lambda Extraction

Description

In Satisfiability Modulo Theories (SMT), the theory of arrays provides operations to access and modify an array at a given index, e.g., read and write. However, common operations to modify multiple indices at once, e.g., memset or memcpy of the standard C library, are not supported. We describe algorithms to identify and extract array patterns representing such operations, including memset and memcpy.We represent these patterns in our SMT solver Boolector by means of compact and succinct lambda terms, which yields better lemmas and increases overall performance. We describe how extraction and merging of lambda terms affects lemma generation, and provide an extensive experimental evaluation of the presented techniques. It shows a considerable improvement in terms of solver performance, particularly on instances from symbolic execution.

Period	28 Sept 2015
Event title	unbekannt/unknown
Event type	Conference
Location	United StatesShow on map