<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 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:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-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;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri","sans-serif";
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-family:"Calibri","sans-serif";}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
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-US" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-family:"Courier New"">(Apologies if you receive this announcement multiple times.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:"Courier New"">We also apologize for resending the first call for papers,
<br>
the original announcement contained an incorrect URL to easychair.)<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">****************************************************<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** ***<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** TAP 2013 ***<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** ***<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** Abstract submission: January 25, 2013 ***<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** Paper submission: February 1, 2013 ***<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">****************************************************<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** TAP 2013 solicits both full papers and ***<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** (industrial) experience/tool papers ***
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">*** in combining proofs and (security) testing ***
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">****************************************************<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">CALL FOR PAPERS<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">7th INTERNATIONAL CONFERENCE ON TESTS AND PROOFS (TAP 2013)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><a href="http://www.spacios.eu/TAP2013"><span style="color:blue">http://www.spacios.eu/TAP2013</span></a>
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> <o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Budapest, Hungary, June 17-21, 2013<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">The TAP conference is devoted to the synergy of proofs and tests, to the<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">application of techniques from both sides and their combination for the<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">advancement of software quality.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Testing and proving seem to be contradictory techniques: once you have<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">proved your program to be correct then additional testing seems<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">pointless; on the other hand, when such a proof in not feasible, then<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">testing the program seems to be the only option. This view has dominated<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">the research community since the dawn of computer science, and has<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">resulted in distinct communities pursuing the seemingly orthogonal<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">research areas.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">However, the development of both approaches has lead to the discovery of<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">common issues and to the realization of potential synergy. Perhaps, use<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">of model checking in testing was one of the first signs that a<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">counterexample to a proof may be interpreted as a test case. Recent<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">breakthroughs in deductive techniques such as satisfiability modulo<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">theories, abstract interpretation, and interactive theorem proving, have<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">paved the way for new and practically effective methods of powering<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">testing techniques. Moreover, since formal, proof-based verification is<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">costly, testing invariants and background theories can be helpful to<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">detect errors early and to improve cost effectiveness. Summing up, in<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">the past few years an increasing number of research efforts have<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">encountered the need for combining proofs and tests, dropping earlier<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">dogmatic views of incompatibility and taking instead the best of what<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">each of these software engineering domains has to offer.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">The TAP conference aims to bring together researchers and practitioners<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">working in the converging fields of testing and proving, and will offer<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">a generous allocation of papers, panels and informal discussions.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Topics of interest cover theory definitions, tool constructions and<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">experimentations, and include (other topics related to TAP are welcome):<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Bridging the gap between concrete and symbolic techniques, e.g. using<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> proof search in satisfiability modulo theories solvers to enhance<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> various testing techniques<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Transfer of concepts from testing to proving (e.g., coverage criteria)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> and from proving to testing<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Program proving with the aid of testing techniques<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- New problematics in automated reasoning emerging from specificities of<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> test generation<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Verification and testing techniques combining proofs and tests<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Generation of test data, oracles, or preambles by deductive techniques<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> such as: theorem proving, model checking, symbolic execution,<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> constraint logic programming<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Model-based testing and verification<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Generation of specifications by deduction<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Automatic bug finding<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Debugging of programs combining static and dynamic analysis<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Formal frameworks<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Tool descriptions and experience reports<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Case studies combining tests and proofs<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Domain specific applications of testing and proving to new application<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> domains such as validating security protocols, vulnerability detection<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> of programs, security<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </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></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Abstract submission: January 25, 2013<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Paper submission: February 1, 2013<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Notification: March 3, 2013<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Camera ready version: April 5, 2013<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">TAP conference: June 17-21, 2013<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Program Chairs:
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">===============<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Margus Veanes (Microsoft Research, USA)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Luca Vigano` (University of Verona, Italy)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </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></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">TBA<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Submission:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">===========<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Please submit your papers via easychair
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><a href="https://www.easychair.org/conferences/?conf=tap2013"><span style="color:blue">https://www.easychair.org/conferences/?conf=tap2013</span></a>
<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">(submission page to be opened in due time)<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">TAP 2013 will<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">accept two types of papers:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Research papers: full papers with at most 16 pages in LNCS format<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> (pdf), which have to be original, unpublished and not submitted<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> elsewhere.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">- Short contributions: work in progress, (industrial) experience<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> reports or tool demonstrations, position statements; an extended<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""> abstract with at most 6 pages in LNCS format (pdf) is expected.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">Subject to final approval by Springer, accepted papers will be published<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">in the Springer LNCS series and will be available at the conference.<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><o:p> </o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New"">The contents of previous TAP proceedings is available at:<o:p></o:p></span></p>
<p class="MsoNormal" style="text-autospace:none"><span style="font-family:"Courier New""><a href="http://www.informatik.uni-trier.de/~ley/db/conf/tap/"><span style="color:blue">http://www.informatik.uni-trier.de/~ley/db/conf/tap/</span></a>
<o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>