[isabelle] Workshop on Automated Theory Engineering (Call for Paper)



=======================================================
Sorry for possible multiple copies of this announcement.
=======================================================

                    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

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.





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