SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software
Analyzing multithreaded programs is notoriously hard due to the exponential number of thread interleavings. Although race detectors can help developers find and fix such bugs before the code is deployed, multithreaded code may still be buggy due to memory errors and assertion violations that are not due to race conditions. This paper presents a property directed symbolic execution of multithreaded code. Our approach, named SIFT, differs from previous work on detecting errors in multithreaded code by being property directed and by handling both memory safety and assertion checking that can be further customized by the user. SIFT can detect bugs that may or may not be due to data races, and works in an iterative way. In each step, it explores the state space using selective scheduling based on a set of interleaving points that have been inferred in the previous step. We have developed three partitioning strategies for improved effectiveness and performance. We have implemented SIFT on top of the KLEE symbolic execution engine and applied it to various real-world and academic benchmarks. SIFT could detect more vulnerabilities than a state-of-the-art memory vulnerability detector.
Thu 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:45 - 18:00 | ICST Symbolic executionResearch Papers / Industry / Testing Tools / Journal-First Papers at Margaret Hamilton Chair(s): Arie van Deursen Delft University of Technology, Netherlands | ||
16:45 15mTalk | Translating EULYNX SysML models into Symbolic Transition Systems for Model-Based Testing of Railway signaling systems Industry Tobias Bachmann Universiteit van Amsterdam, Machiel van der Bijl Axini, Daan van der Meij ProRail, Djurre van der Wal University of Twente, Ana Oprescu University of Amsterdam | ||
17:00 15mTalk | Model checking C++ programs Journal-First Papers Felipe R. Monteiro Amazon, Mikhail R. Gadelha Igalia, Lucas C. Cordeiro University of Manchester, UK Link to publication DOI | ||
17:15 15mTalk | SIFT: A Tool for Property Directed Symbolic Execution of Multithreaded Software Testing Tools Tuba Yavuz University of Florida | ||
17:30 15mTalk | Automating Differential Testing with Overapproximate Symbolic Execution Research Papers | ||
17:45 15mLive Q&A | Discussion and Q&A Research Papers |