<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">

<head>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii">
<meta name=Generator content="Microsoft Word 12 (filtered medium)">
<style>
<!--
 /* Font Definitions */
 @font-face
        {font-family:Tahoma;
        panose-1:2 11 6 4 3 5 4 4 2 4;}
 /* Style Definitions */
 p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0in;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
a:link, span.MsoHyperlink
        {mso-style-priority:99;
        color:blue;
        text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
        {mso-style-priority:99;
        color:purple;
        text-decoration:underline;}
p
        {mso-style-priority:99;
        margin:0in;
        margin-bottom:.0001pt;
        font-size:12.0pt;
        font-family:"Times New Roman","serif";}
span.EmailStyle18
        {mso-style-type:personal-reply;
        font-family:"Calibri","sans-serif";
        color:#1F497D;}
.MsoChpDefault
        {mso-style-type:export-only;
        font-size:10.0pt;}
@page Section1
        {size:8.5in 11.0in;
        margin:1.0in 1.0in 1.0in 1.0in;}
div.Section1
        {page:Section1;}
-->
</style>
<!--[if gte mso 9]><xml>
 <o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
 <o:shapelayout v:ext="edit">
  <o:idmap v:ext="edit" data="1" />
 </o:shapelayout></xml><![endif]-->
</head>

<body lang=EN-US link=blue vlink=purple>

<div class=Section1>

<div>

<div>

<p class=MsoNormal><span style='font-size:10.0pt;font-family:"Tahoma","sans-serif";
color:black'>PLEASE NOTE THAT THE SUBMISSION DEADLINE HAS BEEN EXTENDED TO
April 12, 2009</span><span style='font-size:10.0pt;font-family:"Tahoma","sans-serif";
color:#1F497D'><o:p></o:p></span></p>

</div>

<div>

<p class=MsoNormal><span style='font-size:10.0pt;font-family:"Tahoma","sans-serif";
color:black'>(please accept our apologies if you get duplicate copies of this
announcement)<br>
<br>
===================================================================<br>
<br>
Workshop on Quantitative Analysis of Software<br>
<a href="http://www.eecs.berkeley.edu/~sseshia/qa09/" target="_blank">http://www.eecs.berkeley.edu/~sseshia/qa09/</a><br>
<br>
<br>
on June 28, 2009 in Grenoble, France<br>
Co-located with CAV 2009 <br>
<br>
===================================================================<br>
<br>
----- Aims and Scope -----<br>
<br>
Formal verification of software has mostly been concerned with Boolean<br>
properties of code, such as, are assertions satisfied, are all buffer<br>
accesses within bounds, does it always terminate, is there any<br>
undesirable information flow, etc.. However, often times it is desirable<br>
to ask more quantitative questions about software, such as, what is the<br>
expected number of bugs in the software and what is the mean-time<br>
between failures (to facilitate decisions about software releases), how<br>
much resources (e.g., time, memory, power) does it consume (for<br>
performance analysis, and to provide guarantees for embedded, real-time<br>
systems), how much information does it leak or how well is it obfuscated<br>
(for security related issues).<br>
<br>
This workshop will aim to explore novel techniques for quantitative<br>
analysis of software. It is particularly focused on code-level analysis<br>
rather than analysis purely of models of software or systems. All<br>
techniques are welcome, including static, dynamic, and probabilistic<br>
analyses. The aim of this workshop is bring together researchers from<br>
different areas (programming languages, software engineering, embedded<br>
systems, performance analysis, computer security, formal verification, AI,<br>
randomized/approximation algorithms, etc.) who are interested in any<br>
quantitative aspect of software, thereby providing a platform to<br>
investigate if there are common techniques that could be applied to a<br>
range of quantitative analyses.<br>
<br>
The scope of the workshop, includes, but is not restricted to, the<br>
following topics:<br>
<br>
* Performance Analysis<br>
* Reliability Evaluation<br>
* Resource Bound Analysis<br>
* Execution Time Analysis<br>
* Quantitative Information Flow<br>
* Probabilistic Analysis<br>
* Software Quality Metrics<br>
* SAT and SMT engines for quantitative analysis, e.g., model counting
techniques<br>
<br>
Two categories of papers will be considered: regular (long) papers, and<br>
short position papers that propose a new idea/methodology with<br>
justification. Novelty of the proposed ideas and applicability of<br>
techniques to code-level analysis will be given high weightage in<br>
evaluating papers.<br>
<br>
<br>
----- Paper Submission (note new submission deadline) -----<br>
<br>
Important dates:<br>
<br>
* Submission deadline: April 12th, 2009<br>
* Notification of acceptance/rejection: May 18th, 2009<br>
* Final version due: May 28th, 2009<br>
* Workshop: June 28, 2009<br>
<br>
Papers in all categories will be peer-reviewed. The page limit for<br>
regular papers is 10 and for position papers is 5. Submitted papers (in<br>
PDF) should be written in LaTeX with the following settings: 11pt,<br>
single column, letter size, and at least 1 inch margins.<br>
<br>
Papers should be submitted using the automated submission system <br>
<a href="http://www.easychair.org/conferences/?conf=qa09" target="_blank">http://www.easychair.org/conferences/?conf=qa09</a>
hosted by EasyChair.<br>
<br>
Proceedings will be distributed at the workshop. We are also planning<br>
to publish the proceedings online either in the ENTCS series or as a<br>
UC Berkeley EECS technical report, so that it can serve as a citable<br>
record for the authors.<br>
<br>
<br>
----- Invited Speaker -----<br>
<br>
Thomas A. Henzinger (EPFL)<br>
<br>
<br>
----- Organizers -----<br>
<br>
* Sumit Gulwani (Microsoft Research)<br>
* Sanjit Seshia (UC Berkeley)<br>
<br>
<br>
----- Program Committee -----<br>
<br>
* Luca de Alfaro (UC Santa Cruz)<br>
* Sumit Gulwani (Microsoft Research)<br>
* Marta Kwiatkowska (Oxford Univ.)<br>
* Pasquale Malacaria (Queen Mary Univ.)<br>
* Stephen McCamant (UC Berkeley)<br>
* Nachiappan Nagappan (Microsoft Research)<br>
* Jens Palsberg (UCLA)<br>
* Peter Puschner (T.U. Vienna)<br>
* Sanjit Seshia (UC Berkeley)<br>
<br>
<br>
----- Sponsors -----<br>
<br>
* CAV 2009<br>
* Microsoft Research, Redmond<o:p></o:p></span></p>

</div>

</div>

</div>

</body>

</html>