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 

• Type: Conference
• Year: 2006
• Where: SEFM
• Authors: Sriram K. Rajamani
• Keywords: Analysis Tools, Heuristic Analyzers, SEFM 2006, Software Engineering, Tic Analysis Tools