Automatic Property Checking for Software: Past, Present and Future

9 years 12 months ago
Automatic Property Checking for Software: Past, Present and Future
tic analysis tools based on abstraction are sound but not complete. Several practical static analysis tools are heuristic in nature —they are neither sound nor complete, but have proved to be useful nevertheless. Traditionally, attaching preconditions and postconditions to method boundaries has been widely advocated as the preferred method of writing specifications. The primary advantage of this approach is modularity and (consequently) scalability [13, 15]. However, in addition to the input and return parameters, most function calls have sideeffects resulting from the use and update of global state. Reasoning with such programs requires object invariants, and there has been recent progress in methodologies and tools for stating and checking object invariants [4]. 3 Heuristic analyzers Heuristic analyzers such as PREFix [6, 24], PREFast [24] and Metal [14] do not attempt to cover all paths. Further, along each path they do approximations. However, 1
Sriram K. Rajamani
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where SEFM
Authors Sriram K. Rajamani
Comments (0)