基于模型的应用软件的静态检测方法研究

摘要

该文把静态分析技术与基于模型的演绎验证结合起来提供了一个框架,分析应用源代码,自动生成一个分析器,它能够推断关于给定程序行为的逻辑约束方面的信息。该文引入了一阶逻辑断言来描述API调用语义。这些断言构成分析器使用的模型。通过实验,该方法可被用来识别Java程序中的关于安全的逻辑错误。