Workshops and Tutorials

The following workshops and tutorials will be organised alongside CADE-26 on 6 and 7 Aug 2017. Workshops and tutorials will take place in building Jupiter. The Jupiter building is the one numbered 2 on the map found under Local info.

6 Aug 2017:

7 Aug 2017:

The traditional CADE ATP System Competition (CASC) will also be held at CADE-26. CASC will be held during the main CADE conference on 9 Aug 2017.

ARCADE: Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements

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 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?
Applications: Is automated reasoning applicable in real-world (industrial) scenarios.
Directions: Based on the grand challenges and requirements from real-world applications, what are the research directions the community should promote?
Exemplary Achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself?

Time: Sunday 6 Aug 8:55–17:00

Place: Room 243, Jupiter building

ARCADE workshop webpage

Organisers: Giles Reger, Dmitriy Traytel

HCVS: Horn Clauses for Verification and Synthesis

Most Program Verification and Synthesis problems of interest can be modeled directly using Horn clauses and many recent advances in the Automated Deduction, Constraint/Logic Programming and Verification communities have centered around efficiently solving problems presented as Horn clauses. This workshop aims to bring together researchers working in the communities of Automated Deduction (e.g CADE), Constraint/Logic Programming (e.g., ICLP and CP) and Program Verification community (e.g., CAV, TACAS, and VMCAI) on the topic of Horn clause based analysis, verification and synthesis.

Topics of interest include, but are not limited to the use of Horn clauses, constraints, and related formalisms in the following areas:

Automated deduction
Analysis and verification of programs in various programming paradigms (e.g., imperative, object-oriented, functional, logic, higher-order, concurrent)
Program synthesis
Program testing
Program transformation
Constraint solving
Type systems
Case studies and tools
Challenging problems

Time: Sunday 6 Aug 9:00–17:00

Place: Room 218, Jupiter building

HCVS'17 workshop webpage

Organisers: Alberto Griggio, Manuel Hermenegildo

PCR'17: Workshop on Parallel Constraint Reasoning

The workshop focuses on theory, implementation, and applications of parallel constraint reasoning. The phenomenal recent success in constraint reasoning has made approaches previously deemed impractical within the reach of both industrial and academic applications. Since some time the technology for producing CPUs has hit a physical barrier for obtaining sequential speed-up through laying out transistors on a chip. Since speed-up is no longer achievable through sequential hardware, there is an ongoing shift to wide-spread parallel computing. The workshop program will be organized as a collection of high-quality invited talks.

Time: Sunday 6 Aug 9:00 - 16:30

Place: Room 219, Jupiter building

PCR'17 workshop webpage

Organisers: Antti Hyvärinen, Christoph M. Wintersteiger

ThEdu'17: Theorem Prover Components for Educational Software

(Computer) Theorem Proving (TP) is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. Topics of interest include:

methods of automated deduction applied to checking students' input;
methods of automated deduction applied to prove post-conditions for particular problem solutions;
combinations of deduction and computation enabling systems to propose next steps;
automated provers specific for dynamic geometry systems;
proof and proving in mathematics education.

Time: Sunday 6 Aug 9:00–17:00

Place: Room 218, Jupiter building

ThEdu'17 workshop webpage

Organisers: Pedro Quaresma and Walther Neuper

Tutorial: Certified Functional (Co)programming with Isabelle/HOL

Over the past five years, the organizers have developed programming capabilities for finite and infinite (lazy) data structures in the Isabelle/HOL proof assistant, using the foundational approach characteristic of HOL provers. In contrast with the Isabelle tutorial at CADE-25, the focus will be on verified programming using the subset of Isabelle/HOL that corresponds to a typed functional programming language. The focus will be on mechanisms specific to Isabelle/HOL, notably: (1) reaching a balance between guaranteed termination/productivity and expressiveness; (2) mixing recursion with corecursion soundly; and (3) obtaining compositional proof methods that match the program definitions.

Time: Monday 7 Aug 9:00–17:00

Place: Room 219, Jupiter building

Tutorial webpage

Organisers: Jasmin Blanchette, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

Vampire 2017: The 4th Vampire Workshop

The workshop aims at discussing recent developments in implementing, applying benchmarking and comparing first-order theorem provers and their combinations with other systems. Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The workshop is going to to shed the light on on problems such as

what is essential for substantial progress in theorem proving tools;
what are the best implementation principles to be used;
what are the best heuristics and strategies, depending on application areas;
both successful and unsuccessful case studies;
missing features in modern theorem provers.

Time: Monday 7 Aug 9:30–17:00

Place: Room 243, Jupiter building

Vampire 2017 workshop webpage

Organisers: Laura Kovacs and Andrei Voronkov