Detecting Errors Before Reaching Them

Abstract. Any formalmethodor tool is almostcertainlymoreoftenapplied in situationswheretheoutcomeis failure(acounterexample)rather than success (a correctness proof). We present a method for symbolic model checking that can lead to signi cant time and memory savings for model-checking runs that fail, while occurring only a small overhead for model-checkingruns thatsucceed.Our methoddiscoversan erroras soon as it cannotbe prevented,which can be long beforeit actually occurs for example, the violation of an invariant may become unpreventable many transitions before the invariant is violated. The key observation is that \unpreventability" is a local property of a single module: an error is unpreventable in a module state if no environment can prevent it. Therefore, unpreventability is inexpensive to compute for each module, yet can save much work in the state exploration of the global, compound system. Based on di erent degrees of information available about the environment, we de ne...

• Type: Conference
• Year: 2000
• Where: CAV
• Authors: Luca de Alfaro, Thomas A. Henzinger, Freddy Y. C. Mang
• Keywords: CAV 2000, Correctness Proof, Di Erent Degrees, Hardware, Single Module