[Om-announce] CFP: QA 2009 (pre-CAV workshop)

[Sumit Gulwani]

(please accept our apologies if you get duplicate copies of this announcement)

===================================================================

Workshop on Quantitative Analysis of Software
http://www.eecs.berkeley.edu/~sseshia/qa09/


on June 28, 2009 in Grenoble, France
Co-located with CAV 2009 

===================================================================

----- Aims and Scope -----

Formal verification of software has mostly been concerned with Boolean
properties of code, such as, are assertions satisfied, are all buffer
accesses within bounds, does it always terminate, is there any
undesirable information flow, etc.. However, often times it is desirable
to ask more quantitative questions about software, such as, what is the
expected number of bugs in the software and what is the mean-time
between failures (to facilitate decisions about software releases), how
much resources (e.g., time, memory, power) does it consume (for
performance analysis, and to provide guarantees for embedded, real-time
systems), how much information does it leak or how well is it obfuscated
(for security related issues).

This workshop will aim to explore novel techniques for quantitative
analysis of software. It is particularly focused on code-level analysis
rather than analysis purely of models of software or systems. All
techniques are welcome, including static, dynamic, and probabilistic
analyses. The aim of this workshop is bring together researchers from
different areas (programming languages, software engineering, embedded
systems, performance analysis, computer security, formal verification, AI,
randomized/approximation algorithms, etc.) who are interested in any
quantitative aspect of software, thereby providing a platform to
investigate if there are common techniques that could be applied to a
range of quantitative analyses.

The scope of the workshop, includes, but is not restricted to, the
following topics:

* Performance Analysis
* Reliability Evaluation
* Resource Bound Analysis
* Execution Time Analysis
* Quantitative Information Flow
* Probabilistic Analysis
* Software Quality Metrics
* SAT and SMT engines for quantitative analysis, e.g., model counting techniques

Two categories of papers will be considered: regular (long) papers, and
short position papers that propose a new idea/methodology with
justification. Novelty of the proposed ideas and applicability of
techniques to code-level analysis will be given high weightage in
evaluating papers.


----- Paper Submission -----

Tentative dates:

* Submission deadline: April 5th, 2009
* Notification of acceptance/rejection: May 11th, 2009
* Final version due: May 25th, 2009
* Workshop: June 28, 2009

Papers in all categories will be peer-reviewed. The page limit for
regular papers is 10 and for position papers is 5. Submitted papers (in
PDF) should be written in LaTeX with the following settings: 11pt,
single column, letter size, and at least 1 inch margins.

Papers should be submitted using the automated submission system 
http://www.easychair.org/conferences/?conf=qa09 hosted by EasyChair.

Proceedings will be distributed at the workshop. We are also planning
to publish the proceedings online either in the ENTCS series or as a
UC Berkeley EECS technical report, so that it can serve as a citable
record for the authors.


----- Invited Speaker -----

Thomas A. Henzinger (EPFL)


----- Organizers -----

* Sumit Gulwani (Microsoft Research)
* Sanjit Seshia (UC Berkeley)


----- Program Committee -----

* Luca de Alfaro (UC Santa Cruz)
* Sumit Gulwani (Microsoft Research)
* Marta Kwiatkowska (Oxford Univ.)
* Pasquale Malacaria (Queen Mary Univ.)
* Stephen McCamant (UC Berkeley)
* Nachiappan Nagappan (Microsoft Research)
* Jens Palsberg (UCLA)
* Peter Puschner (T.U. Vienna)
* Sanjit Seshia (UC Berkeley)


----- Sponsors -----

* CAV 2009
* Microsoft Research, Redmond