[isabelle] Call for Papers: Workshop on Automated Theory Engineering



The scope of this workshop has a large overlap with interactive
theorem proving, and ITP systems are explicitly called out in the list
of topics. Apologies in advance if you receive multiple copies. -- Joe



                   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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.