Software Model Checking Based on Abstract-verify-refine Paradigm
基于抽象-验证-细化范例的软件模型检测

How to assure the correctness and reliability of software systems is one of the main problems in software development. Being an important automatic verification technique, Model checking is more and more successful in software analysis and verification. This paper presents a survey to software model checking based on abstract-verify-reflne paradigm, using SLAM at Microsoft and BLAST at UC Berkeley as examples.