Workshops and Tutorials
The following workshops and tutorials will be organised alongside CADE-26 on 6 and 7 Aug 2017.
6 Aug 2017:
- ARCADE: Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
- PCR'17: Workshop on Parallel Constraint Reasoning
- ThEdu'17: Theorem Prover Components for Educational Software
7 Aug 2017:
- HCVS: Horn Clauses for Verification and Synthesis
- Tutorial: Certified Functional (Co)programming with Isabelle/HOL
- Vampire 2017: The 4th Vampire Workshop
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?
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
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.
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.
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.
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.