-
Notifications
You must be signed in to change notification settings - Fork 0
/
workshops.txt
205 lines (163 loc) · 8.81 KB
/
workshops.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
<h1>Workshops and Tutorials</h1>
<p>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 <b>Jupiter</b>. The Jupiter building is the one numbered 2 on the <a href="venue.html">map</a> found under Local info.</p>
<p><b>6 Aug 2017:</b></p>
<ul>
<li><a href="workshops.html#arcade">ARCADE: Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements</a></li>
<li><a href="workshops.html#pcr">PCR'17: Workshop on Parallel Constraint Reasoning</a></li>
<li><a href="workshops.html#thedu">ThEdu'17: Theorem Prover Components for Educational Software</a></li>
</ul>
<p><b>7 Aug 2017:</b></p>
<ul>
<li><a href="workshops.html#hcvs">HCVS: Horn Clauses for Verification and Synthesis</a></li>
<li><a href="workshops.html#coprog">Tutorial: Certified Functional (Co)programming with Isabelle/HOL</a></li>
<li><a href="workshops.html#vampire">Vampire 2017: The 4th Vampire Workshop</a></li>
</ul>
<p>The traditional <a href="http://www.cs.miami.edu/~tptp/CASC/26/">CADE ATP System Competition (CASC)</a> will also be held at CADE-26. CASC will be held during the main CADE conference on 9 Aug 2017.</p>
<br><a id="arcade"></a>
<h2>ARCADE: Automated Reasoning: Challenges, Applications, Directions,
Exemplary Achievements</h2>
<p>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:</p>
<ul>
<li>Challenges: What are the next grand challenges for research on
automated reasoning?</li>
<li>Applications: Is automated reasoning applicable in real-world
(industrial) scenarios.</li>
<li>Directions: Based on the grand challenges and requirements from
real-world applications, what are the research directions the community
should promote?</li>
<li>Exemplary Achievements: What are the landmark achievements of
automated reasoning whose influence reached far beyond the CADE
community itself?</li>
</ul>
<p>Time: Sunday 6 Aug 8:55–17:00</p>
<p>Place: <b>Room 243</b>, Jupiter building</p>
<p><a href="http://www.cs.man.ac.uk/~regerg/arcade/">ARCADE
workshop webpage</a></p>
<p>Organisers:
<a href="http://www.cs.man.ac.uk/~regerg/research.html">Giles Reger</a>,
<a href="https://www21.in.tum.de/~traytel/">Dmitriy Traytel</a></p>
<br><a id="hcvs"></a>
<h2>HCVS: Horn Clauses for Verification and Synthesis</h2>
<p>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.</p>
<p>Topics of interest include, but are not limited to the use of Horn
clauses, constraints, and related formalisms in the following areas:</p>
<ul>
<li>Automated deduction</li>
<li>Analysis and verification of programs in various programming paradigms
(e.g., imperative, object-oriented, functional, logic, higher-order,
concurrent)</li>
<li>Program synthesis</li>
<li>Program testing</li>
<li>Program transformation</li>
<li>Constraint solving</li>
<li>Type systems</li>
<li>Case studies and tools</li>
<li>Challenging problems</li>
</ul>
<p>Time: Sunday 6 Aug 9:00–17:00</p>
<p>Place: <b>Room 218</b>, Jupiter building</p>
<p><a href="http://software.imdea.org/Conferences/hcvs17/">HCVS'17 workshop webpage</a></p>
<p>Organisers:
<a href="https://es-static.fbk.eu/people/griggio/">Alberto Griggio</a>,
<a href="https://cliplab.org/~herme/">Manuel Hermenegildo</a></p>
<br><a id="pcr"></a>
<h2>PCR'17: Workshop on Parallel Constraint Reasoning</h2>
<p>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.</p>
<p>Time: Sunday 6 Aug 9:00 - 16:30</p>
<p>Place: <b>Room 219</b>, Jupiter building</p>
<p><a href="http://pcr17.inf.usi.ch/">PCR'17 workshop webpage</a></p>
<p>Organisers:
<a href="http://www.inf.usi.ch/postdoc/hyvarinen/">Antti Hyvärinen</a>,
<a href="https://www.microsoft.com/en-us/research/people/cwinter/">Christoph M. Wintersteiger</a></p>
<br><a id="thedu"></a>
<h2>ThEdu'17: Theorem Prover Components for Educational Software</h2>
<p>(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:</p>
<ul>
<li>methods of automated deduction applied to checking students' input;</li>
<li>methods of automated deduction applied to prove post-conditions for
particular problem solutions;</li>
<li>combinations of deduction and computation enabling systems to propose
next steps;</li>
<li>automated provers specific for dynamic geometry systems;</li>
<li>proof and proving in mathematics education.</li>
</ul>
<p>Time: Sunday 6 Aug 9:00–17:00</p>
<p>Place: <b>Room 218</b>, Jupiter building</p>
<p><a href="http://www.uc.pt/en/congressos/thedu/thedu17">ThEdu'17
workshop webpage</a></p>
<p>Organisers:
<a href="https://www.mat.uc.pt/~pedro/">Pedro Quaresma</a> and
<a href="http://www.ist.tugraz.at/neuper/">Walther Neuper</a></p>
<br><a id="coprog"></a>
<h2>Tutorial: Certified Functional (Co)programming with Isabelle/HOL</h2>
<p>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.</p>
<p>Time: Monday 7 Aug 9:00–17:00</p>
<p>Place: <b>Room 219</b>, Jupiter building</p>
<p><a href="http://matryoshka.gforge.inria.fr/cade26-tutorial/">Tutorial
webpage</a></p>
<p>Organisers:
<a href="https://people.mpi-inf.mpg.de/~jblanche/">Jasmin Blanchette</a>,
<a href="http://www.infsec.ethz.ch/people/andreloc.html">Andreas Lochbihler</a>,
<a href="http://www4.in.tum.de/~popescua/">Andrei Popescu</a>,
<a href="https://www21.in.tum.de/~traytel/">Dmitriy Traytel</a></p>
<br><a id="vampire"></a>
<h2>Vampire 2017: The 4th Vampire Workshop</h2>
<p>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</p>
<ul>
<li>what is essential for substantial progress in theorem proving tools;</li>
<li>what are the best implementation principles to be used;</li>
<li>what are the best heuristics and strategies, depending on application areas;</li>
<li>both successful and unsuccessful case studies;</li>
<li>missing features in modern theorem provers.</li>
</ul>
<p>Time: Monday 7 Aug 9:30–17:00</p>
<p>Place: <b>Room 243</b>, Jupiter building</p>
<p><a href="http://easychair.org/smart-program/Vampire17/">Vampire
2017 workshop webpage</a></p>
<p>Organisers:
<a href="http://forsyte.at/people/kovacs/">Laura Kovacs</a> and
<a href="http://voronkov.com/">Andrei Voronkov</a></p>