Quote: static source code analysis is automatic, descriptive, and finds bugs in untestable code [»englD10_2001]

Quote: using consistency rules to catch null reference errors [»englD10_2001]

Quote: every item of data must be used; state explicitly before overwriting an unused value [»scowRS_1979]

Quote: type systems say nothing about concurrency or dynamics; e.g., that initialize happens first, or x() must be invoked every 10 ms [»leeEA9_2000]

Quote: annotations and static analysis identified format bugs, buffer overflow bugs, and unknown flaws in wu-ftpd [»evanD1_2002]

Quote: use patterns, like C++ expressions, are more abstract and readable than an equivalent set of operations and auxiliary types [»dosrG1_2006]

Quote: PREfix and PREfast found 1/8 of the bugs fixed in Windows Server 2003 [»laruJR5_2004]

Quote: Slam found many errors in Windows device drivers; it separates the control path from the data path; e.g., resource use [»laruJR5_2004]

Quote: find serious mistakes and usage errors by detecting bug patterns, i.e., code idioms that often error; easily implemented [»hoveD12_2004]

Quote: FindBugs identifies 50 bug patterns using the inheritance hierarchy, linear code scan, control flow graph, and dataflow analysis; implemented with BCEL; most tests are short [»hoveD12_2004]

Quote: bug detectors for thread correctness, performance issue, security violation, usage bug, dropped exception, null pointer, open stream, unchecked return, unconditional wait [»hoveD12_2004]

Quote: PREfast checks parse trees for problemantic idioms; e.g., number of bytes vs. number of characters [»laruJR5_2004]

Quote: ESP checks very large C/C++ programs with a finite state machine of syntactic code patterns; most branches are irrelevant; e.g., security properties over a million lines with 25 false errors [»laruJR5_2004]

Quote: the probabilistic calling context (PCC) is a hash of the calling context and call site; 3% overhead for Java; e.g., detecting anomalous behavior after a training session [»bondMD10_2007]

Quote: use bug checkers for latent bugs; e.g., a covariant equals method works until someone adds the class to a map or set; another latent bug is hashcode/equals [»hoveD12_2004]

Quote: a PQL query is the shortest amount of code that violates a design rule; handles event sequences over related objects [»martM10_2005]

Quote: dynamic analysis by PQL found 200 errors in Eclipse; security flaws, resource leaks, and consistency invariants [»martM10_2005]

Quote: runtime overhead of PQL ranges from 9% to 125%; static analysis helps a lot; max is 19x slowdown [»martM10_2005]

Quote: find bugs by automatic extraction of usage rules; as templates (beliefs) with few contradictions [»englD10_2001]

Quote: rules for automated checks of consistency [»englD10_2001]

Quote: latent specifications in text by naming conventions, assertions, etc.; e.g., lock.. and unlock.., free.. and release.. [»englD10_2001]

Quote: extend static source code analysis to related code that shares the same belief set [»englD10_2001]

Quote: model checkers find a few difficult errors with simplified code; meta-level compilation works directly with program source and found many errors [»chouA11_2000]

Quote: validation methods are primarily used as bug-finders; formal methods are useful because they find different bugs than traditional methods; a more realistic goal than guaranteeing correctness [»dillDL4_1996]

Quote: Slam turns a C program into a boolean program with the same control-flow and Boolean variables; easier to analyze [»laruJR5_2004]

Quote: a bug checker uses static analysis to find correctness violations; while a style checker identifies code style violations [»hoveD12_2004]

Quote: PREfix for path-by-path analysis across function boundaries; finds null pointers, improper memory allocation/deallocation; uninitialized variables, resource state errors, improper library usage [»laruJR5_2004]

Quote: rank potential errors by ease-of-diagnosis, seriousness, and likelihood of false positives; rarely inspect all errors [»englD10_2001]

Quote: rank potential errors by the z statistic for proportions; deviation of observed ratio from expected ratio [»englD10_2001]

Quote: rank potential errors instead of beliefs; beliefs are too sensitive to threshold [»englD10_2001]

Quote: consistency test by annotating procedure with dependency relations for each result; useful for large, untidy structures [»jackD6_1993]

Quote: Vault as a safe C with execution-ordering constraints; object in one of several states; annotate functions for their effect on object state [»laruJR5_2004]

Quote: check restrictions of the following types; Never/Always do X, Always do X before/after Y, If you do X then you must/cannot do Y [»chouA11_2000]

Quote: detect violations of design rules by instrumenting the code using a static alias analysis; can correct erroneous executions on the fly [»martM10_2005]

Quote: check system invariants through compiler extensions; found 34 bugs in a well-tested, cache coherence protocol; short, easily written [»chouA11_2000]

Quote: use meta-level compilation (MC) to easily check path invariants; simple description, complicated source of errors, maintained across all paths; e.g., for cache coherence [»chouA11_2000]

Quote: meta-level compiler extensions pinpoints errors with 10-100 lines written in a few days; avoids complex errors

Quote: meta-level compilation through extensible compiler with high-level state machines applied down every path; transitions triggered by patterns [»chouA11_2000]

Quote: the most common synchronization error was ignoring read synchronization; data may be out-of-date or uninitialized [»hoveD7_2004]

Quote: concurrency bug patterns: mismatched wait, double locking, notify vs. notifyAll, run vs. start, mutable lock, naked notify, spin wait [»hoveD7_2004]

Quote: if enforce that data must be used before it is overwritten, frequent runtime errors that are all right 2/3's of the time [»scowRS_1979, OK]