[Pl-seminar] Reminder: Seminar TOMORROW: Koushik Sen, Concolic Testing: A Decade Later

[Daniel Patterson]

Reminder: This is tomorrow at noon.

On Fri, Sep 23, 2016 at 11:49 AM, Daniel Patterson <dbp at ccs.neu.edu> wrote:

> NUPRL Seminar presents
>
> Koushik Sen
> University of California, Berkeley
>
> 12:00--1:30pm
> Thursday, Oct. 6 2016
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
> Host: Frank Tip
>
> Concolic Testing: A Decade Later
>
> Abstract:
>
> Symbolic execution, which was introduced more than four decades ago,
> is typically used in software testing to explore as many different
> program paths as possible in a given amount of time, and for each path
> to generate a set of concrete input values exercising it, and check
> for the presence of various kinds of errors including assertion
> violations, uncaught exceptions, security vulnerabilities, and memory
> corruption.  A key limitation of classical symbolic execution is that
> it cannot generate useful test inputs if the program under test uses
> complex operations such as pointer manipulations and non-linear
> arithmetic operations.
>
> Our research on Concolic Testing (also known as DART: Directed
> Automated Random Testing or Dynamic Symbolic Execution) alleviated the
> limitations of classical symbolic execution by combining concrete
> execution and symbolic execution.  We demonstrated that concolic
> testing is an effective technique for generating high-coverage test
> suites and for finding deep errors in complex software
> applications. The success of concolic testing in scalably and
> exhaustively testing real-world software was a major milestone in the
> ad hoc world of software testing and has inspired the development of
> several industrial and academic automated testing and security tools.
>
> One of the key challenges of concolic testing is the huge number of
> programs paths in all but the smallest programs, which is usually
> exponential in the number of static branches in the code.  In this
> talk I will describe MultiSE, a new technique for merging states
> incrementally during symbolic execution, without using auxiliary
> variables. The key idea of MultiSE is based on an alternative
> representation of the state, where we map each variable, including the
> program counter, to a set of guarded symbolic expressions called a
> value summary. MultiSE has several advantages over conventional
> symbolic execution and state merging techniques: 1) value summaries
> enable sharing of symbolic expressions and path constraints along
> multiple paths, 2) value-summaries avoid redundant execution, 3)
> MultiSE does not introduce auxiliary symbolic values, which enables it
> to make progress even when merging values not supported by the
> constraint solver, such as floating point or function values.  We have
> implemented MultiSE for JavaScript programs in a publicly available
> open-source tool. Our evaluation of MultiSE on several programs shows
> that MultiSE can run significantly faster than traditional symbolic
> execution.
>
>
> Bio:
>
> Koushik Sen is an associate professor in the Department of Electrical
> Engineering and Computer Sciences at the University of California,
> Berkeley. His research interest lies in Software Engineering,
> Programming Languages, and Formal methods. He is interested in
> developing software tools and methodologies that improve programmer
> productivity and software quality. He is best known for his work on
> ³DART: Directed Automated Random Testing² and concolic testing. He has
> received a NSF CAREER Award in 2008, a Haifa Verification Conference
> (HVC) Award in 2009, a IFIP TC2 Manfred Paul Award for Excellence in
> Software: Theory and Practice in 2010, a Sloan Foundation Fellowship
> in 2011, a Professor R. Narasimhan Lecture Award in 2014, and an Okawa
> Foundation Research Grant in 2015. He has won several ACM SIGSOFT
> Distinguished Paper Awards. He received the C.L. and Jane W-S. Liu
> Award in 2004, the C. W. Gear Outstanding Graduate Award in 2005, and
> the David J. Kuck Outstanding Ph.D. Thesis Award in 2007, and a
> Distinguished Alumni Educator Award in 2014 from the UIUC Department
> of Computer Science. He holds a B.Tech from Indian Institute of
> Technology, Kanpur, and M.S. and Ph.D. in CS from University of
> Illinois at Urbana-Champaign.
>
-------------- next part --------------
HTML attachment scrubbed and removed