Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development

Abstract. 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.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Leonardo Mendonça de Moura, Nikolaj Bjørner
• Keywords: CADE 2010, Logical Reasoning, Satisfiability Modulo Theories, Software Development Tools, Symbolic Reasoning