Abbrevation
TAP
City
Zurich
Country
Switzerland
Deadline Paper
Start Date
End Date
Abstract

<PRE>To prove the correctness of a program is to demonstrate, through<BR>impeccable mathematical techniques, that it has no bugs; to test a<BR>program is to run it with the expectation of discovering bugs&#046; The two<BR>techniques seem contradictory: if you have proved your program, it&#8242;s<BR>fruitless to comb it for bugs; and if you are testing it, that is<BR>surely a sign that you have given up on any hope to prove its<BR>correctness&#046;<BR><BR>Accordingly, proofs and tests have, since the onset of software<BR>engineering research, been pursued by distinct communities using<BR>rather different techniques and tools&#046;<BR><BR>And yet the development of both approaches leads to the discovery of<BR>common issues and to the realization that each may need the other&#046; The<BR>emergence of model checking has been one of the first signs that<BR>contradiction may yield to complementarity, but in the past few years<BR>an increasing number of research efforts have encountered the need for<BR>combining proofs and tests, dropping earlier dogmatic views of<BR>incompatibility and taking instead the best of what each of these<BR>software engineering domains has to offer&#046;<BR><BR>The conference will include a mix of invited and submitted<BR>presentation, and a generous allocation of panels and informal<BR>discussions<BR><BR><BR>Topics<BR>&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;<BR>Possible topics include (as an indicative rather than exhaustive list):<BR><BR>&#8211; Generation of test data, oracles, or preambles by deductive<BR>techniques such as<BR>o theorem proving,<BR>o model checking,<BR>o symbolic execution,<BR>o constraint logic programming, etc&#046;<BR>&#8211; Generation of specifications by deduction<BR>&#8211; Verification techniques combining proofs and tests<BR>&#8211; Program proving with the aid of testing techniques<BR>&#8211; Transfer of concepts from testing to proving (e&#046;g&#046;, coverage criteria)<BR>&#8211; Automatic bug finding<BR>&#8211; Formal frameworks<BR>&#8211; Tool descriptions and experience reports<BR>&#8211; Case studies<BR><BR>Invited speakers<BR>&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;<BR>Boutheina CHETALI<BR>Security Labs, Technology &amp; Innovation<BR>Gemalto &#8211; France<BR><BR>Sriram K&#046; Rajamani<BR>Microsoft Research India<BR><BR>Contributions<BR>&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;&#8211;<BR><BR>Two kinds of contributions are expected:<BR><BR>&#8211; Research papers: full papers of not more than 14 pages<BR>in LNCS format, which have to be original, unpublished and<BR>not submitted elsewhere&#046; The research papers proceedings will be<BR>published in Springer&#8242;s LNCS series&#046;<BR><BR>&#8211; Short presentations of work in progress, industrial<BR>experience reports and tool demonstrations&#046; An extended<BR>abstract of not more than 3 pages is expected and will be<BR>reviewed&#046; The accepted extended abstracts will be<BR>made available in supplementary proceedings&#046; They will be<BR>presented during the conference days&#046;<BR></PRE>