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

Displayed time zone: Tijuana, Baja California change

10:40 - 12:20
Testing and Program AnalysisResearch Papers / Demonstrations at Cortez 1
Chair(s): Jun Sun Singapore Management University, Singapore
10:40
20m
Talk
Regexes are Hard: Decision-making, Difficulties, and Risks in Programming Regular ExpressionsACM SIGSOFT Distinguished Paper Award
Research Papers
Louis G. Michael IV Virginia Tech, James Donohue University of Bradford, James C. Davis Virginia Tech, USA, Dongyoon Lee Stony Brook University, Francisco Servant Virginia Tech
Pre-print File Attached
11:00
20m
Talk
Testing Regex Generalizability And Its Implications: A Large-Scale Many-Language Measurement Study
Research Papers
James C. Davis Virginia Tech, USA, Daniel Moyer Virginia Tech, Ayaan M. Kazerouni Virginia Tech, Dongyoon Lee Stony Brook University
Pre-print File Attached
11:20
20m
Talk
Accurate String Constraints Solution Counting with Weighted Automata
Research Papers
Elena Sherman Boise State University, Andrew Harris Boise State University
11:40
20m
Talk
Subformula Caching for Model Counting and Quantitative Program Analysis
Research Papers
William Eiers University of California at Santa Barbara, USA, Seemanta Saha University of California Santa Barbara, Tegan Brennan University of California, Santa Barbara, Tevfik Bultan University of California, Santa Barbara
12:00
10m
Demonstration
SPrinter: A Static Checker for Finding Smart Pointer Errors in C++ Programs
Demonstrations
Xutong Ma Institute of Software, Chinese Academy of Sciences, Jiwei Yan Institute of Software, Chinese Academy of Sciences, Yaqi Li Institute of Software, Chinese Academy of Sciences, Jun Yan Institute of Software, Chinese Academy of Sciences, Jian Zhang Institute of Software, Chinese Academy of Sciences
12:10
10m
Demonstration
FPChecker: Detecting Floating-Point Exceptions in GPU Applications
Demonstrations
Ignacio Laguna Lawrence Livermore National Laboratory