Size and Accuracy in Model Inference Many works infer finitestate models from execution logs. Large models are more accurate but also more difficult to present and understand. Small models are easier to present and understand but are less accurate. In this work we investigate the tradeoff between model size and accuracy in the context of the classic kTails model inference algorithm. First, we define mkTails, a generalization of kTails from one to many parameters, which enables finegrained control over the tradeoff. Second, we extend mkTails with a reduction based on pastequivalence, which effectively reduces the size of the model without decreasing its accuracy. We implemented our work and evaluated its performance and effectiveness on realworld logs as well as on models and generated logs from the literature.

Subformula Caching for Model Counting and Quantitative Program Analysis Quantitative program analysis is an emerging area with applications to software reliability, quantitative information flow, sidechannel 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 modelcounting queries has been demonstrated in prior work, our key insight is that many subformulas are shared across nonidentical 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 sidechannels. Our experimental results demonstrate that our subformula caching approach significantly improves the performance of quantitative program analysis.