CADE-24 Workshops

[Geoff Sutcliffe]

Call for Papers

     Workshops at CADE-24 -- Lake Placid, New York, 9-10 June, 2013

Short CFPs for the following CADE-24 workshops are attached:

ADDCT  - Automated Deduction: Decidability, Complexity, Tractability 
ARSEC  - Automated Reasoning in Security
ARiSVe - Automated Reasoning in Software Verification
ESARAI - Empirically Successful Automated Reasoning with AI
KInAR  - Knowledge Intensive Automated Reasoning
PxTP   - Proof Exchange for Theorem Proving

For the Workshop Methods for Modalities (M4M) respective Information
will be distributed soon.

Moreover, CADE-24 will host a StarExec meeting.

===== ADDCT ==========================================================

ADDCT - Automated Deduction: Decidability, Complexity, Tractability 

Decidability, and especially complexity and tractability of logical
theories is extremely important for a large number of
applications. Although general logical formalisms (such as predicate
logic or number theory) are undecidable, decidable theories or
decidable fragments thereof (sometimes even with low complexity) often
occur in mathematics, in program verification, in the verification of
reactive, real time or hybrid systems, as well as in databases and
ontologies. It is therefore important to identify such decidable
fragments and design efficient decision procedures for them. It is
equally important to have uniform methods (such as resolution,
rewriting, tableaux, sequent calculi, ...) which can be tuned to
provide algorithms with optimal complexity.

The goal of ADDCT is to bring together researchers interested in
- identifying (fragments of) logical theories which are decidable,
  identifying fragments thereof which have low complexity, and
  analyzing possibilities of obtaining optimal complexity results with
  uniform tools;
- analyzing decidability in combinations of theories and possibilities
  of combining decision procedures;
- efficient implementations for decidable fragments;
- application domains where decidability resp. tractability are
  crucial.

Full Paper submission: March 26, 2013
Notification: April 26, 2013
Final versions: May 10, 2013
Workshop: June 10, 2013

More details: http://userpages.uni-koblenz.de/~sofronie/addct-2013/

===== ARSEC ==========================================================

ARSEC - Automated Reasoning in Security 

Automated reasoning methods have become increasingly critical in many
areas of security, from analyzing cryptographic protocols for flaws to
analyzing access-control and privacy policies. This interaction is
proving to be mutually beneficial: automated reasoning methods are
finding new applications in security; and new automated reasoning
methods, developed for security applications, are enriching the tools
available to all areas of automated reasoning.

ARSEC will bring together researchers interested in automated
reasoning and security to present recent work (including work in
progress) and to discuss new ideas and trends in the field.  

Possible topics include, but are not limited to: 
- Security Protocols
- Security Policies 
- Privacy and Confidentiality
- Intrusion Detection
- Automated Reasoning techniques such as Paramodulation, Rewriting,
  Unification and Satisfiability Modulo Theories (SMT).

Paper Submission: March 25th 
Workshop: June 9th 2013

More details: http://www.cs.albany.edu/~marshall/ARSEC/

===== ARiSVe =========================================================

ARiSVe - Automated Reasoning in Software Verification

The focus of the workshop is application of automated reasoning in the
context of software verification, and, more generally, automation in
software verification. Relevant topics include but are not limited to:
- specifics of verification-related automated reasoning tasks;
- efficient translation of high-level verification conditions
  to logical languages of automated reasoning tools;
- handling of the prover's feedback: proofs, models, answer terms;
- logical theories of interest for program verification, decision
  procedures, integration into existing ATP and SMT systems;
- combination of automated and user-assisted verification;
  tool presentations, tool comparisons, and benchmarks;
- experience reports on verification of complex algorithms and
  real-life software with the use of automated reasoning tools.

Invited speaker:  K. Rustan M. Leino (Microsoft Research)

Abstract submission deadline: March 8, 2013
Submission deadline: March 15, 2013
Notification: April 10, 2013
Camera ready versions due: May 10, 2013
Workshop: June 10, 2013

More details:  http://arisve2013.lri.fr 

===== ESARAI =========================================================

ESARAI - Empirically Successful Automated Reasoning with Artificial
Intelligence

The Empirically Successful Automated Reasoning with Artificial
Intelligence (ESARAI) workshop will bring together two complementary
groups of researchers: researchers in Automated Reasoning who employ
Artificial Intelligence tools and techniques to support their
automated reasoning research, and researchers in Artificial
Intelligence who employ Automated Reasoning tools and techniques to
support the artificial intelligence research. The workshop will offer
mutually beneficial interactions, through the exposure of the two
sides of the research to all. Additionally, the workshop will provide
a focussed forum where the many interfaces between these two research
fields can be presented and discussed. The workshop is soliciting
research, position, applications and system description papers on
combinations of AI and AR. Additionally, the workshop includes system
and application demonstrations. Demonstrations of systems and
applications described in paper presentations, and demonstrations of
systems and applications without an accompanying paper, are both
encouraged.  

