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)

翻译：本文展示了如何将规范性类型检查与约束求解相结合，以提升软件验证过程中的自动化程度。为此，我们定义了一个类型系统，并为{log}（读作“setlog”）实现了一个类型检查器。{log}是一种基于集合理论的约束逻辑编程（CLP）语言及可满足性求解器。具体工作如下：a) 定义了{log}的类型系统；b) 证明了该约束求解器相对于该类型系统是安全的；c) 给出了具体类型检查器的实现；d) 讨论了如何将类型检查与集合约束求解集成以提升软件验证的自动化程度；f) 通过两项工业级案例研究展示了该组合方案取得了非常良好的效果。本文正在《逻辑编程理论与实践》（TPLP）期刊审稿中。