[ecoop-info] CfP: IJCAR Workshop on Automated Theory Exploration

[Peter Höfner]

                [Apologies if you receive multiple copies of this announcement]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
                                CALL FOR PAPERS:

                                    ATX-2012
                  IJCAR Workshop on Automated Theory Exploration
                                (June 30-July 1)
                   http://dream.inf.ed.ac.uk/events/atx2012


GENERAL INFORMATION

This Workshop on Automated Theory Exploration will be held in June/July in Manchester, UK.
It is associated with the 6th International Conference on Automated Reasoning (IJCAR) and
follows on from two series of workshops: Automated Theory Engineering and Automatheo.

SCOPE

Theory exploration means the development of mathematical axioms, definitions, conjectures,
theorems, examples and inference procedures as needed to cover the essential concepts
and analysis tasks of mathematical and other application domains. The automation and
mechanisation of these capabilities are much sought after in areas such as software
verification, the analysis of computer systems, formalised mathematics and indeed
mathematical research.

The aim of the workshop is to bring together researchers with interests in any aspects
of this area, including domain-specific formalisations, tool and theory development,
and general-purpose frameworks for the structuring of theories and their maintenance.

TOPICS

Theory exploration 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 mechanised reasoning for modelling and analysis
o automation applied to formal specification and verification
o domain specific models, languages and solvers
o theorem proving technology for theory exploration
o integration of theories and tools
o the formalisation and automation of mathematics
o case studies/experiences
o automated identification of key concepts and results
o supporting collaborative theory exploration


INVITED SPEAKERS

o Robert L. Constable, Cornell University.
o TBA

SUBMISSIONS

We invite submissions in 3 forms:

o Research papers, up to 10 pages;
o System/tool descriptions, up to 5 pages;
o Extended abstracts, up to 3 pages.

Research and tool papers must be unpublished and not submitted for publication
elsewhere. Extended abstracts are intended to discuss ideas and work in progress.
All papers will be reviewed by the programme committee.

Submissions must be in PDF using the LaTeX EasyChair-format
http://www.easychair.org/easychair.zip . One author of each accepted submission
is expected to present the paper at the workshop. Associated systems demos are
encouraged, where appropriate.

Accepted research and tool 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: 3 April 2012
Notification: 8 May, 2012
Final version: 5 June, 2012
Workshop: 30 June & 1 July, 2012

PROGRAM COMMITTEE

 o Jacques Fleuriot (University of Edinburgh, UK)
 o Timothy Griffin (University of Cambridge, UK)
 o Peter Höfner (NICTA, Australia)
 o Joe Hurd (Galois, USA)
 o Temur Kutsia (RISC, Austria)
 o Roy McCasland (University of Edinburgh, UK)
 o Annabelle McIver (Macquarie University, Australia)
 o Stephan Merz (INRIA, France)
 o Petros Papapanagiotou (University of Edinburgh, UK)
 o Alan Smaill (University of Edinburgh, UK)
 o David Stanovsky (Charles University, Czech Republic)
 o Georg Struth (University of Sheffield, UK)
 o Josef Urban (Radboud University, Netherlands)

WORKSHOP ORGANISERS

 o Alan Smaill
 o Annabelle McIver
 o Peter Höfner
 o Jacques Fleuriot

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.