-
Notifications
You must be signed in to change notification settings - Fork 0
/
program.html
144 lines (120 loc) · 10.6 KB
/
program.html
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
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>CADE-26: Conference Program</title>
<link rel="stylesheet" href="main.css">
</head>
<body>
<header>
<img src="top.png" alt="CADE-26">
</header>
<nav>
<ul>
<li><a href="index.html">Home</a></li>
<li><a href="program.html">Conference Program</a></li>
<li><a href="workshops.html">Workshops & Tutorials</a></li>
<li><a href="http://www.cs.miami.edu/~tptp/CASC/26/" target="_blank">CASC</a></li>
<li><a href="org.html">Organization</a></li>
<li><a href="excursion.html">Excursion to Marstrand</a></li>
<li><a href="registration.html">Registration</a></li>
<li><a href="venue.html">Local Info, Venue & Hotels</a></li>
</ul>
</nav>
<article><div class="content">
<h1>Program</h1>
<p>All talks are held in Lindholmen Science Park, in the conference hall. The conference hall is in the building numbered 1 in the <a href="venue.html">map</a> found under Local info.</p>
<h2>Day 1: Tuesday 8 Aug 2017</h2>
<p>08:00 - 08:45  <b>Registration</b></p>
<p>08:45  <b>Conference Opening</b></p>
<p>09:00 - 10:00  <b>Invited talk: Philippa Gardner</b></p>
<p>10:00 - 10:30  <b>Coffee</b></p>
<p>10:30 - 12:00  <b>Session 1:  Theory combination</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_4">Satisfiability Modulo Theories and Assignments</a>.</b> Maria Paola Bonacina, Stéphane Graham-Lengrand and Natarajan Shankar
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_5">Notions of Knowledge in Combinations of Theories Sharing Constructors</a>.</b> Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_6">On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic</a>.</b> Marco Voigt, Christoph Weidenbach and Matthias Horbach
</ul>
<p>12:00 - 13:30  <b>Lunch break</b></p>
<p>13:30 - 15:30  <b>Session 2: Satisfiability</b></p>
<ul>
<li><b style="color: red">[Best Paper]</b> <b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_9">Short Proofs without New Variables</a>.</b> Marijn Heule, Benjamin Kiesl and Armin Biere
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_7">Satisfiability Modulo Transcendental Functions via Incremental Linearization</a>.</b> Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri and Roberto Sebastiani
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_8">Satisfiability Modulo Bounded Checking</a>.</b> Simon Cruanes
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_10">Relational Constraint Solving in SMT</a>.</b> Baoluo Meng, Andrew Reynolds, Cesare Tinelli and Clark Barrett
</ul>
<p>15:30 - 16:00  <b>Coffee</b></p>
<p>16:00 - 17:30  <b>Session 3: Decision procedures</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_11">Decision Procedures for Theories of Sets with Measures</a>.</b> Markus Bender and Viorica Sofronie-Stokkermans
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_12">A Decision Procedure for Restricted Intensional Sets</a>.</b> Maximiliano Cristia and Gianfranco Rossi
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_13">Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints</a>.</b> Andreas Teucke and Christoph Weidenbach
</ul>
<p>17:30 - 19:00  <b>Reception by the City of Gothenburg (at the conference venue)</b></p>
<h2>Day 2: Wednesday 9 Aug 2017</h2>
<p>09:00 - 10:00  <b>Invited <a href="https://www.eurai.org/">EurAI</a> talk: Grant Passmore</b></p>
<p>10:00 - 10:30  <b>Coffee and start of <a href="http://www.cs.miami.edu/~tptp/CASC/26/">CASC</a></b></p>
<p>10:30 - 12:00  <b>Session 1: Proof certification</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_14">Efficient Certified RAT Verification</a>.</b> Luís Cruz-Filipe, Marijn Heule, Warren Hunt, Matt Kaufmann and Peter Schneider-Kamp
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_15">Efficient Verified (UN)SAT Certificate Checking</a>.</b> Peter Lammich
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_16">Translating between implicit and explicit versions of proof</a>.</b> Roberto Blanco, Zakaria Chihani and Dale Miller
</ul>
<p>12:00 - 13:30  <b>Lunch break</b></p>
<p>13:30 - 15:30  <b>Session 2: First order logic</b></p>
<ul>
<li><b style="color: red">[Best Paper]</b> <b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_17">A Unifying Principle for Clause Elimination in First-Order Logic</a>.</b> Benjamin Kiesl and Martin Suda
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_18">Splitting Proofs for Interpolation</a>.</b> Bernhard Gleiss, Laura Kovacs and Martin Suda
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_19">Detecting Inconsistencies in Large First-Order Knowledge Bases</a>.</b> Stephan Schulz, Geoff Sutcliffe, Josef Urban and Adam Pease
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_20">Theorem Proving for Metric Temporal Logic over the Naturals</a>.</b> Ullrich Hustadt, Ana Ozaki and Clare Dixon
</ul>
<p>15:30 - 16:00  <b>Coffee</b></p>
<p>16:00 - 17:45  <b>Session 3: System descriptions</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_21">Scavenger 0.1: A Theorem Prover Based on Conflict Resolution</a>.</b> Bruno Woltzenlogel Paleo, Daniyar Itegulov and John Slaney
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_22">WorkflowFM: A logic-based formal verification framework for process specification and composition</a>.</b> Petros Papapanagiotou and Jacques Fleuriot
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_23">DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL</a>.</b> Florian Lonsing and Uwe Egly
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_24">CSI: New Evidence - A Progress Report</a>.</b> Julian Nagele, Bertram Felgenhauer and Aart Middeldorp
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_25">Scalable Fine-Grained Proofs for Formula Processing</a>.</b> Haniel Barbosa, Jasmin Christian Blanchette and Pascal Fontaine
</ul>
<h2>Day 3: Thursday 10 Aug 2017</h2>
<p>09:00 - 10:00  <b>Invited talk: June Andronick</b></p>
<p>10:00 - 10:30  <b>Coffee</b></p>
<p>10:30 - 12:00  <b>Session 1: Confluence and termination</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_26">Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems</a>.</b> Christian Sternagel and Thomas Sternagel
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_27">A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms</a>.</b> Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_28">Certifying Safety and Termination Proofs for Integer Transition Systems</a>.</b> Marc Brockschmidt, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
</ul>
<p>12:00 - 13:30  <b>Lunch break</b></p>
<p>13:00 - 14:30  <b>Business Meeting</b></p>
<p>14:30 -   <a href="excursion.html"><b>Excursion</b></p></a>
<h2>Day 4: Friday 11 Aug 2017</h2>
<p>08:45 - 10:00  <b>Best Paper Award, Skolem Award, Herbrand Award </b></p>
<p>10:00 - 10:30  <b>Coffee</b></p>
<p>10:30 - 12:00  <b>Session 1: Program verification</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_29">Biabduction (and Related Problems) in Array Separation Logic</a>.</b> James Brotherston, Nikos Gorogiannis and Max Kanovich
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_30">Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof</a>.</b> Gadi Tellez and James Brotherston
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_31">Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints</a>.</b> Zhaowei Xu, Taolue Chen and Zhilin Wu
</ul>
<p>12:00 - 13:30  <b>Lunch break</b></p>
<p><p>13:30 - 15:30  <b>Session 2: Applications and heuristics</b></p>
<ul>
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_33">The binomial pricing model in finance: a formalization in Isabelle</a>.</b> Mnacho Echenim and Nicolas Peltier
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_32">A Proof Strategy Language and Proof Script Generation for Isabelle/HOL</a>.</b> Yutaka Nagashima and Ramana Kumar
<li><b><a target="_blank" href="https://link.springer.com/chapter/10.1007/978-3-319-63046-5_34">Monte Carlo Tableau Proof Search</a>.</b> Michael Färber, Cezary Kaliszyk and Josef Urban
</ul>
<p><p>13:30 - 15:30  <b>TPTP tea party</b> (come to information desk at 13:20)</p>
<p><p>15:30 -  <b>Closing remarks</b></p>
</div></article>
<footer style="text-align:center;">
<div style="width: 100%; text-align:left; padding-left: 15px; padding-top: 10px; padding-bottom: 10px;">CADE-26 is grateful for sponsorship from:</div>
<a href="https://www.microsoft.com/en-us/research/"><img src="msr.png" style="width: 200px; padding-top:15px; padding-left:30px;" alt="Microsoft Research"/></a>
<a href="http://international.goteborg.se/"><img src="gbg.png" style="padding-top:15px; width: 200px; padding-left:30px;" alt="Gothenburg City"/></a><br>
<a href="https://www.eurai.org/"><img src="EurAi-logo.png" style="padding-top:10px;" alt="EurAI"/></a>
<a href="http://www.chalmers.se/en/areas-of-advance/ict/Pages/default.aspx"><img src="aoa.png" style="width: 280px; padding-left:30px; padding-top:15px;" alt="Information and Communication Technologies Chalmers Area of Advance"/></a>
<a href="http://www.springer.com/gp/"><img src="springer.gif" style="padding-left:30px; padding-top:15px;" alt="Springer"/></a><br>
</footer>
</body>
</html>