From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 45B837EE48 for ; Fri, 20 Feb 2015 15:59:31 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of geoff@cs.miami.edu) identity=pra; client-ip=192.31.89.6; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of geoff@cs.miami.edu designates 192.31.89.6 as permitted sender) identity=mailfrom; client-ip=192.31.89.6; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mcclellan.cs.miami.edu) identity=helo; client-ip=192.31.89.6; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="postmaster@mcclellan.cs.miami.edu"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CLAgCQS+dUnAZZH8Bbg1haAYI4sQcBjQmCIAqHTgEBAQEBARABAQEBAQgUCUKEMyEqPBEwBB07HYgbDaw0oyeFGZIxDEAdgRQFikeIY4VkgRo4gluLQYM+giQcgW4gMoEDJIEbAQEB X-IPAS-Result: A0CLAgCQS+dUnAZZH8Bbg1haAYI4sQcBjQmCIAqHTgEBAQEBARABAQEBAQgUCUKEMyEqPBEwBB07HYgbDaw0oyeFGZIxDEAdgRQFikeIY4VkgRo4gluLQYM+giQcgW4gMoEDJIEbAQEB X-IronPort-AV: E=Sophos;i="5.09,615,1418079600"; d="scan'208";a="100765982" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail3-smtp-sop.national.inria.fr with SMTP; 20 Feb 2015 15:59:06 +0100 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id 2CF2B12144A; Fri, 20 Feb 2015 09:59:06 -0500 (EST) To: caml-list@inria.fr Message-Id: <20150220145906.2CF2B12144A@mcclellan.cs.miami.edu> Date: Fri, 20 Feb 2015 09:59:06 -0500 (EST) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] TESTS AND PROOFS - Deadline extended **************************************************** * * 9th International Conference * on * TESTS AND PROOFS (TAP 2015) * * http://tap2015.in.tum.de/ * * Part of STAF 2015, L'Aquila, Italy, July 20-24, 2015 * http://www.disim.univaq.it/staf2015/ * **************************************************** * * Call for Papers * * Abstract submission: February 23, 2015 (extended) * Paper submission: February 27, 2015 (extended) * **************************************************** 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 among others: - 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 23, 2015 (extended) Paper submission: February 27, 2015 (extended) Notification: April 13, 2015 Camera-ready version: May 3, 2015 STAF conferences: July 20-24, 2015 Program Co-Chairs: =============== Jasmin C. Blanchette (TU Muenchen, Inria) Nikolai Kosmatov (CEA LIST) Program Committee: ================== Bernhard K. Aichernig Dirk Beyer Nikolaj Bjorner Jasmin C. Blanchette Achim D. Brucker Koen Claessen Robert Clariso Marco Comini Catherine Dubois Juhan Ernits Gordon Fraser Angelo Gargantini Christoph Gladisch Martin Gogolla Arnaud Gotlieb Reiner Haehnle Bart Jacobs Thierry Jeron Jacques Julliand Gregory Kapfhammer Nikolai Kosmatov Victor Kuliamin Panagiotis Manolios Karl Meinke Alexandre Petrenko Andrew Reynolds Martina Seidl Nikolai Tillmann T.H. Tse Margus Veanes Luca Vigano Burkhart Wolff Fatiha Zaidi Submission: =========== Please submit your papers via EasyChair: https://www.easychair.org/conferences/?conf=tap2015