VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models
We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end as it bridges abstraction gaps, including: i) the gap between mathematical reals in physical models and machine arithmetic in the implementation, ii) the gap between real physics and its differential-equation models, and iii) the gap between nondeterministic controller models and machine code. VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle/HOL. To minimize the trusted base, we cross-verify KeYmaeraX in Isabelle/HOL. We evaluate the resulting controller and monitors on commodity robotics hardware.
Fri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:40 | VerificationPLDI Research Papers at Grand Ballroom AB Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA | ||
14:00 25mTalk | VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models PLDI Research Papers Brandon Bohrer , Yong Kiam Tan Carnegie Mellon University, USA, Stefan Mitsch Carnegie Mellon University, USA, Magnus O. Myreen Chalmers University of Technology, Sweden, André Platzer Carnegie Mellon University Media Attached | ||
14:25 25mTalk | Crellvm: Verified Credible Compilation for LLVM PLDI Research Papers Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Youngju Song Seoul National University, Juneyoung Lee Seoul National University, Sanghoon Park Seoul National University, South Korea, Mark Dongyeon Shin Seoul National University, South Korea, Yonghyun Kim Seoul National University, South Korea, Sungkeun Cho Seoul National University, South Korea, Joonwon Choi Massachusetts Institute of Technology, USA, Chung-Kil Hur Seoul National University, Kwangkeun Yi Seoul National University Media Attached | ||
14:50 25mTalk | Certified Concurrent Abstraction Layers PLDI Research Papers Ronghui Gu Columbia University, Zhong Shao Yale University, Jieung Kim Yale University, USA, Xiongnan (Newman) Wu Yale University, Jérémie Koenig , Vilhelm Sjöberg Yale University, Hao Chen Yale University, David Costanzo Yale University, Tahina Ramananandro Microsoft Research, n.n. Media Attached | ||
15:15 25mTalk | Modularity for Decidability of Deductive Verification with Applications to Distributed Systems PLDI Research Papers Marcelo Taube Tel Aviv University, Israel, Giuliano Losa University of California at Los Angeles, USA, Kenneth L. McMillan Microsoft Research, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university, James R. Wilcox University of Washington, Doug Woos University of Washington Media Attached | ||