From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p236Z9fg001147 for ; Thu, 3 Mar 2011 07:35:09 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AlIBAPDEbk3Lj65GkWdsb2JhbACmdRUBAQEBCQsKBxEFBRu+PIVhBIwsg0iDDw X-IronPort-AV: E=Sophos;i="4.62,257,1297033200"; d="scan'208";a="101148970" Received: from atp-es2.it.nicta.com.au ([203.143.174.70]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 03 Mar 2011 07:35:03 +0100 Received: from atp-mbx1.it.nicta.com.au ([221.199.216.123] helo=atp-mbx1.in.nicta.com.au) by atp-es2.it.nicta.com.au with esmtp (Exim 4.69) (envelope-from ) id 1Pv27R-0000XU-2E; Thu, 03 Mar 2011 17:34:37 +1100 Received: from peterh.dynhost.nicta.com.au (221.199.216.124) by atp-mbx1.in.nicta.com.au (221.199.216.123) with Microsoft SMTP Server (TLS) id 8.2.176.0; Thu, 3 Mar 2011 17:34:37 +1100 Message-ID: From: =?ISO-8859-1?Q?Peter_H=F6fner?= To: Peter Hoefner Content-Type: text/plain; charset="US-ASCII"; format=flowed MIME-Version: 1.0 (Apple Message framework v936) Date: Thu, 3 Mar 2011 17:34:36 +1100 CC: caml-list@inria.fr, finite-model-theory@lists.rwth-aachen.de, hol-info@lists.sourceforge.net, humanist@lists.princeton.edu, logic-list@helsinki.fi, nwpt-info@lists.ioc.ee, puml-list@cs.york.ac.uk, spin_list@research.bell-labs.com, theorynt@listserv.nodak.edu, vki-list@dfki.de X-Mailer: Apple Mail (2.936) X-TM-AS-Product-Ver: SMEX-8.0.0.4125-6.500.1024-17988.004 X-TM-AS-Result: No--27.447000-0.000000-31 X-TM-AS-User-Approved-Sender: Yes X-TM-AS-User-Blocked-Sender: No X-SA-Exim-Connect-IP: 221.199.216.123 X-SA-Exim-Mail-From: Peter.Hoefner@nicta.com.au X-Spam-Checker-Version: SpamAssassin 3.2.5 (2008-06-10) on atp-es2.it.nicta.com.au X-Spam-Level: X-SA-Exim-Version: 4.2.1 (built Wed, 25 Jun 2008 17:20:07 +0000) X-SA-Exim-Scanned: Yes (on atp-es2.it.nicta.com.au) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p236Z9fg001147 Subject: [Caml-list] Workshop on Automated Theory Engineering (Call for Paper) ======================================================= Sorry for possible multiple copies of this announcement. ======================================================= FIRST CALL FOR PAPERS ATE-2011 CADE23 Workshop on Automated Theory Engineering (31. July 2011) Deadline: 29 April 2011 http://www.nicta.com.au/ate2011/ GENERAL INFORMATION The first Workshop on Automated Theory Engineering will be held in July 2011 in Wroclaw. It is associated with the 23th International Conference on Automated Deduction (CADE23). SCOPE Theory engineering means the development and mechanisation of mathematical axioms, definitions, theorems and inference procedures as needed to cover the essential concepts and analysis tasks of an application domain. It is essential for the qualitative and quantitative modelling and analysis of computing systems. The aim of the workshop is to present users with lightweight domain specific modelling languages, and to devolve the technical intricacies of analysis tasks as far as possible to tools that provide heavyweight automation. The workshop brings together tool and theory developers with industrial engineers to exchange experiences and ideas that stimulate further tool developments and theory designs. A main goal is the creation of a repository of case studies that allows developers to test and improve their theories and tools. TOPICS Theory engineering is relevant to the design of systems, programs, APIs, protocols, algorithms, design patterns, specification languages, programming languages and beyond. It involves technology such as ITP systems, ATP systems, SAT/SMT solvers, model checkers and decision procedures. Specific topics of the workshop include, but are not limited to: o qualitative and quantitative modelling and analysis o formal specification and verification o domain specific models, languages and solvers o theorem proving technology for theory engineering o integration of theories and tools o applications of mechanised reasoning to formal modelling o industrial case studies/experiences We especially invite industrial contributions from the areas of network protocols and concurrent systems, but any submission on the topics outlined is very welcome. INVITED SPEAKER o Timothy Griffin, University of Cambridge, UK o TBA SUBMISSIONS Submission of papers for presentation at the workshop are now invited. Submissions are limited to 10 pages, but shorter extended abstracts are welcome. All papers will be reviewed by the programme committee, and a balanced programme will be selected based on relevance and technical soundness. Submissions must be in PDF using the LaTeX EasyChair-format http://www.easychair.org/easychair.zip . Accepted papers will be published as CEUR Workshop Proceedings. If quality and quantity of the submissions warrants this, we plan to publish a special issue of a recognized journal on the topic of the workshop. IMPORTANT DATES: Submission: 29 April 2011 Notification: 30 May 2011 Final version: 1 July 2011 Workshop: 31 July 2011 PROGRAMME COMMITTEE o Michael Butler, University of Southampton, UK o Ewen Denney, NASA, US o Peter Hoefner, NICTA, Australia o Joe Hurd, Galois, Inc., US o Rajeev Joshi, NASA (JPL) , US o Annabelle McIver, Macquarie University/NICTA, Australia o Stephan Merz, INRIA, France o Marius Portmann, University of Queensland/NICTA, Australia o Georg Struth, University of Sheffield, UK o Geoff Sutcliffe, University of Miami, US ORGANISERS Peter Hoefner, NICTA, Australia Annabelle McIver, Macquarie University, Australia Georg Struth, University of Sheffield, UK The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.