[ecoop-info] CfPart: TAP 2010 - 4th International Conference on Tests and Proofs

Gordon Fraser fraser at cs.uni-saarland.de
Thu Apr 29 13:40:19 CEST 2010


TAP 2010: 4th International Conference on Tests and Proofs

July 1-2, 2010, Malaga, Spain


Part of TOOLS Federated Conferences 2010:
TOOLS Europe 2010, SC 2010, ICMT 2010, TAP 2010

We would like to heartily invite you to participate in the 4th
International Conference on Tests and Proofs. The TAP conference is
devoted to the convergence of proofs and tests.  It combines ideas
from both sides for the advancement of software quality.

About Tests and Proofs:
To prove the correctness of a program is to demonstrate, through
impeccable mathematical techniques, that it has no bugs; to test a
program is to run it with the expectation of discovering bugs. The two
techniques seem contradictory: 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

Accordingly, proofs and tests have, since the onset of software
engineering research, been pursued by distinct communities using
rather different techniques and tools.

And yet the development of both approaches leads 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, but 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.

Registration is handled by the TOOLS Conference series. Registration and
accommodation details can be found at:


Early registration runs until May 28. On-line registration will be
open until June 23, 2010. After that day, only on-site registration
will be possible.

Keynote Speakers:
Michael Ernst, University of Washington, USA
Nachi Nagappan, Microsoft Research, USA


July 1, 2010

09:00 -- Opening

09:05 -- Keynote: Mike Ernst
      How Tests and Proofs Impede One Another: The Need for Always-On
      Static and Dynamic Feedback

10:30 -- Break

11:00 -- Session 1: Shared Session with TOOLS Europe

 * Phillip Heidegger, Peter Thiemann. JSConTest: Contract-Driven
   Testing of JavaScript Code (TOOLS)

 * Jonathan de Halleux, Nikolai Tillmann: Moles: tool-assisted
   environment isolation with closures (TOOLS)

 * Koen Claessen, Nicholas Smallbone and John Hughes. QuickSpec:
   Guessing Formal Specifications using Testing (TAP)

12:30 -- Lunch

14:30 -- Session 2: "Testing Proofs"

 * Ki Yung Ahn and Ewen Denney. Testing First-Order Logic Axioms in
   Program Verification

 * Martin Gogolla, Lars Hamann and Mirco Kuhlmann. Proving OCL
   Invariant Independence by Automatically Generated Test Cases

 * Lydie du Bousquet and Michel Levy. Proof process evaluation with
   mutation analysis

16:00 -- Break

16:30 -- Session 3: "Test Generation using Proof Techniques"

 * Christoph Gladisch, Shmuel Tyszberowicz, Bernhard Beckert and
   Amiram Yehudai. Generating Regression Unit Tests using a
   Combination of Verification and Capture & Replay

 * Suresh Thummalapenta, Jonathan Halleux, Nikolai Tillmann and Scott
   Wadsworth. DyGen: Automatic Generation of High-Coverage Tests via
   Mining Gigabytes of Dynamic Traces

 * Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti and Jacques
   Julliand. Combining Static Analysis and Test Generation for C
   Program Debugging

July 2, 2010

09:00 -- SC Shared Keynote: Valérie Issarny
      From Middleware to on the Fly Connector Synthesis for the
      Dynamic Composition of Pervasive Software Intensive Networked Systems

10:30 -- Break

11:00 -- Keynote: Nachiappan Nagappan
      Myths in Software Engineering: From the Other Side

12:30 -- Lunch

14:30 -- Session 3 (continued): "Test Generation using Proof Techniques"

 * Eugene Goldberg and Panagiotis Manolios. Generating High Quality
Tests for Boolean Circuits by Treating Tests as Proof Encodings

15:00 -- Session 4: "Theorem Proving and Testing"

 * Jasmin Christian Blanchette. Relational Analysis of (Co)inductive
   Predicates, (Co)algebraic Datatypes, and (Co)recursive Functions

 * Vlad Rusu. Combining narrowing and theorem proving for
   rewriting-logic specifications

16:00 -- Break

16:30 -- Session 5: "Abstraction"

 * Jacques Julliand, Nicolas Stouls, BUE Pierre-christophe and
   Pierre-Alain Masson. Syntactic Abstraction of B Models to Generate

 * Pierre-Christophe Bue, Frederic Dadeau, Adrien de Kermadec and
   Fabrice Bouquet. Building a test-ready abstraction of a behavioral
   model using CLP

17:30 -- Discussion + closing

Conference Chairs:
Yuri Gurevich, Microsoft Research, USA
Bertrand Meyer, ETH Zuerich, Switzerland

Program Chairs:
Gordon Fraser, Saarland University, Germany
Angelo Gargantini, University of Bergamo, Italy

Program Committee:
Bernhard K. Aichernig, Graz University of Technology, Austria
Paul Ammann, George Mason University, USA
Bernhard Beckert, University of Koblenz, Germany
Dirk Beyer, Simon Fraser University, Canada
Koen Claessen, Chalmers University of Technology, Sweden
John Clark, University of York, UK
Catherine Dubois, ENSIIE, Evry, France
Carlo Furia, ETH Zuerich, Switzerland
Patrice Godefroid, Microsoft Research, USA
Martin Gogolla, University of Bremen, Germany
Arnaud Gotlieb, IRISA, France
Reiner Haehnle, Chalmers University of Technology, Sweden
Bart Jacobs, Katholieke Universiteit Leuven, Belgium
Victor Kuliamin, Russain Academy of Sciences, Russia
Karl Meinke, KTH Royal Institute of Technology, Sweden
Manuel Nunez, Universidad Complutense de Madrid, Spain
Sam Owre, SRI International, USA
Doron Peled, Bar Ilan University, Israel
Wolfram Schulte, Microsoft Research, USA
Yannis Smaragdakis, University of Massachusetts, USA
Assia Touil, Supelec, France 
T.H. Tse, University of Hong Kong, China 


More information about the ecoop-info mailing list