论文部分内容阅读
模型检查技术在硬件和协议设计方面已经取得很大成功，但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究，来解决并发程序验证的建模问题，包括把验证公式映射到切片准则．并把得到的程序切片转化为验证所需的模型。经程序切片处理后，软件模型检查效率得到提高。