Extreme Model Checking

One of the central axioms of extreme programming is the disciplined use of regression testing during stepwise software development. Due to recent progress in software model checking, it has become possible to supplement this process with automatic checks for behavioral safety properties of programs, such as conformance with locking idioms and other programming protocols and patterns. For efficiency reasons, all checks must be incremental, i.e., they must reuse partial results from previous checks in order to avoid all unnecessary repetition of expenification tasks. We show that the lazy-abstraction algorithm, and its implementation in Blast, can be extended to support the fully automatic and incremental checking of temporal safety properties during software development. 1 From Extreme Programming to Extreme Verification Program verification has been a central problem of computer science for many years [39, 40]. The importance of the verification problem has, despite its inherent in...

• Type: Conference
• Year: 2003
• Where: BIRTHDAY
• Authors: Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido
• Keywords: Applied Computing, BIRTHDAY 2003, Extreme Programming, Model Checking, Safety Properties