<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=iso-8859-1"><meta name=Generator content="Microsoft Word 14 (filtered medium)"><style><!--
/* Font Definitions */
@font-face
        {font-family:Calibri;
        panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
        {margin:0cm;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Calibri","sans-serif";
        mso-fareast-language:EN-US;}
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.MsoPlainText, li.MsoPlainText, div.MsoPlainText
        {mso-style-priority:99;
        mso-style-link:"Plain Text Char";
        margin:0cm;
        margin-bottom:.0001pt;
        font-size:11.0pt;
        font-family:"Calibri","sans-serif";
        mso-fareast-language:EN-US;}
span.EmailStyle17
        {mso-style-type:personal-compose;
        font-family:"Calibri","sans-serif";
        color:windowtext;}
span.PlainTextChar
        {mso-style-name:"Plain Text Char";
        mso-style-priority:99;
        mso-style-link:"Plain Text";
        font-family:"Calibri","sans-serif";}
.MsoChpDefault
        {mso-style-type:export-only;
        font-family:"Calibri","sans-serif";
        mso-fareast-language:EN-US;}
@page WordSection1
        {size:612.0pt 792.0pt;
        margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
        {page:WordSection1;}
--></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-GB link=blue vlink=purple><div class=WordSection1><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>AVOCS 2013 Final Call for Papers <o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoPlainText>**********************************************************************<o:p></o:p></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>13<sup>th</sup> Automated Verification of Critical Systems (AVOCS) 2013 Workshop<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><a href="http://www.avocs2013.org.uk/"><span style='font-family:"Calibri","sans-serif";color:black'>http://www.avocs2013.org.uk</span></a><o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>11-13<sup>th</sup> September, 2013<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>University of Surrey, UK<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoPlainText>**********************************************************************<o:p></o:p></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>The aim of Automated Verification of Critical Systems (AVoCS) 2013 is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. The subject is to be interpreted broadly and inclusively. It covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving, abstract interpretation, and refinement pertaining to various types of critical systems which need to meet stringent dependability requirements (safety-critical, business-critical, performance-critical, etc). Contributions that describe different techniques, or industrial case studies are encouraged. The technical programme will consist of invited and contributed talks and also allow for short presentations of ongoing work. The workshop will be relatively informal, with an emphasis on discussion.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>There will be a few studentships available funded by Formal Methods Europe in order to support PhD students who present a paper at the workshop.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Topics include (but are not limited to)<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Model Checking<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Automatic and Interactive Theorem Proving<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    SAT, SMT or Constraint Solving for Verification<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Abstract Interpretation<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Specification and Refinement<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Requirements Capture and Analysis<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Verification of Software and Hardware<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Specification and Verification of Fault Tolerance and Resilience<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Probabilistic and Real-Time Systems<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Dependable Systems<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Verified System Development<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Industrial Applications<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Important Dates<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Submission (abstract for full paper): 31<sup>st</sup> May 2013<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Submission (full papers): 7<sup>th</sup> June 2013 <o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Notification (full papers): 12<sup>th</sup> July 2013<o:p></o:p></span></p><p class=MsoNormal style='text-indent:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Submission (short papers): 19<sup>nd</sup> July 2013<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Notification (short papers): 26<sup>th</sup> July 2013<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Registration deadline (including accommodation): 30<sup>th</sup> July 2013<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Submission of final versions: 5<sup>th</sup> August 2013<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Workshop: 11-13<sup>th</sup> September 2013<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>We will have two invited speakers, one on Applying Formal Methods and one on Inside Tools.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Submission Details<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Full Papers: Submissions of full papers to the workshop must not have been published or be concurrently considered for publication elsewhere. All submissions will be peer-reviewed and judged on the basis of originality, contribution to the field, technical and presentation quality, and relevance to the workshop. Final versions of the papers must be written in English and not exceed 15 pages (excluding the title page). Formatting details are provided on the website.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Short Contributions: AVoCS'13 encourages the submissions of short contributions in order to stimulate discussions at the workshop. Reports on ongoing work or surveys on work published elsewhere are welcome. The Programme Committee will select short contributions on the basis of submitted abstracts according to significance and general interest. Short contributions must be written in English and not exceed 2 pages (excluding the title page). <o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Conference Proceedings &amp; Special Journal Issue<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>At the workshop, pre-proceedings will be available in the form of a Surrey University Technical Report; this report will also include the short contributions.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>After the workshop, the authors of accepted full papers will have about one month in order to revise their papers for publication in the workshop post-proceedings which will appear in the Electronic Communications of the EASST Open Access Journal. Short papers will not be part of the proceedings in the Open Access Journal.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>We will invite authors of a selection of the best papers presented at the workshop to submit extended versions of their work for publication in a special issue of Elsevier's journal Science of Computer Programming.<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Program Committee<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Phil Brooke (University of Teeside, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Radu Calinescu (University of York, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Alessandro Fantechi (University of Florence, Italy)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Michael Goldsmith (University of Oxford, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Gudmund Grov (Heriot-Watt, Edinburgh, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Anne Haxthausen (TU, Denmark)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Constance Heitmeyer (Naval Research Laboratory, US)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Thai Son Hoang (ETH, Zurich)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Cliff Jones (Newcastle University, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Gerald Lüttgen (University of Bamberg, Germany)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Stephan Merz (INRIA Nancy &amp; LORIA, France)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Alice Miller (University of Glasgow, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Hoang Nga Nguyen (University of Swansea, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Jaco van de Pol (University of Twente, The Netherlands)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Kristin Yvonne Rozier, (NASA Ames Research Center, USA)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Markus Roggenbach (Swansea University, UK)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Marco Roveri (Fondazione Bruno Kessler, Italy)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Thomas Santen (Microsoft Research Aachen, Germany)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Steve Schneider (University of Surrey, UK, Co-Chair)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Helen Treharne (University of Surrey, UK, Co-Chair)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Laurent Voisin (Systerel, France)<o:p></o:p></span></p><p class=MsoNormal style='margin-left:1.0cm;text-autospace:none'><span style='font-family:"Courier New"'>Lijun Zhang (TU, Denmark)<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Steering Committee<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Michael Goldsmith (University of Oxford, UK)<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Stephan Merz (INRIA Nancy &amp; LORIA, F)<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>    Markus Roggenbach (Swansea University, UK)<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'>Organization Committee<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal style='text-indent:36.0pt;text-autospace:none'><span style='font-family:"Courier New"'>Helen Treharne<o:p></o:p></span></p><p class=MsoNormal style='text-indent:36.0pt;text-autospace:none'><span style='font-family:"Courier New"'>Steve Schneider<o:p></o:p></span></p><p class=MsoNormal style='text-autospace:none'><span style='font-family:"Courier New"'><o:p>&nbsp;</o:p></span></p><p class=MsoNormal><o:p>&nbsp;</o:p></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'> - - - - - - <o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'>Dr Helen Treharne<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'>Senior Lecturer<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'>Department of Computing<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'>University of Surrey<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'>GU2 7XH<o:p></o:p></span></p><p class=MsoNormal><span style='mso-fareast-language:EN-GB'>Phone: +44 1483 683161<o:p></o:p></span></p><p class=MsoNormal><o:p>&nbsp;</o:p></p></div></body></html>