Sciweavers

CADE
2010
Springer

Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development

13 years 4 months ago
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.
Leonardo Mendonça de Moura, Nikolaj Bj&osla
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Leonardo Mendonça de Moura, Nikolaj Bjørner
Comments (0)