From efd1caabfa57821fb6bc1c1db49774eb5f9a0700 Mon Sep 17 00:00:00 2001
From: Pavel Panchekha <me@pavpanchekha.com>
Date: Wed, 30 Aug 2023 16:00:50 -0600
Subject: [PATCH] Jonas's talk

---
 community-meetings.html | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/community-meetings.html b/community-meetings.html
index aa9b0e1..3014d6c 100644
--- a/community-meetings.html
+++ b/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