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 E35E87EEAF for ; Tue, 29 Jan 2013 16:20:19 +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: AlgJAErnB1HAH1kG/2dsb2JhbAA6ChaDMwGoYwGRNIESc4IXKyEqBARFMAQdWAWFMAeCQQyfZJEUhyuJCY0UBAeDCWEDiGGNK4Edjy+DFYFI X-IPAS-Result: AlgJAErnB1HAH1kG/2dsb2JhbAA6ChaDMwGoYwGRNIESc4IXKyEqBARFMAQdWAWFMAeCQQyfZJEUhyuJCY0UBAeDCWEDiGGNK4Edjy+DFYFI X-IronPort-AV: E=Sophos;i="4.84,561,1355094000"; d="scan'208";a="382166" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail3-smtp-sop.national.inria.fr with SMTP; 29 Jan 2013 16:20:14 +0100 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id 2568C121596; Tue, 29 Jan 2013 10:20:18 -0500 (EST) To: caml-list@inria.fr Message-Id: <20130129152018.2568C121596@mcclellan.cs.miami.edu> Date: Tue, 29 Jan 2013 10:20:18 -0500 (EST) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] CADE-24 Workshop CFPs Call for Papers Workshops at CADE-24 -- Lake Placid, New York, 9-10 June, 2013 Short CFPs for the following CADE-24 workshops are attached: ADDCT - Automated Deduction: Decidability, Complexity, Tractability ARiSVe - Automated Reasoning in Software Verification ESARAI - Empirically Successful Automated Reasoning with AI KInAR - Knowledge Intensive Automated Reasoning PxTP - Proof Exchange for Theorem Proving StarExec For the following two CADE-24 workshops respective information will be distributed soon: Methods for Modalities (M4M), Automated Reasoning in Crypto-Protocol Analysis ===== ADDCT ========================================================== ADDCT - Automated Deduction: Decidability, Complexity, Tractability Decidability, and especially complexity and tractability of logical theories is extremely important for a large number of applications. Although general logical formalisms (such as predicate logic or number theory) are undecidable, decidable theories or decidable fragments thereof (sometimes even with low complexity) often occur in mathematics, in program verification, in the verification of reactive, real time or hybrid systems, as well as in databases and ontologies. It is therefore important to identify such decidable fragments and design efficient decision procedures for them. It is equally important to have uniform methods (such as resolution, rewriting, tableaux, sequent calculi, ...) which can be tuned to provide algorithms with optimal complexity. The goal of ADDCT is to bring together researchers interested in - identifying (fragments of) logical theories which are decidable, identifying fragments thereof which have low complexity, and analyzing possibilities of obtaining optimal complexity results with uniform tools; - analyzing decidability in combinations of theories and possibilities of combining decision procedures; - efficient implementations for decidable fragments; - application domains where decidability resp. tractability are crucial. Full Paper submission: March 26, 2013 Notification: April 26, 2013 Final versions: May 10, 2013 Workshop: June 10, 2013 More details: http://userpages.uni-koblenz.de/~sofronie/addct-2013/ ===== ARiSVe ========================================================= ARiSVe - Automated Reasoning in Software Verification The focus of the workshop is application of automated reasoning in the context of software verification, and, more generally, automation in software verification. Relevant topics include but are not limited to: - specifics of verification-related automated reasoning tasks; - efficient translation of high-level verification conditions to logical languages of automated reasoning tools; - handling of the prover's feedback: proofs, models, answer terms; - logical theories of interest for program verification, decision procedures, integration into existing ATP and SMT systems; - combination of automated and user-assisted verification; - tool presentations, tool comparisons, and benchmarks; - experience reports on verification of complex algorithms and real-life software with the use of automated reasoning tools. Invited speaker: K. Rustan M. Leino (Microsoft Research) Abstract submission deadline: March 8, 2013 Submission deadline: March 15, 2013 Notification: April 10, 2013 Camera ready versions due: May 10, 2013 Workshop: June 10, 2013 More details: http://arisve2013.lri.fr ===== ESARAI ========================================================= ESARAI - Empirically Successful Automated Reasoning with Artificial Intelligence The Empirically Successful Automated Reasoning with Artificial Intelligence (ESARAI) workshop will bring together two complementary groups of researchers: researchers in Automated Reasoning who employ Artificial Intelligence tools and techniques to support their automated reasoning research, and researchers in Artificial Intelligence who employ Automated Reasoning tools and techniques to support the artificial intelligence research. The workshop will offer mutually beneficial interactions, through the exposure of the two sides of the research to all. Additionally, the workshop will provide a focussed forum where the many interfaces between these two research fields can be presented and discussed. The workshop is soliciting research, position, applications and system description papers on combinations of AI and AR. Additionally, the workshop includes system and application demonstrations. Demonstrations of systems and applications described in paper presentations, and demonstrations of systems and applications without an accompanying paper, are both encouraged. Submission deadline - 22nd April Notification of acceptance - 13th May Final versions due - 20th May Workshop - 9th or 10th June More details: http://www.cs.miami.edu/~geoff/Conferences/ESARAI/ ===== KInAR ========================================================== KInAR - Knowledge Intensive Automated Reasoning Extensive digital sources of knowledge are becoming available, such as formal ontologies, databases, dictionaries and natural language reference works. Online sources like Wikipedia and IMDb, mathematical libraries like Mizar and various search engines and web services have gained widespread acceptance among the general population, but the sheer quantity of data can be an obstacle for human users. Automated reasoning (AR) systems have been advancing in their capabilities, and there is a growing interest in employing their deductive power to make digital knowledge more accessible. This poses challenges to AR research, but it is also a chance to bring AR into the public and to see large-scale usage of AR systems. In the KInAR workshop we aim to compile approaches to AR on large knowledge sources, and to aid the connections between researchers working on such projects. We invite submissions on any topics regarding KInAR, such as: - theoretical foundations: calculi for knowledge intensive reasoning, - knowledge corpora and their management, - extracting (semi-)formal knowledge from large informal corpora, - system descriptions of applications regarding the workshop topic, - benchmarking such systems, - robustness: reasoning despite flaws in digital knowledge, - combining knowledge from different sources. Submission deadline: 8 April 2013 Author notification: 2 May 2013 Camera-ready version: 9 May 2013 KInAR workshop: 10 June 2013 More details: http://userpages.uni-koblenz.de/~bpelzer/kinar2013 ===== PxTP =========================================================== PxTP - Proof Exchange for Theorem Proving The past decades have seen impressive advances in computer-aided reasoning, both in automated and interactive theorem proving. As shown by various system competitions, such as CASC, SMT-COMP, and the SAT competition, deduction tools are able to tackle larger problems progressively faster and are increasingly more applicable to a wider range of problems. In recent years, integration of such automated tools in larger verification environments has demonstrated the potential to reduce the amount of manual verification work. It is becoming clear that the success of deduction tools will not only depend on their power to solve large and difficult problems in an isolated manner, but it will also rely on their ability to cooperate, by exchanging problems, proofs, and models. The PxTP workshop aims at encouraging such cooperation by inviting contributions on various aspects of communication, integration, and cooperation between systems and formalisms. The workshop's mission is to facilitate building of complex reasoning applications and reuse of reasoning tools by developing and discussing suitable integration, translation and communication methods, standards, protocols, and application programming interfaces (APIs). The workshop would like to bring together the interested developers of automatic and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and APIs, and producers of standards and protocols. Submission of papers: 11 April 2013 Notification: 2 May 2013 Camera-ready versions due: 9 May 2013 Workshop: 10 June 2013 More details: http://www.cs.ru.nl/pxtp13/cfp.txt ===== StarExec ======================================================= StarExec The StarExec project is an NSF funded project to design, implement, and operate StarExec, a web service designed for the comparative evaluation of logic solvers (automated theorem provers) on benchmark problems. The $1.85 million budget of the grant is mostly dedicated to purchasing and operating a medium-sized cluster of an anticipated 150 compute nodes, which will be used to run jobs submitted by users of the system. We anticipate users will be members of various logic-solving subcommunities of the broader automated theorem proving community The StarExec 2013 workshop will bring together logic-solving community leaders, logic solver competition organizers, StarExec power users, and the StarExec organizers, to discuss the current status of the StarExec project. The workshop will have four sessions: - A status report from the StarExec organizers, and a demonstration of StarExec as it has been developed by the time of the workshop. - Use of StarExec by the attendees, so they can get a feeling of how well the implementation will meet their solver evaluation needs. - A feedback session based on the use of StarExec. - A presentation by the StarExec organizers on the short and medium terms plans for development and use of StarExec. StarExec 2013 will not invite papers or general attendance. Rather, the workshop will be aimed specifically at the types of researchers described above, to maximize the positive impact on the development and use of StarExec. The NSF grant will provide travel, accomodation, and registration support for 20 participants, 10 from the USA and 10 from overseas. More details: http://clc.cs.uiowa.edu/starexec13/