TY - GEN
T1 - Testing static analyzers with randomly generated programs
AU - Cuoq, Pascal
AU - Monate, Benjamin
AU - Pacalet, Anne
AU - Prevosto, Virgile
AU - Regehr, John
AU - Yakobowski, Boris
AU - Yang, Xuejun
PY - 2012/4/11
Y1 - 2012/4/11
N2 - Static analyzers should be correct. We used the random C-program generator Csmith, initially intended to test C compilers, to test parts of the Frama-C static analysis platform. Although Frama-C was already relatively mature at that point, fifty bugs were found and fixed during the process, in the front-end (AST elaboration and type-checking) and in the value analysis, constant propagation and slicing plug-ins. Several bugs were also found in Csmith, even though it had been extensively tested and had been used to find numerous bugs in compilers.
AB - Static analyzers should be correct. We used the random C-program generator Csmith, initially intended to test C compilers, to test parts of the Frama-C static analysis platform. Although Frama-C was already relatively mature at that point, fifty bugs were found and fixed during the process, in the front-end (AST elaboration and type-checking) and in the value analysis, constant propagation and slicing plug-ins. Several bugs were also found in Csmith, even though it had been extensively tested and had been used to find numerous bugs in compilers.
U2 - 10.1007/978-3-642-28891-3_12
DO - 10.1007/978-3-642-28891-3_12
M3 - Conference contribution
AN - SCOPUS:84859469491
SN - 9783642288906
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 120
EP - 125
BT - NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings
T2 - 4th NASA Formal Methods Symposium, NFM 2012
Y2 - 3 April 2012 through 5 April 2012
ER -