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

Quantitative program analysis is an emerging area with applications to software reliability, quantitative information flow, side-channel detection and attack synthesis. Most quantitative program analysis techniques rely on model counting constraint solvers, which are typically the bottleneck for scalability. Although the effectiveness of formula caching in expediting expensive model-counting queries has been demonstrated in prior work, our key insight is that many subformulas are shared across non-identical constraints generated during program analyses. This has not been utilized by prior formula caching approaches. In this paper we present a subformula caching framework and integrate it into a model counting constraint solver. We experimentally evaluate its effectiveness under three quantitative program analysis scenarios: 1) model counting constraints generated by symbolic execution, 2) reliability analysis using probabilistic symbolic execution, 3) adaptive attack synthesis for side-channels. Our experimental results demonstrate that our subformula caching approach significantly improves the performance of quantitative program analysis.

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