ARCADE                    http://www.cs.man.ac.uk/~regerg/arcade/
Automated Reasoning:
Challenges, Applications, Directions, Exemplary achievements

6 August 2017, Gothenburg, Sweden (co-located with CADE-26)


The main goal of this workshop is to bring together key people from various subcommunities of automated reasoning—such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving—to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community.

The structure of the workshop will be informal. We invite extended abstracts (2-4 pages, using the EasyChair class style http://www.easychair.org/publications/for_authors) in the form of non-technical position statements aimed at prompting lively discussion. The title of the workshop is indicative of the kind of discussions we would like to encourage:

Challenges: What are the next grand challenges for research on automated reasoning? Thereby, we refer to problems, solving which would imply a significant impact (e.g., shift of focus) on the CADE community and beyond. Roughly ten years ago SMT was one such challenge.

Applications: Is automated reasoning applicable in real-world (industrial) scenarios. Should reports on such applications be encouraged at a venue like CADE, perhaps by means of a special case study paper category?

Directions: Based on the grand challenges and requirements from real-world applications, what are the research directions the community should promote? What bridges between the different subcommunities of automated reasoning need to be strengthened? What new communities should be included (if at all)? For example, following Reiner Hähnle’s question in the AAR Newsletter, is there a place at CADE for research on usable automated reasoning (in resemblance to the flourishing topic of usable security)?

Exemplary achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself? What can we learn from those successes when shaping our future research?

Contributions will be grouped into similar themes and authors will be invited to make their case within discussion panels. Authors will then be invited to extend their abstracts (e.g., by transcripts of the discussion and a summary of the discussion’s outcomes) for inclusion in an EPiC post-proceedings.

IMPORTANT DATES (Anywhere on Earth):

  • Submission deadline: 12 May 2017
  • Notification: 23 June 2017
  • Workshop: 6 August 2017
  • Post-proceedings deadline: 29 September 2017


  • Franz Baader, TU Dresden
  • Christoph Benzmüller, Freie Universität Berlin
  • Armin Biere, Johannes Kepler University Linz
  • Nikolaj Bjørner, Microsoft Research
  • Jasmin Christian Blanchette, Inria Nancy & Loria
  • Maria Paola Bonacina, Università degli Studi di Verona
  • Pascal Fontaine, Loria, Inria, University of Lorraine
  • Silvio Ghilardi, Università degli Studi di Milano
  • Martin Giese, University of Oslo
  • Jürgen Giesl, RWTH Aachen
  • Alberto Griggio, FBK-IRST
  • Reiner Hähnle, TU Darmstadt
  • Marijn Heule, The University of Texas at Austin
  • Laura Kovács, Vienna University of Technology
  • Aart Middeldorp, University of Innsbruck
  • Neil Murray, SUNY at Albany
  • David Plaisted, University of North Carolina at Chapel Hill
  • Andrei Popescu, Middlesex University London
  • Giles Reger, University of Manchester (co-chair)
  • Renate Schmidt, The University of Manchester
  • Stephan Schulz, DHBW Stuttgart
  • Geoff Sutcliffe, University of Miami
  • Cesare Tinelli, The University of Iowa
  • Dmitriy Traytel, ETH Zürich (co-chair)
  • Andrei Voronkov, The University of Manchester
  • Christoph Weidenbach, Max Planck Institute for Informatics