From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 08FF37FCF9 for ; Tue, 21 Apr 2015 10:56:11 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Iain.Whiteside@newcastle.ac.uk) identity=pra; client-ip=128.240.234.22; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Iain.Whiteside@newcastle.ac.uk"; x-sender="Iain.Whiteside@newcastle.ac.uk"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of Iain.Whiteside@newcastle.ac.uk designates 128.240.234.22 as permitted sender) identity=mailfrom; client-ip=128.240.234.22; receiver=mail2-smtp-roc.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: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@cheviot22.ncl.ac.uk) identity=helo; client-ip=128.240.234.22; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Iain.Whiteside@newcastle.ac.uk"; x-sender="postmaster@cheviot22.ncl.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AuAQCFDzZVnBbq8IBBGoJmeFwFx10Gh0o8EAEBAQEBAQERAQEBAQEICwkJFC6EJx0dGRUFHgE+Qg4ZBBOIKwEMN6UTliaJQIRdCwEBAR6MdIJZCwoHAYMFDEEdgRYFhjKOf4I3hQ+DPIl5EoZBggYuDIFVbwGBAQkXIoEAAQEB X-IPAS-Result: A0AuAQCFDzZVnBbq8IBBGoJmeFwFx10Gh0o8EAEBAQEBAQERAQEBAQEICwkJFC6EJx0dGRUFHgE+Qg4ZBBOIKwEMN6UTliaJQIRdCwEBAR6MdIJZCwoHAYMFDEEdgRYFhjKOf4I3hQ+DPIl5EoZBggYuDIFVbwGBAQkXIoEAAQEB X-IronPort-AV: E=Sophos;i="5.11,614,1422918000"; d="scan'208";a="136013738" Received: from cheviot22.ncl.ac.uk ([128.240.234.22]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 21 Apr 2015 10:56:10 +0200 Received: from exhubvm01.ncl.ac.uk ([128.240.234.5] helo=EXHUBVM01.campus.ncl.ac.uk) by cheviot22.ncl.ac.uk with esmtp (Exim 4.63) (envelope-from ) id 1YkTyS-0007bN-FO for caml-list@inria.fr; Tue, 21 Apr 2015 09:56:08 +0100 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, 21 Apr 2015 09:56:07 +0100 From: Iain Whiteside To: "caml-list@inria.fr" Thread-Topic: AI4FM 2015: Call for Short Contributions Thread-Index: AQHQfBEAo/yY8uVocUuasQsEYG/7GQ== Date: Tue, 21 Apr 2015 08:56:05 +0000 Message-ID: <3EA767D1-C71C-432F-B6A0-E09DC231E6BF@newcastle.ac.uk> Reply-To: "ai4fm2015@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.7] Content-Type: text/plain; charset="us-ascii" Content-ID: <34831B61DFAFB646B54C5F9376C2D80D@fangorn.ncl.ac.uk> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Subject: [Caml-list] AI4FM 2015: Call for Short Contributions ------------------------------------------------- AI4FM 2015 - the 6th International Workshop on the use of AI in Formal Methods http://www.ai4fm.org/ai4fm-2015/ Edinburgh, 1st September, 2015 In association with AVoCS 2015 https://sites.google.com/site/avocs15 ------------------------------------------------- --- First Call for Contributions --- Important Dates --------------- Submission deadline: 1st August, 2015 Notification of acceptance: 10th August, 2015 Final version due: 21st August, 2015 Workshop: 1st September, 2015 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. - Novel ideas on how to use AI (e.g. machine learning, pattern recognition)= =20 in proof automation. - Use of cloud elasticity for: scalability on large scale developments,=20 proof/lemma exploration. - Techniques for bridging the development to maintenance gap. =20 We want to continue the area of research beyond our sponsored project=20 (at Newcastle and Edinburgh universities), which has come to an end. This means we would particularly encourage the submission of position=20 papers on new ideas or research directions for the use of AI techniques=20 in the proof discovery process as well as in modelling best practices.=20 Student grants --------------- Thanks to sponsorships from FME and SICSA we can offer financial support=20 for a limited number of students registering for AVoCS in the form of a=20 registration fee waiver (full or partial). As this is limited, we ask the s= tudents=20 that would like to take the advantage of this support to submit a short app= lication.=20 The details on how to apply will be available in due course from the AVoCS= =20 webpage. History --------------- This will be the fifth workshop in the series. Previous workshops were held= at: - Singapore, May 2014 @ FM (www.ai4fm.org/ai4fm-2014/) - 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 2015 to another workshop, conference or a journal. Submission is by email to: ai4fm2015@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) * Iain Whiteside (University of Edinburgh, UK) * Gudmund Grov (Heriot Watt University, UK) Contact Details ---------------- If you have any queries, please email the organisers at the following=20 email address: ai4fm2015@ai4fm.org=