BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Michigan Institute for Computational Discovery and Engineering - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://micde.umich.edu
X-WR-CALDESC:Events for Michigan Institute for Computational Discovery and Engineering
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Detroit
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20240310T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20241103T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20250309T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20251102T060000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:20260308T070000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:20261101T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Detroit:20250121T150000
DTEND;TZID=America/Detroit:20250121T160000
DTSTAMP:20260614T234717
CREATED:20250106T213237Z
LAST-MODIFIED:20250128T161655Z
UID:10000790-1737471600-1737475200@micde.umich.edu
SUMMARY:MICDE-CSE Seminar: Andrew Appel\, Professor\, Princeton University
DESCRIPTION:Bio: Andrew Appel is Eugene Higgins Professor Computer Science\, and served from 2009-2015 as Chair of Princeton’s CS department. His research is in software verification\, computer security\, programming languages and compilers\, and technology policy. He received his A.B. summa cum laude in physics from Princeton in 1981\, and his Ph.D. in computer science from Carnegie Mellon University in 1985. Professor Appel has been editor in chief of ACM Transactions on Programming Languages and Systems and is a fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s)\, Standard ML of New Jersey (1990s)\, Foundational Proof-Carrying Code (2000s)\, and the Verified Software Toolchain (2010-present). \nFormally Verified Numerical Methods\nAbstract: Formal machine-checked program verification uses mechanized logical tools to connect low-level programs to the specifications of the algorithms they are supposed to implement. The same program verification tools can work in many application domains. But it’s not enough just to implement an algorithm; the program is fully “correct” only if the algorithm (provably) computes an answer to the problem or question of interest. Proofs of algorithm correctness rely on the mathematics of the application domains\, and each domain has its own mathematics.\nIn recent years we have applied this method to numerical methods (algorithms for scientific computing) and numerical analysis (reasoning about the accuracy of those methods)\, with machine-checked proofs formally connected to low-level program-correctness proofs. I will discuss the results of the numerical integration of differential equations and the solving of linear systems. Some of these results are joint work with Ariel Kellison and David Bindel (Cornell)\, Mohit Tekriwal and Jean-Baptiste Jeannin (Michigan).
URL:https://micde.umich.edu/event/micde-cse-seminar-andrew-appel-professor-princeton-university/
LOCATION:BBB 3725\, 2260 Hayward St.\, Ann Arbor\, United States
CATEGORIES:Micde,Micde Seminar
ATTACH;FMTTYPE=image/png:https://micde.umich.edu/wp-content/uploads/2025/01/Andrew-Apple.png
END:VEVENT
END:VCALENDAR