Abstraction-based model checking programs

作者：Qian Junyan^*; Xu Baowen; Zhang Yingzhou

来源：Journal of Computational Information Systems, 2007, 3(2): 675-682.

• Formal verification
• Predicate abstraction

Model checking is an automatic formal verification technique for a finite state system. Iterative abstraction refinement has emerged recently as the leading approach to software model checking. We present a methodology for automatically verifying programs against safety specifications based on finite state machine. As the first step, an initial abstract model is automatically extracted from source code using predicate abstraction and theorem proving. In order to reduce time complexities of this process, we partition the set of candidate predicates into subsets, and then construct abstract model independently.

• 出版日期2007
• 单位东南大学