65
IRUS Total
Downloads

© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.

File Description SizeFormat 
paper.pdfAccepted version1.05 MBAdobe PDFView/Open
Title: © 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Authors: Kapus, T
Cadar, C
Item Type: Conference Paper
Abstract: Symbolic execution is an effective technique for exploring paths ina program and reasoning about all possible values on those paths.However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to morethan one memory object. In such cases, symbolic execution typicallyforks execution into multiple states, one for each object to whichthe pointer could refer.In this paper, we propose a technique that avoids this expensiveforking by using asegmented memory model. In this model, mem-ory is split into segments, so that each symbolic pointer refers toobjects in a single segment. The size of the segments are bound by athreshold, in order to avoid expensive constraints. This results in amemory model where forking due to symbolic pointer dereferencesis significantly reduced, often completely.We evaluate our segmented memory model on a mix of wholeprogram benchmarks (such asm4andmake) and library bench-marks (such asSQLite), and observe significant decreases in execu-tion time and memory usage.
Issue Date: Aug-2019
Date of Acceptance: 24-May-2019
URI: http://hdl.handle.net/10044/1/72045
DOI: 10.1145/3338906.3338936
Publisher: ACM
Start Page: 774
End Page: 784
Copyright Statement: This paper is embargoed until publication.
Sponsor/Funder: Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Funder's Grant Number: EP/L002795/1
EP/N007166/1
Conference Name: ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’19)
Keywords: Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Symbolic execution
memory models
pointer alias analysis
KLEE
Publication Status: Published
Start Date: 2019-08-26
Finish Date: 2019-08-30
Conference Place: Tallinn, Estonia
Online Publication Date: 2019-08
Appears in Collections:Computing
Faculty of Engineering