the game of swapping

_layouts/programme.html

@@ -208,11 +208,11 @@ <h3>more like a draft than final</h3>
 
     <tr class="track-key">
       <td>
-	16:00  &ndash; 17:30
+	16:00  &ndash; 17:45
 	<br>
 	Room: SR7+8
       </td>
-      <td>{{ session("#6a", "Richard Bubel", [113,114,115]) }}</td>
+      <td>{{ session("#6a", "Richard Bubel", [113,114,115, 208]) }}</td>
     </tr>
 
     <tr class="track-keymaera">
@@ -271,7 +271,7 @@ <h3>more like a draft than final</h3>
 
     <tr class="">
       <th>14:00  &ndash; 15:30</th>
-      <td>{{ session("#3", "X", [207,208,209]) }}</td>
+      <td>{{ session("#3", "X", [207,209]) }}</td>
     </tr>
 
     <tr class="break">
@@ -304,21 +304,21 @@ <h3>more like a draft than final</h3>
     </tr>
 
     <tr>
-      <th>09:00 &ndash; 10:30</th>
+      <th>09:00 &ndash; 10:45</th>
       <td>
-	{{ session("#8", "X", [30,31, 301]) }}
+	{{ session("Isabelle", "X", [30,31, 301, 34]) }}
       </td>
     </tr>
 
     <tr class="break">
-      <th>10:30 &ndash;11:00</th>
+      <th>10:45 &ndash;11:10</th>
       <td>Coffee</td>
     </tr>
 
     <tr>
       <th>11:00  &ndash; 12:30</th>
       <td>
-	{{ session("#8", "X", [32,33,34,35,37,38]) }}
+	{{ session("#8", "X", [32,33,35,37]) }}
       </td>
     </tr>
 

talks/ahrendt.md

@@ -2,9 +2,8 @@
 author: "Wolfgang Ahrendt"
 kind: "Short Talk (10 min. + 5 min.)"
 track: "KeYmaera Track"
-title: "tbd"
+title: "On proving that an unsafe controller is not proven safe"
 slot: 219
 length: 15 
 ---
-
-tbd.
+Formal verification of cyber-physical systems is one way to guarantee safety. However, care must be taken because modelling errors might result in proving a faulty controller safe, which is potentially catastrophic in practice. We deal with two such modelling errors in differential dynamic logic, and provide conditions under which these two modelling errors cannot cause a faulty controller to be proven safe. We also show how these conditions can be proven with help of KeYmaera X.

talks/bordis.md

@@ -3,7 +3,7 @@ author: "Tabea Bordis"
 kind: "Either Regular or Short. Whatever fits best into the program."
 track: "Common Track"
 title: "Free Facts: An Alternative to Inefficient Axioms in Dafny"
-slot:  13
+slot:  15
 length: 30
 ---
 

talks/heydari-tabar.md

@@ -3,7 +3,7 @@ author: "Asmae Heydari-Tabar"
 kind: "Short Talk (10 min. + 5 min.)"
 track: "Common Track, KeY-only Track"
 title: "Data Dependence Logic: Applications"
-slot: 15
+slot: 209
 length: 30
 ---
 

talks/lohar.md

@@ -3,8 +3,8 @@ author: "Debasmita Lohar"
 kind: "Regular Talk (20 min. + 10 min.)"
 track: "Common Track"
 title: "Towards Practical Analysis and Optimization for Finite-Precision"
-length: 22
-slot: 22
+length: 30
+slot: 13
 ---
 
 Finite-precision programs inevitably introduce numerical uncertainties due to input noises and finite-precision (roundoff) errors inherent in arithmetic operations. Furthermore, implementing these programs on hardware necessitates a trade-off between accuracy and efficiency. Therefore, it is crucial to ensure that numerical uncertainties remain acceptably small and to optimize implementations for accurate results tailored to specific applications.

talks/pascual.md

@@ -1,8 +1,9 @@
 ---
-author: "[email protected]"
+author: "Romain Pascual"
 kind: "Regular Talk (20 min. + 10 min.)"
 track: "Common Track"
 title: "Convide or Formal reasoning for geometric modeling"
-length: 30
+length: 22
+slot: 22
 ---