TAP 2014
8th International Conference on TESTS AND PROOFS
Scope
=====
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 orthogonal techniques: once a program
has been proven to be correct then additional testing seems
pointless; however, when such a proof in not feasible, then
testing the program seems to be the only option. This view
has dominated the research community for a long time, and has
resulted in distinct communities pursuing the different
research areas.
The development of both approaches has led to the discovery of
common issues and to the realization of potential synergy.
Perhaps, the 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 by offering
a generous forum for the presentation of ongoing research,
for tutorials on established technologies and for informal discussions.
Topics of Interest
==================
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
- 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
- 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
- Testing of verification environments and reasoning engines like solvers and theorem provers
- New approaches such as crowd-sourcing and serious games to infer intended semantics and assess correctness
- Formal frameworks
- Tool descriptions and experience reports
Important Dates:
================
Abstract submission: February 25, 2014
Paper submission: March 1, 2014
Notification: April 28, 2014
Camera ready version: May 12, 2014
TAP conference: July 24-25, 2014
Program Chairs:
===============
Martina Seidl (JKU Linz/TU Wien, Austria)
Nikolai Tillmann (Microsoft Research, USA)
Program Committee:
==================
Arnaud Gotlieb
Dirk Beyer
Achim D. Brucker
Robert Clarisó
Marco Comini
Catherine Dubois
Juhan Ernits
Gordon Fraser
Angelo Gargantini
Christoph Gladisch
Martin Gogolla
Reiner Hähnle
Bart Jacobs
Thierry Jéron
Jacques Julliand
Gregory Kapfhammer
Nikolai Kosmatov
Victor Kuliamin
Karl Meinke
Alexandre Petrenko
Holger Schlingloff
Martina Seidl
Nikolai Tillmann
T.H. Tse
Margus Veanes
Luca Viganò
Burkhart Wolff
Fatiha Zaidi
Submission:
===========
Please submit your papers via easychair
https://www.easychair.org/conferences/?conf=tap2014
TAP 2014 will accept two types of papers and also tutorials:
- Research papers: full papers with at most 16 pages in LNCS format
(pdf), which have to be original, unpublished and not submitted
elsewhere. Research papers should clearly describe the addressed
problem, the relevant state-of-the-art, the scientifically-founded
solution, and the benefits of the presented approach.
- 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.
The same evaluation criteria apply to short papers as to full
research papers. Short papers will be reviewed to the same
standards of quality as full research papers.
- Tutorials: TAP 2014 further invites one-hour tutorial presentations
surveying the state-of-the-art of any research field related
to the topics of TAP. Tutorial proposals shall have a maximum
length of 3 pages in LNCS format (pdf) and provide information
about the content, a short outline, and information about the
speakers.
Accepted full and short papers will be published in the Springer LNCS
series and will be available at the conference. Accepted tutorials
will be assigned a slot of 60 minutes during the conference.
The contents of previous TAP proceedings is available at:
http://www.informatik.uni-trier.de/~ley/db/conf/tap/tap2013.html
Submitted by Anonymous
on
8th International Conference on TESTS AND PROOFS
Scope
=====
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 orthogonal techniques: once a program
has been proven to be correct then additional testing seems
pointless; however, when such a proof in not feasible, then
testing the program seems to be the only option. This view
has dominated the research community for a long time, and has
resulted in distinct communities pursuing the different
research areas.
The development of both approaches has led to the discovery of
common issues and to the realization of potential synergy.
Perhaps, the 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 by offering
a generous forum for the presentation of ongoing research,
for tutorials on established technologies and for informal discussions.
Topics of Interest
==================
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
- 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
- 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
- Testing of verification environments and reasoning engines like solvers and theorem provers
- New approaches such as crowd-sourcing and serious games to infer intended semantics and assess correctness
- Formal frameworks
- Tool descriptions and experience reports
Important Dates:
================
Abstract submission: February 25, 2014
Paper submission: March 1, 2014
Notification: April 28, 2014
Camera ready version: May 12, 2014
TAP conference: July 24-25, 2014
Program Chairs:
===============
Martina Seidl (JKU Linz/TU Wien, Austria)
Nikolai Tillmann (Microsoft Research, USA)
Program Committee:
==================
Arnaud Gotlieb
Dirk Beyer
Achim D. Brucker
Robert Clarisó
Marco Comini
Catherine Dubois
Juhan Ernits
Gordon Fraser
Angelo Gargantini
Christoph Gladisch
Martin Gogolla
Reiner Hähnle
Bart Jacobs
Thierry Jéron
Jacques Julliand
Gregory Kapfhammer
Nikolai Kosmatov
Victor Kuliamin
Karl Meinke
Alexandre Petrenko
Holger Schlingloff
Martina Seidl
Nikolai Tillmann
T.H. Tse
Margus Veanes
Luca Viganò
Burkhart Wolff
Fatiha Zaidi
Submission:
===========
Please submit your papers via easychair
https://www.easychair.org/conferences/?conf=tap2014
TAP 2014 will accept two types of papers and also tutorials:
- Research papers: full papers with at most 16 pages in LNCS format
(pdf), which have to be original, unpublished and not submitted
elsewhere. Research papers should clearly describe the addressed
problem, the relevant state-of-the-art, the scientifically-founded
solution, and the benefits of the presented approach.
- 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.
The same evaluation criteria apply to short papers as to full
research papers. Short papers will be reviewed to the same
standards of quality as full research papers.
- Tutorials: TAP 2014 further invites one-hour tutorial presentations
surveying the state-of-the-art of any research field related
to the topics of TAP. Tutorial proposals shall have a maximum
length of 3 pages in LNCS format (pdf) and provide information
about the content, a short outline, and information about the
speakers.
Accepted full and short papers will be published in the Springer LNCS
series and will be available at the conference. Accepted tutorials
will be assigned a slot of 60 minutes during the conference.
The contents of previous TAP proceedings is available at:
http://www.informatik.uni-trier.de/~ley/db/conf/tap/tap2013.html