7 citations · 17 across the 16 of their papers we have counts for
19 papers
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…