Sibylle Möhle, Cunjing Ge, Armin Biere,
"Program Analysis Benchmarks Submitted to the Model Counting Competition MC 2020"
, Serie FMV Reports Series, Vol. 21/1, Institute for Formal Models and Verification, Johannes Kepler University, Linz, 1-2021
Original Titel:
Program Analysis Benchmarks Submitted to the Model Counting Competition MC 2020
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
Institute for Formal Models and Verification, Johannes Kepler University