Jonas's talk

community-meetings.html

@@ -72,6 +72,36 @@ <h1>FPBench Meetings</h1>
 
 -->
 
+    <div class="community-talk">
+      <div class="when">
+        September 7, 2023
+      </div>
+      <div class="title">
+        A PVS Formalization of Taylor Error Expressions
+      </div>
+      <div class="speaker">
+        Jonas Katona, Yale University
+      </div>
+      <div class="abstract">
+        Due to the limits of finite precision arithmetic, as one works
+        with floating-point representations of real numbers in
+        computer programs, round-off errors tend to accumulate under
+        mathematical operations and may become unacceptably large.
+        Symbolic Taylor Error Expressions is a technique used in the
+        tool FPTaylor to bound the round-off errors accumulated under
+        differentiable mathematical operations which provides a good
+        trade-off between efficiency and accuracy. In this
+        presentation, I will present a formally verified
+        implementation of Symbolic Taylor Error Expressions in a
+        specification language, automated theorem prover, and
+        typechecker called Prototype Verification System (PVS). I will
+        also go over how this formal specification in PVS will enable
+        the integration of Symbolic Taylor Expressions in PRECiSA, a
+        prototype static analysis tool that can compute verified
+        round-off error bounds for floating-point programs.
+      </div>
+    </div>
+
     <div class="community-talk">
       <div class="when">
         August 3, 2023