Extreme Model Checking

10 years 11 months ago
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...
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar,
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Authors Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido
Comments (0)