Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
复制标题
虫子、痣和骷髅：软件开发的符号推理
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Nikolaj S. Bjørner
中科院分区：
文献类型：
--
作者：
L. D. Moura;Nikolaj S. Bjørner
符号推理是许多软件开发工具的核心，例如：bug查找器，测试用例生成器和验证器。新的兴趣是使用符号推理来合成代码、循环不变式和排名函数。由于技术的进步和越来越多的应用，可满足性模理论（SMT）求解器已经成为最近关注的焦点。在本文中，我们回顾了这些应用程序中的一些使用软件验证程序作为错误发现者“类固醇”，并建议需要新的模型发现技术来增加这些求解器支持的应用程序集。
Symbolic reasoning is in the core of many software development tools such as: bug-finders, test-case generators, and verifiers. Of renewed interest is the use of symbolic reasoning for synthesing code, loop invariants and ranking functions. Satisfiability Modulo Theories (SMT) solvers have been the focus of increased recent attention thanks to technological advances and an increasing number of applications. In this paper we review some of these applications that use software verifiers as bug-finders “on steroids” and suggest that new model finding techniques are needed to increase the set of applications supported by these solvers.