Wed 7 Nov 2018 16:37 - 17:00 at Horizons 10-11 - Symbolic Execution and Constraint Solving Chair(s): Satish Chandra

Recently, symbolic program analysis techniques have been extended to
quantitative analyses using model counting constraint solvers. Given
a constraint and a bound, a model counting constraint solver computes
the number of solutions for the constraint within the bound. We present
a parameterized model counting constraint solver for string and numeric
constraints. We first construct a multi-track deterministic finite state
automaton that accepts all solutions to the given constraint. We limit
the numeric constraints to linear integer arithmetic, and for non-regular
string constraints we over-approximate the solution set. Counting the
number of accepting paths in the generated automaton solves the model
counting problem. Our approach is parameterized in the sense that, we do
not assume a finite domain size during automata construction, resulting in
a potentially infinite set of solutions, and our model counting approach
works for arbitrarily large bounds. We experimentally demonstrate
the effectiveness of our approach on a large set of string and numeric
constraints extracted from software applications. We experimentally compare
our tool to five existing model counting constraint solvers for string and
numeric constraints and demonstrate that our tool is as efficient and as
or more precise than other solvers. Moreover, our tool can handle mixed
constraints with string and integer variables that no other tool can.

Conference Day
Wed 7 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00
Symbolic Execution and Constraint SolvingResearch Papers at Horizons 10-11
Chair(s): Satish ChandraFacebook
Concurrency Verification with Maximal Path Causality
Research Papers
Qiuping YiTexas A&M University, Jeff HuangTexas A&M University
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks
Research Papers
Shengjian (Daniel) GuoVirginia Tech, Meng WuVirginia Tech, Chao WangUSC
Symbolic Execution with Existential Second-Order Constraints
Research Papers
Sergey MechtaevNational University of Singapore, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler, Abhik RoychoudhuryNational University of Singapore
DOI Pre-print
Parameterized Model Counting for String and Numeric Constraints
Research Papers
Abdulbaki AydinMicrosoft, USA, William EiersUniversity of California at Santa Barbara, USA, Lucas Bang, Tegan Brennan, Miroslav GavrilovUniversity of California at Santa Barbara, USA, Tevfik BultanUniversity of California, Santa Barbara, Fang YuNational Chengchi University