Submission deadline - 22nd April
Notification of acceptance - 13th May
Final versions due - 20th May
Workshop - 9th or 10th June

More details: http://www.cs.miami.edu/~geoff/Conferences/ESARAI/

===== KInAR ==========================================================

KInAR - Knowledge Intensive Automated Reasoning 

Extensive digital sources of knowledge are becoming available, such as
formal ontologies, databases, dictionaries and natural language
reference works. Online sources like Wikipedia and IMDb, mathematical
libraries like Mizar and various search engines and web services have
gained widespread acceptance among the general population, but the
sheer quantity of data can be an obstacle for human users. Automated
reasoning (AR) systems have been advancing in their capabilities, and
there is a growing interest in employing their deductive power to make
digital knowledge more accessible.  This poses challenges to AR
research, but it is also a chance to bring AR into the public and to
see large-scale usage of AR systems. In the KInAR workshop we aim to
compile approaches to AR on large knowledge sources, and to aid the
connections between researchers working on such projects.

We invite submissions on any topics regarding KInAR, such as:
- theoretical foundations: calculi for knowledge intensive reasoning,
- knowledge corpora and their management,
- extracting (semi-)formal knowledge from large informal corpora,
- system descriptions of applications regarding the workshop topic,
- benchmarking such systems,
- robustness: reasoning despite flaws in digital knowledge,
- combining knowledge from different sources.

Submission deadline: 8 April 2013
Author notification: 2 May 2013
Camera-ready version: 9 May 2013
KInAR workshop: 10 June 2013

More details: http://userpages.uni-koblenz.de/~bpelzer/kinar2013

===== PxTP ===========================================================

PxTP - Proof Exchange for Theorem Proving

The past decades have seen impressive advances in computer-aided
reasoning, both in automated and interactive theorem proving. As shown
by various system competitions, such as CASC, SMT-COMP, and the SAT
competition, deduction tools are able to tackle larger problems
progressively faster and are increasingly more applicable to a wider
range of problems. In recent years, integration of such automated
tools in larger verification environments has demonstrated the
potential to reduce the amount of manual verification work.

It is becoming clear that the success of deduction tools will not only
depend on their power to solve large and difficult problems in an
isolated manner, but it will also rely on their ability to cooperate,
by exchanging problems, proofs, and models. The PxTP workshop aims at
encouraging such cooperation by inviting contributions on various
aspects of communication, integration, and cooperation between systems
and formalisms. The workshop's mission is to facilitate building of
complex reasoning applications and reuse of reasoning tools by
developing and discussing suitable integration, translation and
communication methods, standards, protocols, and application
programming interfaces (APIs). The workshop would like to bring
together the interested developers of automatic and interactive
theorem proving tools, developers of combined systems, developers and
users of translation tools and APIs, and producers of standards and
protocols. 

Submission of papers: 11 April 2013
Notification: 2 May 2013
Camera-ready versions due: 9 May 2013
Workshop: 10 June 2013

More details: http://www.cs.ru.nl/pxtp13/

===== StarExec =======================================================

StarExec 

The StarExec project is an NSF funded project to design, implement,
and operate StarExec, a web service designed for the comparative
evaluation of logic solvers (automated theorem provers) on benchmark
problems. The $1.85 million budget of the grant is mostly dedicated to
purchasing and operating a medium-sized cluster of an anticipated 150
compute nodes, which will be used to run jobs submitted by users of
the system. We anticipate users will be members of various
logic-solving subcommunities of the broader automated theorem proving
community

The StarExec 2013 workshop will bring together logic-solving community
leaders, logic solver competition organizers, StarExec power users,
and the StarExec organizers, to discuss the current status of the
StarExec project. The workshop will have four sessions:
- A status report from the StarExec organizers, and a demonstration of
  StarExec as it has been developed by the time of the workshop.
- Use of StarExec by the attendees, so they can get a feeling of how
  well the implementation will meet their solver evaluation needs.
- A feedback session based on the use of StarExec.
- A presentation by the StarExec organizers on the short and medium
  terms plans for development and use of StarExec.

StarExec 2013 will not invite papers or general attendance. Rather,
the workshop will be aimed specifically at the types of researchers
described above, to maximize the positive impact on the development
and use of StarExec. The NSF grant will provide travel, accomodation,
and registration support for 20 participants, 10 from the USA and 10
from overseas.

More details: http://clc.cs.uiowa.edu/starexec13/