swMATH ID: 9957
Software Authors: Dams, Dennis R.; Namjoshi, Kedar S.
Description: Orion: high-precision methods for static error analysis of C and C++ programs. We describe the algorithmic and implementation ideas behind a tool, Orion, for finding common programming errors in C and C++ programs using static code analysis. We aim to explore the fundamental trade-off between the cost and the precision of such analyses. Analysis methods that use simple dataflow domains run the risk of producing a high number of false error reports. On the other hand, the use of complex domains reduces the number of false errors, but limits the size of code that can be analyzed.par Orion employs a two-level approach: potential errors are identified by an efficient search based on a simple domain; each discovered error path is then scrutinized by a high-precision feasibility analysis aimed at filtering out as many false errors as possible.par We describe the algorithms used and their implementation in a GCC-based tool. Experimental results on a number of software programs bear out the expectation that this approach results in a high signal-to-noise ratio of reported errors, at an acceptable cost.
Homepage: http://link.springer.com/chapter/10.1007/11804192_7
Related Software: SatAbs; BLAST; Goanna; ASTREE; SLAM; CVC; Bandera; DART; ESC/Java; veriSoft; AProVE; CEGAR; MU-CSeq; Symbiotic 2; CPAlien; Jakstab; FrankenBit; Ultimate Kojak; Lazy-CSeq; Threader
Cited in: 4 Publications

Cited in 0 Serials

Citations by Year