Better Lemmas with Lambda Extraction

Beschreibung

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.

Zeitraum	28 Sep. 2015
Ereignistitel	unbekannt/unknown
Veranstaltungstyp	Konferenz
Ort	USA/Vereinigte StaatenAuf Karte anzeigen