Skip to Content.
Sympa Menu

coq-club - [Coq-Club] 1 CFP Test And Proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 1 CFP Test And Proof


chronological Thread 
  • From: Burkhart Wolff <bwolff AT inf.ethz.ch>
  • To: <acl2 AT utlists.utexas.edu>, <agents AT csc.liv.ac.uk>, <agents AT cs.umbc.edu>, <ai AT cs.man.ac.uk>, <aiia AT di.unito.it>, <announcements AT lists.artist-embedded.org>, <arw-committee AT csc.liv.ac.uk>, <asl AT vassar.edu>, <calculemus-ig AT ags.uni-sb.de>, <cl-all AT coli.uni-sb.de>, <clean-list AT cs.kun.nl>, <cl-stud AT coli.uni-sb.de>, <concurrency AT cwi.nl>, <dl AT dl.kr.org>, <elsnet-list AT elsnet.org>, <elsnet-list AT let.uu.nl>, <coq-club AT inria.fr>, <finite-model-theory AT informatik.rwth-aachen.de>, <finite-model-theory AT lists.rwth-aachen.de>, <fmcad AT utlists.utexas.edu>, <fm-discussion AT cs.man.ac.uk>, <fmics AT inrialpes.fr>, <fm-info AT air16.larc.nasa.gov>, <fom AT cs.nyu.edu>, <haskell AT haskell.org>, <hol-info AT lists.sourceforge.net>, <img AT cs.man.ac.uk>, <isabelle-users AT cl.cam.ac.uk>, <kgs-list AT logic.at>, <ki-inf AT uni-koblenz.de>, <kr AT kr.org>, <laas-dependability-announce AT laas.fr>, <lfcs-interest AT dcs.ed.ac.uk>, <lics AT informatik.hu-berlin.de>, <lics AT research.bell-labs.com>, <list AT prooftheory.org>, <loco AT csc.liv.ac.uk>, <logic-announce AT uclink4.berkeley.edu>, <logic AT cs.stanford.edu>, <logic-list AT helsinki.fi>, <loginf AT lat.inf.tu-dresden.de>, <math.logik AT gmx.net>, <metaprl AT metaprl.org>, <mizar-forum AT mizar.uwb.edu.pl>, <mowgli-dev AT cs.unibo.it>, <newsletter AT aarinc.org>, <om-announce AT openmath.org>, <omdoc AT mathweb.org>, <petrinet AT informatik.uni-hamburg.de>, <plt-scheme AT slow.flux.utah.edu>, <prog-lang AT diku.dk>, <puml-list AT cs.york.ac.uk>, <pvs AT csl.sri.com>, <relmics-l AT mcmaster.ca>, <rewriting AT ens-lyon.fr>, <senseval-discuss AT listserv.hum.gu.se>, <sig-charme AT dcs.gla.ac.uk>, <sigparse-list AT lists.andrew.cmu.edu>, <synalp AT inrialpes.fr>, <theorem-provers AT ai.mit.edu>, <theory-a AT listserv.nodak.edu>, <theory-logic AT cs.cmu.edu>, <theorynt AT listserv.nodak.edu>, <twelf-list AT twelf.org>, <types-announce AT lists.seas.upenn.edu>, <vdm-forum AT jiscmail.ac.uk>, <w3c-math-wg AT w3.org>, <zforum AT prg.ox.ac.uk>
  • Subject: [Coq-Club] 1 CFP Test And Proof
  • Date: Tue, 16 Nov 2010 12:42:12 +0100

Apologies for multiple copies ...

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    CALL FOR PAPERS
     5th International Conference on Tests and Proofs (TAP 2011)
      http://www.tap2011.informatik.uni-bremen.de/
      June 30 - July 1, 2011, Zuerich, Switzerland
      Part of the TOOLS Federated Conferences 2011

The TAP conference is devoted to the convergence of proofs and tests, to
the application of techniques from both sides and their combination for
the advancement of software quality. Test and Proof seem to be
contradictory techniques: if you have proved your program, it's
fruitless to comb it for bugs; and if you are testing it, that is surely
a sign that you have given up on any hope to prove its correctness.
Accordingly, proofs and tests have, since the onset of software
engineering research, been pursued by distinct communities.

However, the development of both approaches lead to the discovery of
common issues and to the realization that each may need the other. The
emergence of model checking has been one of the first signs that
contradiction may yield to complementarity. Further evidence give
test data generation techniques from models or programs boil down to
constraint resolution techniques for relatively large formula; the
advent of powerful SMT solvers have therefore powered new testing
techniques.  Finally, since formal, proof-based verification is costly,
testing invariants and background theories can be helpful to detect
errors early and to improve cost effectivity.  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 panels and informal discussions.

Topics of interest include (other topics related to TAP are welcome):
- 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
- Formal frameworks
- Tool descriptions and experience reports
- Case studies combining tests and proofs

Abstract submission: February 04, 2011
Paper submission: February 11, 2011
Notification: March 14, 2011
Camera ready version: March 28, 2011
TAP conference: June 30 - July 01, 2011
TOOLS conferences (TOOLS, ICMT, SC, TAP): June 27 - July 01, 2011
Conference Chairs: Yuri Gurevich, Bertrand Meyer
Program Chairs: Martin Gogolla, Burkhart Wolff
Publication Chair: Gordon Fraser
Web Chair: Lars Hamann

Program Committee (to be finalized; acceptance for few names pending):
 Nazareno Aguirre, Bernhard K. Aichernig, Paul Ammann, Benoit Baudry,
 Dirk Beyer, Nikolaj Bjoerner, Achim Brucker, Koen Claessen, Robert
 Clariso, John A. Clark, Marco Comini, Catherine Dubois, Gordon
 Fraser, Carlo Alberto Furia, Angelo Gargantini, Arnaud Gotlieb,
 Reiner Haehnle, Bart Jacobs, Thierry Jeron, Gregory Kapfhammer,
 Nikolai Kosmatov, Victor Kuliamin, Karl Meinke, Antoni Olive, Holger
 Schlingloff, T.H. Tse, Margus Veanes.

Submissions (via http://www.tap2011.informatik.uni-bremen.de/):
- Research papers: full papers with at most 16 pages in LNCS format
 (pdf), which have to be original, unpublished and not submitted
 elsewhere.
- 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.

Accepted papers will be published in the Springer LNCS series (details
to be confirmed) and will be available at the conference. The program
chairs are negotiating with journals about a special issue dedicated to
extended versions of selected conference papers.

The contents of previous TAP proceedings is available at:
http://www.informatik.uni-trier.de/~ley/db/conf/tap/

------------------------------------------------------------------------



Archive powered by MhonArc 2.6.16.

Top of Page