CADE-26

Workshops and Tutorials

The following workshops and tutorials will be organised alongside CADE-26 on 6 and 7 Aug 2017.

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:

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:

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.

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:

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.

Organisers: Jasmin Blanchette, 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

Vampire 2017 workshop webpage

Organisers: Laura Kovacs and Andrei Voronkov