The Coq mailing list

[Peter H�fner <Peter.Hoefner AT nicta.com.au>]

                [Apologies if you receive multiple copies of this 
announcement]
                            *** Deadline extended to 17th April 2012 ***
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
                                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.

Please upload your submission at: 
https://www.easychair.org/conferences/?conf=atx2012

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: 17 April 2012 (*Extended Deadline*)
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.