Kei Imada

A Hoare Logic for Continuous-Time Stochastic Processes

A Nonstandard Temporal Logic for Continuous-Time Systems

A Hoare Logic for Continuous-Time Stochastic Systems

Abstract

Continuous-time stochastic processes like Brownian motion model noise in the physical world, from particles in a fluid to interest rates and stock prices. We have many tools for reasoning about probabilistic programs, but it remains unclear how to apply them to continuous-time stochastic processes. In this talk I will try to convince you that we can reason about these processes the way we reason about programs: by writing them as ordinary probabilistic programs with a small time step dt and taking dt to 0.

I will define a continuous semantics for pWhile-dt, a probabilistic imperative language with a time step variable dt, by collecting the limit points of its standard program semantics as dt approaches to 0. I will present a Hoare logic over our continuous semantics in which properties proved on the standard semantics for small dt transfer to the continuous semantics. To demonstrate our logic, we will verify properties of Brownian motion and geometric Brownian motion with loop invariants. Finally, I will present a prototype implementation that applies off-the-shelf probabilistic program analysis tools to reason about continuous-time stochastic processes.

This is joint work with Justin Hsu.

A Nonstandard Temporal Logic for Continuous-Time Verification

Cornell University

Advisor: Justin Hsu

GPA: 4.1

Relevant Coursework

• Introduction to Kleene Algebra
• Category Theory for Computer Scientists
• Applied Logic
• Advanced Compilers
• Program Synthesis
• Formal Methods in Robotics

Swarthmore College

Thesis: The Equivalence of Typed λ Calculi and Cartesian Closed Categories

Cumulative GPA: 3.94 Major GPA: 3.95

Relevant Coursework

• Operating Systems
• Artificial Intelligence
• Mobile Robotics
• Computer Networks
• Natural Language Processing
• Programming Languages
• Parallel and Distributed Systems
• Algorithms
• Data Structures and Algorithms
• Introduction to Computer Systems
• Category Theory
• Topology
• Modeling
• Real Analysis
• Basic Differential Equations
• Modern Algebra
• Several Variable Calculus
• Honors Linear Algebra
• Introduction to Computer Science
• Introduction to Linguistics
• Introduction to Psychology

Budapest Semesters in Mathematics

Relevant Coursework

• Conjecture & Proof
• Real Functions and Measures
• Introduction to Topology
• Theory of Computing
• Mathematical Cryptography
• Philosophy of Mathematics

Research Assistant

• Developed a logic to prove temporal properties about hybrid systems using nonstandard analysis
• Built a programming language using menhir to model hybrid systems and prove loop invariants with Z3
• Proved critical safety properties of simplified train control and water-level monitor systems

Software Engineer

• Developed an internal Python iptables library with in-memory caching and batch-commit functionalities tailored for performance
• Improved existing Python iptables library’s performance by orders of magnitude
• Integrated iptables into FlashBlade clusters and improved its performance by removing unnecessary system calls

Software Engineer Intern

• Designed and implemented a scalable web analytics tool that detects and diagnoses SSD drive failures
• Improved latency by 200% by introducing caching layers that store structured responses from Amazon Redshift
• Designed the front end using React and Typescript, with ag-grid, highcharts, and react-select as core components

Network RAM Research Assistant

• Employed machine learning analysis methods on system statistics to predict when the system is about to swap to disk
• Headed the development of the user level policy infrastructure in C for the NSwap network RAM implementation
• Reduced the runtime of memory intensive benchmarks by 99% and their swap disk usage by 97%

Project Lead

• One of 15 students selected to maintain servers that host web servers, mail servers, and other critical services
• Collaborate with other SCCS members to develop various services for the Swarthmore College community
• Administer SCCS-run servers and troubleshoot outages

Computer Science Teaching Assistant

• Assist computer science professors in lectures and help their students learn concepts in data structures, algorithms, and computer systems
• Lead weekly support sessions to clarify class material and provide lab assistance to students
• Mentor students through structure, logic, and syntax errors while teaching debugging techniques
• Communicate with students, professors, and other peer mentors to explain difficult concepts in clear, concise ways

Mathematics Clinician

• Facilitate weekly support sessions to help over 100 students for all mathematics classes offered at the college
• Guide students through difficult concepts in various courses such as real analysis, modern algebra, multivariable calculus, and linear algebra

Information Technology Services Associate

• Answer questions and troubleshoot technical problems on software, networks, accounts, phones, printers, and mobile devices
• Manage and troubleshoot computers and printers in public spaces on the Swarthmore College campus

SwatPrereqView

• Devised a website that visualized prerequisites for 1,850 Swarthmore courses with a total of 1,000 prerequisites
• Designed the frontend using Semantic UI and vis.js
• Built the backend with Flask and a parallel Beautiful Soup 4 scraper in Python 3

Airpool

• Headed the development team for a website that would help Swarthmore students schedule carpool rides to and from the airport
• Scheduled more than 150 rides with more than 1,000 views (Swarthmore Facebook page no longer a mess before break)
• Designed the frontend using DataTables, Fullcalendar, JQuery, and Semantic UI
• Implemented the backend with Flask and MySQL with LDAP authentication

Three-Dimensional Fractal Rendering Software on GPU Clusters

• Developed a 3D fractal renderer on a GPU cluster using CUDA C/C++ and OpenMPI with Jonah Langlieb and Liam Packer
• Generated a 8192x8192 PNG image of a tenth iteration 3D fractal in 30 seconds using distributed ray marching techniques
• Tested benchmarks of the software on Swarthmore College's commodity computer cluster
• Co-authored a report about the project and its scalability

Real-time IIR Filtering Python Package

• Engineered a real-time Butterworth type signal filtering package in Python that could filter more than 250 kHz in real-time
• Identified and eliminated bottlenecks in the code to increase its processing speed by more than 250 times
• Devised a graphic user interface in Python using tkinter and the signal filtering package to demonstrate its uses
• Created a wave audio file frequency filtering package using the signal filtering package

Whoson Visualizer

• Visualized more than 1,000 students logged into Swarthmore College Computer Science Department computers
• Designed a search box to search users on department computers throughout campus
• Built the backend using Python, developed the frontend with Semantic UI and arborjs

TriCo Course Scheduler Project

• Spearheaded the project that would help over 4,000 students schedule their courses out of over 10,000 courses
• Built the backend for the project using Python, developed the frontend with Bootstrap, Fuze.js, and DHTMLX
• Helped more than 1,000 Swarthmore College, Bryn Mawr College, and Haverford College students schedule their courses