-
Notifications
You must be signed in to change notification settings - Fork 0
/
program.txt
107 lines (85 loc) · 8.91 KB
/
program.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
<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>