Abstract | ||
---|---|---|
Model counting is the problem of determining the number of solutions that satisfy a given set of constraints. Model counting has numerous applications in the quantitative analyses of program execution time, information flow, combinatorial circuit designs as well as probabilistic reasoning. We present a new approach to model counting for structured data types, specifically strings in this work. The key ingredient is a new technique that leverages generating functions as a basic primitive for combinatorial counting. Our tool SMC which embodies this approach can model count for constraints specified in an expressive string language efficiently and precisely, thereby outperforming previous finite-size analysis tools. SMC is expressive enough to model constraints arising in real-world JavaScript applications and UNIX C utilities. We demonstrate the practical feasibility of performing quantitative analyses arising in security applications, such as determining the comparative strengths of password strength meters and determining the information leakage via side channels. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1145/2594291.2594331 | PLDI |
Keywords | Field | DocType |
combinatorial circuit design,quantitative analysis,information flow,combinatorial counting,model counting,new approach,expressive string language,model constraint,unbounded string,model counter,new technique,information leakage,consolidation,user defined functions,query optimization | Programming language,Password strength,Information leakage,Computer science,Unix,Real-time computing,Theoretical computer science,Probabilistic logic,Query optimization,Information flow (information theory),Algorithm,User-defined function,Data model | Conference |
Volume | Issue | ISSN |
49 | 6 | 0362-1340 |
Citations | PageRank | References |
11 | 0.51 | 21 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Loi Luu | 1 | 393 | 23.07 |
Shweta Shinde | 2 | 173 | 9.15 |
Prateek Saxena | 3 | 1915 | 97.73 |
Brian Demsky | 4 | 500 | 33.84 |