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.

翻译：本文展示了如何将规范性类型检查与约束求解相结合，以提升软件验证过程中的自动化程度。我们通过定义一个类型系统并实现{log}（读作"setlog"）的类型检查器来实现这一目标。{log}是一种基于集合论的约束逻辑编程（CLP）语言及可满足性求解器。具体研究步骤如下：a) 为{log}定义类型系统；b) 证明约束求解器相对于该类型系统是安全的；c) 给出具体类型检查器的实现方案；d) 讨论如何通过整合类型检查与集合约束求解来提升软件验证的自动化水平；e) 通过两个工业级案例研究展示了该组合方法所取得的优异效果。