First International Workshop on Numerical Abstractions for Software Verification.
July 8th, 2008.
Affliated with CAV 2008
Venue: Princeton, NJ
We measure our understanding (and control) by the extent to which
we can arithmetize an activity.
-- Alan J. Perlis, Epigrams in Programming.
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 InterestThe 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.
Format of the WorkshopThis 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.
ProceedingsWe 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.
|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|
|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|