Friday, November 11, 2022
11/11/2022 - 10:30am
A relaxed-pace seminar on impromptu subjects related to the interests of the audience.
Everyone is welcome.
The subjects are geometry, probability, combinatorics, dynamics, and more!
11/11/2022 - 12:00pm
In a broad sense, formal methods are mathematically rigorous techniques used to describe, monitor, and check system properties and limitations in computer systems, along with the fields in which these techniques can generally be applied, guidelines for how these techniques can be used, and tools or software used in the implementation of these techniques. One application of formal methods is in monitoring and checking the propagation of errors in computational programs. 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 soundly bound the round-off error of mathematical operators which provide a good trade-off between efficiency and accuracy.
In this presentation, I will give a general overview to formal methods, the history of formal methods, and how formal methods are applied in various fields of engineering and industry. Afterwards, 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 these error expressions can be used in PRECiSA, a prototype static analysis tool that can compute verified round-off error bounds for floating-point programs. Time permitting, I will introduce other theorems, properties, and structures which I have proven in PVS for inclusion in the NASA PVS Library.
11/11/2022 - 2:00pm
Abstract: Uniqueness of limit structures is a central topic in many problems in geometry and PDEs. In geometric analysis, Łojasiewicz inequality has been widely used a robust tool to derive uniqueness. In this talk, I will give a brief introduction to Łojasiewicz inequalities and their applications, focusing on two problems on uniqueness of limit – for the tangent cone of an Einstein manifold, and for the tangent flow of mean curvature flow.