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 CE2787F84F for ; Tue, 25 Feb 2014 15:01:58 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of Iain.Whiteside@newcastle.ac.uk) identity=pra; client-ip=128.240.234.12; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Iain.Whiteside@newcastle.ac.uk"; x-sender="Iain.Whiteside@newcastle.ac.uk"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of Iain.Whiteside@newcastle.ac.uk designates 128.240.234.12 as permitted sender) identity=mailfrom; client-ip=128.240.234.12; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Iain.Whiteside@newcastle.ac.uk"; x-sender="Iain.Whiteside@newcastle.ac.uk"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of postmaster@cheviot12.ncl.ac.uk designates 128.240.234.12 as permitted sender) identity=helo; client-ip=128.240.234.12; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Iain.Whiteside@newcastle.ac.uk"; x-sender="postmaster@cheviot12.ncl.ac.uk"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnsDAHKhDFOA8OoMnGdsb2JhbAA/GoJlXFekOQqZH4UHFg4BAQEBAQYNCQkUKIIsHTYVBR4BgQAOGQQTiAUBDDaWT6Q2hQ2GMY13CwoHAYMGD2aBFASJEIs5kEQKiHGBaAkXIg X-IPAS-Result: AnsDAHKhDFOA8OoMnGdsb2JhbAA/GoJlXFekOQqZH4UHFg4BAQEBAQYNCQkUKIIsHTYVBR4BgQAOGQQTiAUBDDaWT6Q2hQ2GMY13CwoHAYMGD2aBFASJEIs5kEQKiHGBaAkXIg X-IronPort-AV: E=Sophos;i="4.97,540,1389740400"; d="scan'208";a="50467881" Received: from cheviot12.ncl.ac.uk ([128.240.234.12]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 25 Feb 2014 15:01:58 +0100 Received: from exhubvm01.ncl.ac.uk ([128.240.234.5] helo=EXHUBVM01.campus.ncl.ac.uk) by cheviot12.ncl.ac.uk with esmtp (Exim 4.63) (envelope-from ) id 1WIIa4-0001NX-Cd for caml-list@inria.fr; Tue, 25 Feb 2014 14:01:56 +0000 Received: from EXMBDB02.campus.ncl.ac.uk ([fe80::c039:e17:9d60:9f3]) by EXHUBVM01.campus.ncl.ac.uk ([2002:80f0:ea05::80f0:ea05]) with mapi id 14.03.0158.001; Tue, 25 Feb 2014 14:01:28 +0000 From: Iain Whiteside To: "caml-list@inria.fr" Thread-Topic: *Deadline extended* Final call for contributions AI4FM 2014 Thread-Index: AQHPMjITX2vd3Ql5oUWDcIlVkK5WQw== Date: Tue, 25 Feb 2014 14:01:28 +0000 Message-ID: <9D397CC2-30D8-4D44-B7C8-56DF6D870060@newcastle.ac.uk> Reply-To: "ai4fm2014@ai4fm.org" Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [10.4.160.6] Content-Type: text/plain; charset="iso-8859-1" Content-ID: <6D8B64636407D544A570B5DF244B5A94@fangorn.ncl.ac.uk> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Subject: [Caml-list] *Deadline extended* Final call for contributions AI4FM 2014 ------------------------------------------------- AI4FM 2014 - the 5th International Workshop on the use of AI in Formal Methods =20=20=20=20=20=20 http://www.ai4fm.org/ai4fm-2014/ Singapore, 13th May, 2014 In association with FM 2014 ------------------------------------------------- --- Final Call for Contributions --- Confirmed Speakers --------------- Rustan Leino, Microsoft Research Chin Wei Ngan, National University of Singapore Dominique M=E9ry, LORIA and Universit=E9 de Lorraine Important Dates --------------- Submission deadline: *March 15, 2014* Notification of acceptance: March 22, 2014 Final version due: April 22, 2014 Workshop: May 13th, 2014 General --------------- This workshop will bring together researchers from formal methods,=20 automated reasoning and AI; it will address the issue of how AI can=20 be used to support the formal software development process, including=20 requirement analysis, modelling and proof. Previous AI4FM workshops=20 have included a mix of industrial and academic participants and we=20 anticipate attracting a similarly diverse audience.=20 Rigorous software development using formal methods allows the construction= =20 of an accurate characterisation of a problem domain that is firmly based=20 on mathematics; by applying standard mathematical analyses, these methods=20 can be used to prove that systems satisfy formal specifications. Research=20 has shown that with tools backed by mature theory, formal methods are=20 becoming cost effective and their use is easier to justify, not as an=20 academic exercise, legal requirement or niche markets -- but as part of=20 a business case. However, while industrial use of formal methods is=20 increasing, in order to make it more mainstream, the cost of applying=20 formal methods, in terms of mathematical skill level and development=20 time, must still be reduced. We believe that AI can help with these=20 issues. Scope --------------- We encourage submissions presenting work in progress, tools under development, and PhD projects, in order that the workshop can become=20 a forum for active dialogue between the groups involved in automated=20 reasoning, formal methods and artificial intelligence. Particular=20 areas of interest include, but are not limited to: - The use of AI and automated reasoning to support and guide the formal=20 modelling process. - The use of AI and automated reasoning in the requirement capture process. - The use of AI to reuse formal models, programs and proofs. - The use of machine learning to support interactive theorem proving. - The use of machine learning to enhance automated theorem proving. - The development of search heuristics. - The use of AI for term synthesis, invariant generation, lemma discovery=20 and concept invention. - The use of AI for counter-example generation. - The use of constraint solvers in formal methods.=20 - The role of AI planning for formal systems developments, from requirement= s=20 to the end product (including software and hardware). - The interplay between reasoning and modelling and the role of AI in this= =20 framework. - Ontologies in the formal engineering process. History --------------- This will be the fifth workshop in the series. Previous workshops were held= at: - Rennes, France, July 2013 @ ITP (www.ai4fm.org/ai4fm-2013/) - Schloss Dagstuhl, Germany, July 2012 (www.dagstuhl.de/12271) - Edinburgh, UK, April 2011 (www.ai4fm.org/ai4fm-2011.php) - Newcastle, UK, May 2010 (www.ai4fm.org/ko-meeting.php) Submission --------------- The main aim for the workshop is discussion, thus submissions do not=20 need to be original. Extended versions of submissions may have been=20 published previously, or submitted concurrently with or after AI4FM=20 2014 to another workshop, conference or a journal. Submission is by email to: ai4fm2014@ai4fm.org Please submit an abstract up to 3 pages in a PDF format. The extended=20 abstracts will be handed out to all participants, and will be made=20 into a technical report prior to the workshop.=20 Acceptance for presentation at the workshop will be made by the=20 organisers based on relevance to the workshop. Organisers --------------- * Leo Freitas (Newcastle University, UK) * Gudmund Grov (Heriot-Watt University, UK) * Iain Whiteside (Newcastle University, UK) Contact Details ---------------- If you have any queries, please email the organisers at the following=20 email address: ai4fm2014@ai4fm.org