Software engineering and automated deduction
Willem I. Visser, Nikolaj Bjørner, Natarajan Shankar · 2014
Software poses a range of engineering challenges. How do we capture the expected behavior of the software? How can we check if such behavioral descriptions are consistent and valid? How do we generate test instances that explore and examine different parts of the software. We focus on the underlying technology by which a number of these problems can be reduced to a logical form and answered using automated deduction. In the first part we briefly summarize the use of automated deduction within software engineering. Then we consider some of the current and future trends in software engineering and the type of advances it may require from automated deduction. We observe that in the past software engineering problems were solved by merely leveraging advances in automated deduction, especially in SAT and SMT solving, whereas we are now entering a phase where advances in automated deduction are also driven by software engineering requirements.