Workshop Description
General Information
The First International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop will take place in association with The 26th International Conference on Automated Deduction (CADE-26) on the August 6, 2017.
Scope
The main goal of this workshop is to bring together key people from various sub-communities 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 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 sub-communities of CADE need to be strengthened? What new communities should be included (if at all)? For example, following Reiner Hahnle’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 for inclusion in post-proceedings to be published in EPiC.
Submission
Please submit your paper via this EasyChair submission page. Submissions should use the EPiC LaTeX format. We solicit non-technical extended abstracts of 2–4 pages (without firmly enforcing this length requirement). The post-proceedings version of the paper may be longer (but still of a reasonable length).
Important Dates
Submission deadline: | 12 May, 2017 |
Author notification: | 23 June, 2017 |
Workshop: | 6 August, 2017 |
Post-proceedings deadline: | 29 September, 2017 |
Program
This is the final program. We have attached preprints of the submitted position papers. These may be modified before being published in the official proceedings. Each session will consist of a number of presentations and then a discussion session covering all presentations. Each discussion session will begin with a set of starting questions from the authors. We encourage attendees to consider these questions and read the preprints to prepare for lively discussion!
08:55-09:00 | Intro | |||
09:00-10:00 | Session: Bridges Between Communities | |||
09:00-09:10 | Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, and Werner M. Seiler | SC-square: when Satisfiability Checking and Symbolic Computation join forces | slides | |
09:10-09:20 | Simon Cruanes | Making Automatic Theorem Provers more Versatile | slides | |
09:20-09:25 | Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, and Uwe Waldmann | Towards Strong Higher-Order Automation for Fast Interactive Verification | slides | |
09:25-10:00 | Discussion
|
|||
10:00-10:30 | Coffee Break | |||
10:30-11:15 | Session: Artificial Intelligence and Machine Learning | |||
10:30-10:35 | Maria Paola Bonacina | Automated Reasoning for Explainable Artificial Intelligence | slides | |
10:35-10:40 | Josef Urban | AI at CADE/IJCAR | ||
10:40-10:50 | Stephan Schulz | We know (nearly) nothing! But can we learn? | slides | |
10:50-11:15 | Discussion
|
|||
11:15-12:00 | Session: User Interfaces and Industrial Usage | |||
11:15-11:25 | Reiner Hähnle and Marieke Huisman | 24 Challenges in Deductive Software Verification | slides | |
11:25-11:35 | J Moore and Marijn Heule | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions | slides | |
11:35-12:00 | Discussion
|
|||
12:00-14:00 | Lunch | |||
14:00-15:00 | Session: Proof Formats | |||
14:00-14:10 | Bertram Felgenhauer | Beyond DRAT: Challenges in Certifying UNSAT | slides | |
14:10-14:20 | Marijn Heule and Benjamin Kiesl | The Potential of Interference-Based Proof Systems | slides | |
14:20-14:30 | Giles Reger and Martin Suda | Checkable Proofs for First-Order Theorem Proving | slides | |
14:30-15:00 | Discussion
|
|||
15:00-15:30 | Coffee Break | |||
15:30-16:30 | Session: Provers | |||
15:30-15:40 | Gopal Gupta, Elmer Salazar, Kyle Marple, Zhuo Chen, and Farhad Shakerin | A Case for Predicate Answer Set Programming | slides | |
15:40-15:50 | Andrew Reynolds | Challenges for Fast Synthesis Procedures in SMT | slides | |
15:50-16:00 | Christoph Weidenbach | Do Portfolio Solvers Harm? | slides | |
16:00-16:30 | Discussion
|
|||
16:30-17:00 | Concluding Discussion | |||
19:00 | ARCADE Dinner at Hello Monkey (Directions) |
Organisation
Organisers
Giles Reger, The University of Manchester
Dmitriy Traytel, ETH Zürich
Program Committee
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 Kovacs, 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
Renate Schmidt, The University of Manchester
Stephan Schulz, DHBW Stuttgart
Geoff Sutcliffe, University of Miami
Cesare Tinelli, The University of Iowa
Andrei Voronkov, The University of Manchester
Christoph Weidenbach, Max Planck Institute for Informatics