Make no mistake about it: Computers process numbers - not symbols.
We measure our understanding (and control) by the extent to which
we can arithmetize an activity.

-- Alan J. Perlis, Epigrams in Programming.

Goals

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

We plan to showcase projects that have applied numerical reasoning to software. We also wish to focus on emerging applications such as floating point analysis, program termination, timing analysis, resource estimation, overflow detection, hybrid systems and binary analysis.

Format of the Workshop

This is a one-day pre-conference workshop consisting of presentations from invited speakers only. There will be 4 sessions with two invited speakers in each session. Each speaker will be expected to deliver a 35 minute talk. This will be followed by 5-10 minutes of audience interaction.

Proceedings

We are happy to announce that the post-proceedings of this workshop will appear as a special issue in the journal Formal Methods in Systems Design.

Program

8:50-9:00 Opening Remarks
9:00-9:45 Tevfik Bultan, UC Santa Barbara, Infinite State Model Checking Using Presburger Arithmetic
9:45-10:30 Byron Cook, Microsoft Research, Cambridge, Proving recursive programs terminating, without the recursion
10:30-11:00 (COFFEE)
11:00-11:45 Patrick Cousot, ENS, France, Numerical Domains for Software Verification By Abstract Interpretation
11:45-12:30 Sriram Rajamani, Microsoft Research, India, Automatically Refining Abstract Interpretations
12:30 - 2:00 (LUNCH)
2:00 - 2:45 Mirko Conrad, MathWorks, USA, Translation Validation of Generated Code in the Context of IEC61508
2:45-3:30 Stavros Tripakis, Cadence Labs, USA, Modular Code Generation from Synchronous Block Diagrams
3:30 - 4:00 (COFFEE)
4:00-4:45 Ashish Tiwari, SRI, USA, Using the Theory of Reals in Analyzing Continous and Hybrid Systems
4:45-5:30 Matthieu Martel, Universite de Perpignan, France, Enhancing the implementation of mathematical formulas.
5:30 - 5:40 Closing Remarks

Organizers

Franjo Ivančić, Sriram Sankaranarayanan, and Chao Wang (NEC Laboratories America)

Contact

For questions related to this workshop and abstract submission for talks please contact the organizers.