论文标题
组合类型检查并设置约束求解以改进自动化软件验证
Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
论文作者
论文摘要
在本文中，我们展示了如何将处方类型的检查和约束解决方案组合在一起，以增加软件验证期间的自动化。我们通过定义类型系统并实现{log}（read``setLog''）的Typechecker，这是一种基于集合理论的约束逻辑编程（CLP）语言和满意度求解器。因此，我们进行如下：a）定义了{log}的类型系统； b）事实证明，约束求解器是安全的W.R.T.类型系统； c）提出了混凝土打字机的实现； d）讨论了在软件验证过程中的类型检查和设置约束求解以增加自动化的集成； f）提出了两个工业强度的案例研究，其中使用了这种组合的结果非常好。 在逻辑编程理论和实践中的考虑（TPLP）
In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read `setlog'), a Constraint Logic Programming (CLP) language and satisfiability solver based on set theory. Hence, we proceed as follows: a) a type system for {log} is defined; b) the constraint solver is proved to be safe w.r.t. the type system; c) the implementation of a concrete typechecker is presented; d) the integration of type checking and set constraint solving to increase automation during software verification is discussed; and f) two industrial-strength case studies are presented where this combination is used with very good results. Under consideration in Theory and Practice of Logic Programming (TPLP)
