SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer

T. Reps, S. Horwitz, and M. Sagiv, “Precise Interprocedural Dataflow Analysis Via Graph Reachability,” in POPL

1995

Earlier work this paper cites.

C. Lattner and V. Adve, “LLVM: A Compilation Framework For Lifelong Program Analysis & Transformation,” in CGO

2004

Earlier work this paper cites.

D. Novillo, “GCC- An Architectural Overview, Current Status And Future,” in The Linux Symposium

2006

Earlier work this paper cites.

B. Dutertre and L. De Moura, “The Yices SMT Solver,” August 2006

2006

Earlier work this paper cites.

L. De Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in TACAS

2008

Earlier work this paper cites.

R. Brummayer and A. Biere, “Boolector: An Efficient SMT Solver For Bit-Vectors And Arrays,” in TACAS

2009

Earlier work this paper cites.

C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, and C. Tinelli, “CVC4,” in CAV

2011

Earlier work this paper cites.

M. Junker, R. Huuck, A. Fehnker, and A. Knapp, “SMT-based False Positive Elimination In Static Program Analysis,” in ICFEM

2012

Cited alongside, same era.

A. Cimatti, A. Griggio, B. Schaafsma, and R. Sebastiani, “The MathSAT5 SMT Solver,” in TACAS

2013

Cited alongside, same era.

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-C: A Software Analysis Perspective,” Formal Aspects of Computing

2015

Cited alongside, same era.

C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. O’Hearn, I. Papakonstantinou, J. Purbrick, and D. Rodriguez, “Moving Fast With Software Verification,” in NASA Formal Methods

2015

Cited alongside, same era.

M. Arroyo, F. Chiotta, and F. Bavera, “An User Configurable Clang Static Analyzer Taint Checker,” in SCCC

2016

Cited alongside, same era.

[Online; accessed September-2018]

M. Larabel, “OpenBSD Switches To Clang Compiler For I386/AMD64.” https://www.phoronix.com/scan.php?page=news_item&px=OpenBSD-Default-Clang , 2017 · 2018

Closest in time.

G. Horváth, P. Szécsi, Z. Gera, D. Krupp, and N. Pataki, “Implementation And Evaluation Of Cross Translation Unit Symbolic Execution For C Family Languages,” in ICSE

2018

Closest in time.

[Online; accessed September-2018]

A. Dergachev, “Clang Static Analyzer: A Checker Developer’s Guide.” https://github.com/haoNoQ/clang-analyzer-guide , 2018 · 2018

Closest in time.

[Online; accessed September-2018]

“Available Checkers.” https://clang-analyzer.llvm.org/available_checks.html , 2018 · 2018

Closest in time.

[Online; accessed September-2018]

“Cppcheck - A Tool For Static C/C++ Code Analysis.” http://cppcheck.sourceforge.net , 2018 · 2018

Closest in time.

M. R. Gadelha, F. R. Monteiro, J. Morse, L. C. Cordeiro, B. Fischer, and D. A. Nicole, “ESBMC 5.0: An Industrial-Strength C Model Checker,” in ASE