@techreport{44f7a1008bd242f9b140f8c56a48e00c,
title = "Program Analysis Benchmarks Submitted to the Model Counting Competition MC 2020",
abstract = "Symbolic execution is a program analysis technique that systematically explores program execution paths by using symbolic inputs instead of concrete data. For each execution path, it is possible to construct a path condition (PC) using symbolic condition. The path condition is satisfiable if and only if the path is executable. Thus satisfiability solvers can be used to generate input data for exercising the program paths and traversing the flow graph. This is an essential task in software testing and static analysis (for bug finding). A further question is: How often can the path be executed, given a random input? This is the path execution frequency problem. And it can be solved with counting tools.",
author = "Sibylle M{\"o}hle and Cunjing Ge and Armin Biere",
year = "2021",
month = jan,
language = "English",
series = "FMV Reports Series",
publisher = "Institute for Formal Models and Verification, Johannes Kepler University",
type = "WorkingPaper",
institution = "Institute for Formal Models and Verification, Johannes Kepler University",
}