|
| 1 | +--- |
| 2 | +layout: default |
| 3 | +title: events |
| 4 | +--- |
| 5 | + |
| 6 | +<h1>CENTAUR Annual Meeting 2025</h1> |
| 7 | +<h4>Paul Brest Hall<br/> |
| 8 | +555 Salvatierra Walk<br/> |
| 9 | +Stanford, CA 94305</h4> |
| 10 | +<br/> |
| 11 | +<a href="https://www.eventbrite.com/e/2025-centaur-annual-meeting-tickets-1528070553159" class="btn"> |
| 12 | +Register |
| 13 | +</a> |
| 14 | +<!--<a href="https://youtu.be/g4yNwnGNANI?si=IwMv4t33gyCxMHBv" class="btn"> |
| 15 | +Recap Video |
| 16 | +</a>--> |
| 17 | + |
| 18 | +<h2>Tuesday September 23</h2> |
| 19 | +<table> |
| 20 | +<tr> |
| 21 | +<td style="width:20%;">8:30am-9:00am</td> |
| 22 | +<td style="width:32">Breakfast and Registration</td> |
| 23 | +<td style="width:18%;"></td> |
| 24 | +<td style="width:20%;"></td> |
| 25 | +</tr> |
| 26 | + |
| 27 | +<tr> |
| 28 | +<td>9:00am-9:10am</td> |
| 29 | +<td><a href="https://youtu.be/KiyOg4924x0">Opening Remarks</a></td> |
| 30 | +<td>Clark Barrett</td> |
| 31 | +<td>Director of Centaur</td> |
| 32 | +</tr> |
| 33 | + |
| 34 | +<tr> |
| 35 | +<td colspan="4" style="text-align:center;font-weight:bold;"> |
| 36 | +Session I |
| 37 | +</td> |
| 38 | +</tr> |
| 39 | +<tr> |
| 40 | +<td>9:10am-9:30am</td> |
| 41 | +<td>CSLib: A Formal Methods Platform for the Future of Everything</td> |
| 42 | +<td>Clark Barrett</td> |
| 43 | +<td>Director of Centaur</td> |
| 44 | +</tr> |
| 45 | +<tr> |
| 46 | +<td>9:30am-9:50am</td> |
| 47 | +<td>Lean SMT: An SMT Tactic for Discharging Proof Goals in Lean</td> |
| 48 | +<td>Abdalrhman Mohamed</td> |
| 49 | +<td>PhD Student</td> |
| 50 | +</tr> |
| 51 | +<tr> |
| 52 | +<td>9:50am-10:20am</td> |
| 53 | +<td>Coffee break</td> |
| 54 | +<td></td> |
| 55 | +<td></td> |
| 56 | +</tr> |
| 57 | + |
| 58 | +<tr> |
| 59 | +<td colspan="4" style="text-align:center;font-weight:bold;"> |
| 60 | +Session II |
| 61 | +</td> |
| 62 | +</tr> |
| 63 | + |
| 64 | +<tr> |
| 65 | +<td>10:20am-10:40am</td> |
| 66 | +<td>Verification and Synthesis of Spatial Implications for Bounding Volume Hierarchy Traversals</td> |
| 67 | +<td>Nestan Tsiskaridze</td> |
| 68 | +<td>Research Scientist</td> |
| 69 | +</tr> |
| 70 | +<tr> |
| 71 | +<td>10:40am-11:00am</td> |
| 72 | +<td>Verifying Nonlinear Neural Feedback Systems Using Polyhedral Enclosures</td> |
| 73 | +<td>Samuel Akinwande</td> |
| 74 | +<td>PhD Student</td> |
| 75 | +</tr> |
| 76 | +<tr> |
| 77 | +<td>11:00am-11:20am</td> |
| 78 | +<td>Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL</td> |
| 79 | +<td>Hanna Lachnitt</td> |
| 80 | +<td>PhD Student</td> |
| 81 | +</tr> |
| 82 | + |
| 83 | + |
| 84 | +<tr> |
| 85 | +<td>11:20am-11:50am</td> |
| 86 | +<td>Coffee break</td> |
| 87 | +<td></td> |
| 88 | +<td></td> |
| 89 | +</tr> |
| 90 | + |
| 91 | +<tr> |
| 92 | +<td colspan="4" style="text-align:center;font-weight:bold;"> |
| 93 | +Session III |
| 94 | +</td> |
| 95 | +</tr> |
| 96 | + |
| 97 | +<tr> |
| 98 | +<td>11:50am-12:20pm</td> |
| 99 | +<td>Lightning Talks</td> |
| 100 | +<td></td> |
| 101 | +<td></td> |
| 102 | +</tr> |
| 103 | + |
| 104 | +<tr> |
| 105 | +<td>12:20pm-2:20pm</td> |
| 106 | +<td>Lunch and Poster Session</td> |
| 107 | +<td></td> |
| 108 | +<td></td> |
| 109 | +</tr> |
| 110 | + |
| 111 | +<tr> |
| 112 | +<td colspan="4" style="text-align:center;font-weight:bold;"> |
| 113 | +Session IV |
| 114 | +</td> |
| 115 | +</tr> |
| 116 | +<tr> |
| 117 | +<td>2:20pm-2:40pm</td> |
| 118 | +<td>Bit-precise Reasoning with Parametric Bit-vectors</td> |
| 119 | +<td>Yoni Zohar</td> |
| 120 | +<td>Professor, Bar-Ilan University</td> |
| 121 | +</tr> |
| 122 | +<tr> |
| 123 | +<td>2:40pm-3:00pm</td> |
| 124 | +<td>Integer Reasoning Modulo Different Constants in SMT</td> |
| 125 | +<td>Elizaveta Pertseva</td> |
| 126 | +<td>PhD Student</td> |
| 127 | +</tr> |
| 128 | +<tr> |
| 129 | +<td>3:00pm-3:20pm</td> |
| 130 | +<td>Bounded Quantifiers for Finite Relations</td> |
| 131 | +<td>Mudathir Mohamed</td> |
| 132 | +<td>PhD Student at University of Iowa</td> |
| 133 | +</tr> |
| 134 | +<td>3:20pm-3:50pm</td> |
| 135 | +<td>Coffee break</td> |
| 136 | +<td></td> |
| 137 | +<td></td> |
| 138 | +</tr> |
| 139 | + |
| 140 | +<tr> |
| 141 | +<td colspan="4" style="text-align:center;font-weight:bold;"> |
| 142 | +Session V |
| 143 | +</td> |
| 144 | +</tr> |
| 145 | +<tr> |
| 146 | +<td>3:50pm-4:10pm</td> |
| 147 | +<td>Leveraging Subproblems for Improved SMT Solver Performance</td> |
| 148 | +<td>Amalee Wilson</td> |
| 149 | +<td>PhD Student</td> |
| 150 | +</tr> |
| 151 | +<tr> |
| 152 | +<td>4:10pm-4:30pm</td> |
| 153 | +<td>Towards SMT Solver Stability via Input Normalization</td> |
| 154 | +<td>Daneshvar Amrollahi</td> |
| 155 | +<td>PhD Student</td> |
| 156 | +</tr> |
| 157 | +<tr> |
| 158 | +<td>4:30pm-4:50pm</td> |
| 159 | +<td></td> |
| 160 | +<td>Rachel Cleaveland</td> |
| 161 | +<td>PhD Student</td> |
| 162 | +</tr> |
| 163 | +<tr> |
| 164 | +<tr> |
| 165 | +<td>4:50pm-5:00pm</td> |
| 166 | +<td>Closing Remarks</td> |
| 167 | +<td>Clark Barrett</td> |
| 168 | +<td>Director of Centaur</td> |
| 169 | +</tr> |
| 170 | + |
| 171 | +<tr> |
| 172 | +<td colspan="4" style="text-align:center;font-weight:bold;"> |
| 173 | +Reception |
| 174 | +</td> |
| 175 | +</tr> |
| 176 | +<tr> |
| 177 | +<td>5:00pm-7:00pm</td> |
| 178 | +<td colspan="3">Reception</td> |
| 179 | +</tr> |
| 180 | + |
| 181 | +</table> |
0 commit comments