Subformula caching for model counting and quantitative program analysis

William Eiers, Seemanta Saha, Tegan Brennan, Tevfik Bultan

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages453-464
Number of pages12
ISBN (Electronic)9781728125084
DOIs
StatePublished - Nov 2019
Event34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019 - San Diego, United States
Duration: Nov 10 2019Nov 15 2019

Publication series

NameProceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019

Conference

Conference34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019
Country/TerritoryUnited States
CitySan Diego
Period11/10/1911/15/19

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Software
  • Control and Optimization

Keywords

  • Formula caching
  • Model counting
  • Quantitative program analysis

Fingerprint

Dive into the research topics of 'Subformula caching for model counting and quantitative program analysis'. Together they form a unique fingerprint.

Cite this