[isabelle] Workshop on Automated Theory Engineering (Extended Deadline)

Sorry for possible multiple copies of this announcement.

                    LAST CALL FOR PAPERS

                      CADE23 Workshop on
                Automated Theory Engineering
                            (31. July 2011)

              Extended Deadline: 6 May 2011

  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

  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.

  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.

  o  Timothy Griffin, University of Cambridge, UK
  o  TBA

  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.

  Submission (extended):    6 May 2011
  Notification:    30 May 2011
  Final version:   1 July 2011
  Workshop:       31 July 2011

  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

  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.