| 
|
QuoteRef: laruJR5_2004
Topic:
handling complexity
Topic:
the effect of scale
Topic:
decomposition of a system into levels
Topic:
what is a computer
Topic:
debugging by usage rules
Topic:
code optimization by flow analysis
Topic:
flavor analysis and typestates for supplementary type checking
Topic:
owned resources and data objects
Topic:
consistency testing
Topic:
boolean values, binary numbers, and bit strings
Topic:
model checker
Topic:
declarative vs. procedural representation
Topic:
device driver
Group:
security
Topic:
aliasing
Reference
Larus, J.R., Ball, T., Das, M., DeLine, R., Fahndrich, M., Pincus, J., Rajamani, S.K., Venkatapathy, R., "Righting software", IEEE Software, May/June 2004, pp. 92-100. Google
92 ;;Quote: a vast amount of code is required to realize a programmer's intent, often concisely stated
92+;;Quote: use correctness tools to close the immense gap between code and intent
94 ;;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
94 ;;Quote: PREfast checks parse trees for problemantic idioms; e.g., number of bytes vs. number of characters
94 ;;Quote: PREfix and PREfast found 1/8 of the bugs fixed in Windows Server 2003
95 ;;Quote: Slam turns a C program into a boolean program with the same control-flow and Boolean variables; easier to analyze
96 ;;Quote: eliminate spurious paths in a Boolean program by automatically adding boolean control variables; e.g., resource allocation within loops and conditionals
96 ;;Quote: Slam found many errors in Windows device drivers; it separates the control path from the data path; e.g., resource use
97 ;;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
98 ;;Quote: Vault as a safe C with execution-ordering constraints; object in one of several states; annotate functions for their effect on object state
98+;;Quote: Vault identifies non-aliasing objects for type state analysis
Topic: handling complexity (60 items)
Topic: the effect of scale (17 items)
Topic: decomposition of a system into levels (49 items)
Topic: what is a computer (62 items)
Topic: debugging by usage rules (41 items)
Topic: code optimization by flow analysis (47 items)
Topic: flavor analysis and typestates for supplementary type checking (68 items)
Topic: owned resources and data objects (12 items)
Topic: consistency testing (60 items)
Topic: boolean values, binary numbers, and bit strings (44 items)
Topic: model checker (49 items)
Topic: declarative vs. procedural representation (54 items)
Topic: device driver (15 items)
Group: security (23 topics, 874 quotes)
Topic: aliasing (28 items)