14 citations · 31 across the 17 of their papers we have counts for
20 papers
Proof Interfaces for Exploratory Mathematics
Nishant Kheterpal, Matthew Keenan, Cyrus Omar +1
This paper describes a mathematics interface intended for both educational applications and exploratory mathematics. Both learners and mathematics practitioners often use pen and p…
Hazel Prover: A Classroom Proof Assistant for Learning Structural Induction
Matthew Keenan, Nishant Kheterpal, Jean-Baptiste Jeannin +1
Proof assistants offer instant feedback and incremental proof scaffolding to users. Both of these features have long held promise in improving mathematics education in classroom se…
Towards Formal Verification of Hybrid Synchronous Programs with Refinement Types
Serra Z. Dane, Jiawei Chen, Marc Pouzet +1
Cyber-physical systems (CPS) such as autonomous cars, aircraft, and robots are often also safety-critical; thus it is imperative that they operate as intended with a high degree of…
Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
Yichen Tao, Hongfei Fu, Jiawei Chen +1
Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potential…
Synchronous Programming with Refinement Types
Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Shimels Ayele +6
Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the saf…
Security Verification of Low-Trust Architectures
Qinhan Tan, Yonathan Fisseha, Shibo Chen +4
Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave compo…
Falsification of a Vision-based Automatic Landing System
Sara Shoouri, Shayan Jalili, Jiahong Xu +5
At smaller airports without an instrument approach or advanced equipment, automatic landing of aircraft is a safety-critical task that requires the use of sensors present on the ai…
Efficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes
Liren Yang, Hang Zhang, Jean-Baptiste Jeannin +1
Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorit…
Automating Geometric Proofs of Collision Avoidance with Active Corners
Nishant Kheterpal, Elanor Tang, Jean-Baptiste Jeannin
Avoiding collisions between obstacles and vehicles such as cars, robots or aircraft is essential to the development of automation and autonomy. To simplify the problem, many collis…
A Concurrent Switching Model for Traffic Congestion Control
Hossein Rastgoftar, Xun Liu, Jean-Baptiste Jeannin
We introduce a new conservation-based approach for traffic coordination modeling and control in a network of interconnected roads (NOIR) with switching movement phase rotations at…
Formally verified asymptotic consensus in robust networks
Mohit Tekriwal, Avi Tachna-Fram, Jean-Baptiste Jeannin +2
Distributed architectures are used to improve performance and reliability of various systems. Examples include drone swarms and load-balancing servers. An important capability of a…
Formalization of Asymptotic Convergence for Stationary Iterative Methods
Mohit Tekriwal, Joshua Miller, Jean-Baptiste Jeannin
Solutions to differential equations, which are used to model physical systems, are computed numerically by solving a set of discretized equations. This set of discretized equations…
Dandelion: Certified Approximations of Elementary Functions
Heiko Becker, Mohit Tekriwal, Eva Darulova +2
Elementary function operations such as sin and exp cannot in general be computed exactly on today's digital computers, and thus have to be approximated. The standard approximations…
A formal proof of the Lax equivalence theorem for finite difference schemes
Mohit Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin
The behavior of physical systems is typically modeled using differential equations which are too complex to solve analytically. In practical problems, these equations are discretiz…
A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems: Extended Technical Report
Hammad Ahmad, Jean-Baptiste Jeannin
Signal temporal logic (STL) was introduced for monitoring temporal properties of continuous-time signals for continuous and hybrid systems. Differential dynamic logic (dL) was intr…
A Physics-Based Finite-State Abstraction for Traffic Congestion Control
Hossein Rastgoftar, Jean-Baptiste Jeannin
This paper offers a finite-state abstraction of traffic coordination and congestion in a network of interconnected roads (NOIR). By applying mass conservation, we model traffic coo…
Grand Challenges for Embedded Security Research in a Connected World
Wayne Burleson, Kevin Fu, Denise Anthony +7
Protecting embedded security is becoming an increasingly challenging research problem for embedded systems due to a number of emerging trends in hardware, software, networks, and a…
Formal Specification of Continuum Deformation Coordination
Hossein Rastgoftar, Jean-Baptiste Jeannin, Ella Atkins
Continuum deformation is a leader-follower multiagent cooperative control approach. Previous work showed a desired continuum deformation can be uniquely defined based on trajectori…
Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions
Kyle D. Julian, Shivam Sharma, Jean-Baptiste Jeannin +1
The next generation of aircraft collision avoidance systems frame the problem as a Markov decision process and use dynamic programming to optimize the alerting logic. The resulting…
Type Inference for Static Compilation of JavaScript (Extended Version)
Satish Chandra, Colin S. Gordon, Jean-Baptiste Jeannin +4
We present a type system and inference algorithm for a rich subset of JavaScript equipped with objects, structural subtyping, prototype inheritance, and first-class methods. The ty…