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 B63D57FA5F for ; Thu, 19 Jan 2017 15:13:35 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=geoff@cs.miami.edu; spf=Pass smtp.mailfrom=geoff@cs.miami.edu; spf=None smtp.helo=postmaster@mcclellan.cs.miami.edu 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 IronPort-PHdr: =?us-ascii?q?9a23=3AzwU4ExE7Gh1vWQsruVcG9p1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78oMywAkXT6L1XgUPTWs2DsrQf2raQ7/mrBDFIyK3CmUhKSIZLWR4BhJ?= =?us-ascii?q?detC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+?= =?us-ascii?q?KPjrFY7OlcS30P2594HObwlSijewZbx/IA+5oAnMucUbgYtvIbstxxXUpXdFZ/?= =?us-ascii?q?5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnM?= =?us-ascii?q?VhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1ji?= =?us-ascii?q?oMKjw3/3zNisFokqxVvRGvqRJ/zYPPfI2ZKOZycr/Bcd8GWWZMWNtaWSxbAoO7?= =?us-ascii?q?aosCF+UBMvhfr4nzqVsDtgexBRK2COPqyz9HnHr23awg3+s/DA7GwRErE9YPvn?= =?us-ascii?q?vKq9X1OqkSWv2owqnV0TXMc/dW2Tbz6IjGbB8tpPeBVq9+f8rWzEkgDQLFjlOI?= =?us-ascii?q?pIzgJzOV2f4BvHWF4OZ4TuKvk3QnqwB3ojig2MgskJPFiZ4SylDB7Sl23pw6Jc?= =?us-ascii?q?a4SUFnYd6rCppQtzuAO4txWMMiTGdlszs5xL0eoZO3YSwHxIo9yxPRdvCLaYuF?= =?us-ascii?q?7xb5WOuQJzpzmWhrd6ilhxmo9Eit0u38Wdew0FZNtidFl8XDuWwJ1xPN7siHTu?= =?us-ascii?q?Fy/kG71TmTzADf8OREIUEumqreKp4t2KA/mYcOsUjbHy/2nlv5jLOOe0k5/uWk?= =?us-ascii?q?9f7rb7v7qpOGNIJ5jhvyP6U2lsy6G+s4MwwOX2aB+eS70b3u5UL5T6tNjv04nK?= =?us-ascii?q?nUq4zVJd8Bqq68Ag9ayIMj6xelAzi4zdsYgGELLEhZdxKfk4jpJ1bOLejkAvil?= =?us-ascii?q?hlSslC5nx/THPr36HpXANWPDkbfkfbZl8UFQ0gszzdZF55JVEL4NOvzzWlWi/O?= =?us-ascii?q?DfWxQwNgjxx+f8FP180JkfUCSBGPy3KqTX5FCF4ewhC+KXIooUsTP8bfUp+rau?= =?us-ascii?q?onI+l1FVRrS11p8WZn61X6c1a36FaGbh149SWVwBuRAzGbTn?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DpCACWyIBY/wZZH8BeHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBgxQBAQEBAX+EDJ83AZJNggwBK4JAhXYXAQEBAQEBAQEBAQFiKII?= =?us-ascii?q?zGYJBISpNMAQdiUcOn1ySJogIB4IwMo5FhAkMW4IxBZAnix2GYYMYh1+CBIUPi?= =?us-ascii?q?WiScCEBNYFIhyIgihkBAQE?= X-IPAS-Result: =?us-ascii?q?A0DpCACWyIBY/wZZH8BeHAEBBAEBCgEBFwEBBAEBCgEBgxQ?= =?us-ascii?q?BAQEBAX+EDJ83AZJNggwBK4JAhXYXAQEBAQEBAQEBAQFiKIIzGYJBISpNMAQdi?= =?us-ascii?q?UcOn1ySJogIB4IwMo5FhAkMW4IxBZAnix2GYYMYh1+CBIUPiWiScCEBNYFIhyI?= =?us-ascii?q?gihkBAQE?= X-IronPort-AV: E=Sophos;i="5.33,254,1477954800"; d="scan'208";a="209961451" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail3-smtp-sop.national.inria.fr with SMTP; 19 Jan 2017 15:13:34 +0100 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id C341812150A; Thu, 19 Jan 2017 09:13:33 -0500 (EST) To: caml-list@inria.fr Message-Id: <20170119141333.C341812150A@mcclellan.cs.miami.edu> Date: Thu, 19 Jan 2017 09:13:33 -0500 (EST) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] JAR Special Issue on Automated Reasoning Systems =============================================================================== CALL FOR PAPERS Journal of Automated Reasoning Special Issue On Automated Reasoning Systems The past few decades have seen major developments and practical achievements in automated reasoning systems. For example, SAT solving has become an inherent part of the standard hardware production process; SMT solvers are now the backbone of most software verification techniques; first-order theorem provers have pushed the productivity of interactive theorem proving to a new level; computer algebra systems have solved difficult problems in mathematics and biology; knowledge representation systems have become indispensable for reasoning in the world wide web; automatic termination checkers routinely prove the termination of complex programs. This special issue is dedicated to automated reasoning systems in their full variety along the following dimensions: 1) considered logic: propositional (including (D)QBF), first-order modulo theories, modal, temporal, decidable fragments of larger logics, FOL, and HOL, ...; 2) considered problem: satisfiability, interpolation, quantifier elimination, consequence finding, model building, reachability, termination, ...; 3) application area: formal methods, artificial intelligence, mathematics, biology, product development, security, ...; 4) user base: academic, educational, or industrial. In particular, we welcome papers emphasizing engineering aspects because, while often crucial for the success of automated reasoning tools, they are typically not given a sufficiently detailed treatment in theory papers or system description papers published at conferences or workshops. We welcome full-length papers describing past work not previously published in a journal as well as papers of any length describing new developments. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are also eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. We encourage submissions that include most, if not all, of the following: (i) theory details (ii) implementation details (iii) applications, and (iv) experiments. Papers should be in PDF format, following the JAR guidelines for authors, http://www.springer.com/computer/theoretical+computer+science/journal/10817 and be submitted using EasyChair: https://easychair.org/conferences/?conf=jars2017 To encourage a speedy review cycle, we will expect authors of submissions to serve as referees for other submissions as needed. Important Dates 3 Apr 2017 Submission deadline 1 Nov 2017 Notification of acceptance/rejection 1 Mar 2018 Final version For more information, please see https://www.mpi-inf.mpg.de/JARS17/ Guest Editors Armin Biere, Johannes Kepler University, Linz, Austria Cesare Tinelli, The University of Iowa, Iowa City, USA Christoph Weidenbach, Max Planck Institute for Informatics, Saarbruecken, Germany