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.

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 Chandra Facebook
Concurrency Verification with Maximal Path Causality
Research Papers
Qiuping Yi Texas A&M University, Jeff Huang Texas A&M University
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks
Research Papers
Shengjian (Daniel) Guo Virginia Tech, Meng Wu Virginia Tech, Chao Wang USC
Symbolic Execution with Existential Second-Order Constraints
Research Papers
Sergey Mechtaev National University of Singapore, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler, Abhik Roychoudhury National University of Singapore
DOI Pre-print
Parameterized Model Counting for String and Numeric Constraints
Research Papers
Abdulbaki Aydin Microsoft, USA, William Eiers University of California at Santa Barbara, USA, Lucas Bang , Tegan Brennan , Miroslav Gavrilov University of California at Santa Barbara, USA, Tevfik Bultan University of California, Santa Barbara, Fang Yu National Chengchi University