Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Call for Papers: Workshop on Automated Theory ...


view this post on Zulip Email Gateway (Aug 18 2022 at 17:06):

From: Joe Hurd <joe.hurd@comlab.ox.ac.uk>
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


Last updated: Mar 29 2024 at 04:18 UTC