NSV 2015 - 8th International Workshop on Numerical Software Verification (NSV-VIII)

Numerical abstractions are key to software verification. The CAV community has actively pursued technologies such as Presburger arithmetic, convex polyhedra (linear arithmetic), bit vectors, SAT solvers and quantifier elimination to handle numerical abstractions. Other conferences and workshops focus on the theory and practice of constraint solvers. However, the application of this technology to verification is spread across many communities including verification, programming languages, embedded systems and software engineering.
This workshop aims to bring together people who apply numerical reasoning to software verification. We also hope to bring forth ideas and techniques from embedded systems and control theory, that can be used for verification. The overall goal of this activity is to enable people pursuing applications to use the underlying reasoning in a more informed manner, while at the same time, enabling people who work on solvers to understand the key applications.
Topics of Interest
The topics of interest will focus on constraint solving technologies and applications. We are inviting leading researchers to talk about the current development and future prospects on applying logical and mathematical techniques for reasoning about numerical aspects of software. The scope of the workshop includes
numerical domains for abstract interpretation,
Symbolic model checking,
Arithmetic decision procedures,
size abstractions,
termination analysis,
timing/complexity analysis,
checking real-time properties,
validation for avionics, and automotive applications.