Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
arXiv (Cornell University)(2022)
摘要
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)
更多查看译文
关键词
type checking,set constraint,automated
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要