## SSS Abstracts |

We introduce component-driven proof automation, an approach to overcome these problems for CPSs built from small libraries of reusable components. First, an end-user builds a high-level component-based design in a graphical design tool, then automation exploits the component structure of the high-level model to derive a formal safety specification and proof in dL. Formal methods expertise is only required once, in the implementation of the specification generator and automated prover: the resulting design and verification toolchain can be used with no formal methods knowledge. Example applications include flight plans for unmanned drones as well as road and rail network designs.

We present the CoasterX toolchain for design and verification of roller coaster track designs as a case study in component-driven proof automation. Roller coasters are a safety-critical class of trains, characterized by gravity propulsion and closed-loop tracks with complex changes in track grade. We show how the velocity and acceleration bounds proved by CoasterX can (a) assure compliance with international safety standards and (b) explain safety violations and their resolution in real coasters, such as the Steel Phantom and its successor Phantom's Revenge, both at the Kennywood Amusement Park in Pittsburgh. We significantly advance the scalability of dL verification according to multiple metrics, achieving near order-of-magnitude improvement in the numbers of variables and component instances verified.

In Partial Fulfillment of the Speaking Requirement

Joint work with Dr. Euiwoong Lee. Ms. Dhivya Eswaran, and Prof. Ariel D. Procaccia

In Partial Fulfillment of the Speaking Requirement

In Partial Fulfillment of the Speaking Requirement

In Partial Fulfillment of the Speaking Requirement

We will describe Cartesian cubical type theory, a novel dependent type theory that supports higher inductive types and univalence while restoring the connection between proofs and programs. We will also demonstrate how univalence can simplify ordinary type-theoretic reasoning in the RedPRL proof assistant currently under development at CMU.

Joint work with Kuen-Bang Hou (Favonia) and Robert Harper

In Partial Fulfillment of the Speaking Requirement

In Partial Fulfillment of the Speaking Requirement

In Partial Fulfillment of the Speaking Requirement

In Partial Fulfillment of the Speaking Requirement

In the second part, I will discuss two models for multisource domain adaptations: the first model optimizes the worst-case bound, while the second model is a smoothed approximation of the first one and optimizes a task-adaptive bound. We also demonstrate the effectiveness of both models by conducting extensive experiments showing superior adaptation performance on a real-world application: vehicle counting.

Joint work with Shanghang Zhang, Guanhang Wu, Joao Costeira, Jose Moura and Geoff Gordon

In Partial Fulfillment of the Speaking Requirement

Further applications of synchronization strings will also be briefly discussed including a general method of simulating symbol corruption channels over any given insertion-deletion channel, an efficient and near-optimal coding scheme for interactive communication over insertion-deletion channels, and list-decodable insertion-deletion codes.

This talk is based on a joint work with Bernhard Haeupler.

In Partial Fulfillment of the Speaking Requirement