Blogs (1) >>
ASE 2019
Sun 10 - Fri 15 November 2019 San Diego, California, United States
Wed 13 Nov 2019 11:20 - 11:40 at Cortez 1 - Testing and Program Analysis Chair(s): Jun Sun

As an important extension of symbolic execution (SE), probabilistic symbolic execution (PSE) computes execution probabilities of program paths. Using this information, PSE can prioritize path exploration strategies. To calculate the probability of a path PSE relies on solution counting approaches for the path constraint. The correctness of a solution counting approach depends on the methodology used to count solutions and whether a path constraint maintains a one-to-one relation with program input values. This work focuses on the latter aspect of the solution counting correctness for string constraints.

In general, maintaining a one-to-one relation is not always possible, especially in a presence of non-linear constraints. To deal with this issue, researchers that work on PSE for numerical domains either analyze programs with linear constraints, or develop novel techniques to handle solution counting of non-linear constraints. For the string domain, however, previous work on PSE mainly focuses on efficient and accurate solution counting for automata-based string models and has not investigated whether a one-to-one relationship between the strings encoded by automata and input string values is preserved. In this work we demonstrate that traditional automata-base string models fail to maintain one-to-one relations and propose to use the weighted automata model, which preserves the one-to-one relation between the path constraint it encodes and the input string values. We use this model to implement a string constraint solver and show its correctness on a set of non-trivial synthetic benchmarks. We also present an empirical evaluation of traditional and proposed automata solvers on real-world string constraints. The evaluations show that while being less efficient than traditional automata models, the weighted automata model maintains correct solution counts.

Wed 13 Nov

10:40 - 12:20: Papers - Testing and Program Analysis at Cortez 1
Chair(s): Jun SunSingapore Management University, Singapore
ase-2019-papers10:40 - 11:00
Regexes are Hard: Decision-making, Difficulties, and Risks in Programming Regular ExpressionsACM SIGSOFT Distinguished Paper Award
Louis G. Michael IVVirginia Tech, James DonohueUniversity of Bradford, James C. DavisVirginia Tech, USA, Dongyoon LeeStony Brook University, Francisco ServantVirginia Tech
Pre-print File Attached
ase-2019-papers11:00 - 11:20
Testing Regex Generalizability And Its Implications: A Large-Scale Many-Language Measurement Study
James C. DavisVirginia Tech, USA, Daniel MoyerVirginia Tech, Ayaan M. KazerouniVirginia Tech, Dongyoon LeeStony Brook University
Pre-print File Attached
ase-2019-papers11:20 - 11:40
Accurate String Constraints Solution Counting with Weighted Automata
Elena ShermanBoise State University, Andrew HarrisBoise State University
ase-2019-papers11:40 - 12:00
Subformula Caching for Model Counting and Quantitative Program Analysis
William EiersUniversity of California at Santa Barbara, USA, Seemanta SahaUniversity of California Santa Barbara, Tegan BrennanUniversity of California, Santa Barbara, Tevfik BultanUniversity of California, Santa Barbara
ase-2019-Demonstrations12:00 - 12:10
SPrinter: A Static Checker for Finding Smart Pointer Errors in C++ Programs
Xutong MaInstitute of Software, Chinese Academy of Sciences, Jiwei YanInstitute of Software, Chinese Academy of Sciences, Yaqi LiInstitute of Software, Chinese Academy of Sciences, Jun YanInstitute of Software, Chinese Academy of Sciences, Jian ZhangInstitute of Software, Chinese Academy of Sciences
ase-2019-Demonstrations12:10 - 12:20
FPChecker: Detecting Floating-Point Exceptions in GPU Applications
Ignacio LagunaLawrence Livermore National Laboratory