<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. The two<BR>techniques seem contradictory: if you have proved your program, it′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.<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.<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. 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.<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>–––––––<BR>Possible topics include (as an indicative rather than exhaustive list):<BR><BR>– 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.<BR>– Generation of specifications by deduction<BR>– Verification techniques combining proofs and tests<BR>– Program proving with the aid of testing techniques<BR>– Transfer of concepts from testing to proving (e.g., coverage criteria)<BR>– Automatic bug finding<BR>– Formal frameworks<BR>– Tool descriptions and experience reports<BR>– Case studies<BR><BR>Invited speakers<BR>––––––––––––––––<BR>Boutheina CHETALI<BR>Security Labs, Technology & Innovation<BR>Gemalto – France<BR><BR>Sriram K. Rajamani<BR>Microsoft Research India<BR><BR>Contributions<BR>–––––––––––––<BR><BR>Two kinds of contributions are expected:<BR><BR>– 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. The research papers proceedings will be<BR>published in Springer′s LNCS series.<BR><BR>– Short presentations of work in progress, industrial<BR>experience reports and tool demonstrations. An extended<BR>abstract of not more than 3 pages is expected and will be<BR>reviewed. The accepted extended abstracts will be<BR>made available in supplementary proceedings. They will be<BR>presented during the conference days.<BR></PRE>
Abbrevation
TAP
City
Zurich
Country
Switzerland
Deadline Paper
Start Date
End Date
Abstract