[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] TAP 2013: 2nd Call for Papers

(Apologies if you receive this announcement multiple times.)



***                                              ***

***  TAP 2013                                    ***

***                                              ***

***  Abstract submission: January 25, 2013       ***

***  Paper submission:    February 1, 2013       ***


***  TAP 2013 solicits both full papers and      ***

***  (industrial) experience/tool papers         ***

***  in combining proofs and (security) testing  ***









Budapest, Hungary, June 18-19, 2013


The TAP conference is devoted to the synergy of proofs and tests, to the

application of techniques from both sides and their combination for the

advancement of software quality.

Testing and proving seem to be contradictory techniques: once you have

proved your program to be correct then additional testing seems

pointless; on the other hand, when such a proof in not feasible, then

testing the program seems to be the only option. This view has dominated

the research community since the dawn of computer science, and has

resulted in distinct communities pursuing the seemingly orthogonal

research areas.


However, the development of both approaches has lead to the discovery of

common issues and to the realization of potential synergy. Perhaps, use

of model checking in testing was one of the first signs that a

counterexample to a proof may be interpreted as a test case. Recent

breakthroughs in deductive techniques such as satisfiability modulo

theories, abstract interpretation, and interactive theorem proving, have

paved the way for new and practically effective methods of powering

testing techniques. Moreover, since formal, proof-based verification is

costly, testing invariants and background theories can be helpful to

detect errors early and to improve cost effectiveness. Summing up, in

the past few years an increasing number of research efforts have

encountered the need for combining proofs and tests, dropping earlier

dogmatic views of incompatibility and taking instead the best of what

each of these software engineering domains has to offer.


The TAP conference aims to bring together researchers and practitioners

working in the converging fields of testing and proving, and will offer

a generous allocation of papers, panels and informal discussions.


Topics of interest cover theory definitions, tool constructions and

experimentations, and include (other topics related to TAP are welcome):

- Bridging the gap between concrete and symbolic techniques, e.g. using

  proof search in satisfiability modulo theories solvers to enhance

  various testing techniques

- Transfer of concepts from testing to proving (e.g., coverage criteria)

  and from proving to testing

- Program proving with the aid of testing techniques

- New problematics in automated reasoning emerging from specificities of

  test generation

- Verification and testing techniques combining proofs and tests

- Generation of test data, oracles, or preambles by deductive techniques

  such as: theorem proving, model checking, symbolic execution,

  constraint logic programming

- Model-based testing and verification

- Generation of specifications by deduction

- Automatic bug finding

- Debugging of programs combining static and dynamic analysis

- Formal frameworks

- Tool descriptions and experience reports

- Case studies combining tests and proofs

- Domain specific applications of testing and proving to new application

  domains such as validating security protocols, vulnerability detection

  of programs, security


Important Dates:


Abstract submission:   January 25, 2013

Paper submission:      February 1, 2013

Notification:          March 3, 2013

Camera ready version:  April 5, 2013

TAP conference:        June 17-21, 2013


Program Chairs:


Margus Veanes (Microsoft Research, USA)

Luca Vigano` (University of Verona, Italy)


Program Committee:


Paul Ammann

Dirk Beyer

Achim D. Brucker

Robert Clarisò

Marco Comini

Catherine Dubois

Gordon Fraser

Angelo Gargantini

Christoph Gladisch

Martin Gogolla

Arnaud Gotlieb

Wolfgang Grieskamp

Reiner Hähnle

Bart Jacobs

Thiérry Jeron

Jacques Julliand

Gregory Kapfhammer

Nikolai Kosmatov

Victor Kuliamin

Michael Leuschel

Karl Meinke

Alexandre Petrenko

Holger Schlingloff

T.H. Tse

Margus Veanes (co-chair)

Luca Viganò (co-chair)

Burkhart Wolff

Fatiha Zaidi




Please submit your papers via easychair



TAP 2013 will

accept two types of papers:


- Research papers: full papers with at most 16 pages in LNCS format

  (pdf), which have to be original, unpublished and not submitted



- Short contributions: work in progress, (industrial) experience

  reports or tool demonstrations, position statements; an extended

  abstract with at most 6 pages in LNCS format (pdf) is expected.


Subject to final approval by Springer, accepted papers will be published

in the Springer LNCS series and will be available at the conference.


The contents of previous TAP proceedings is available at: