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 Jun
14:00 - 15:40: PLDI Research Papers - Verification at Grand Ballroom AB Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA | ||||||||||||||||||||||||||||||||||||||||||
| 14:00 - 14:25 Talk | Brandon Bohrer, Yong Kiam TanCarnegie Mellon University, USA, Stefan MitschCarnegie Mellon University, USA, Magnus O. MyreenChalmers University of Technology, Sweden, André PlatzerCarnegie Mellon University Media Attached | |||||||||||||||||||||||||||||||||||||||||
| 14:25 - 14:50 Talk | Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Youngju SongSeoul National University, Juneyoung LeeSeoul National University, Sanghoon ParkSeoul National University, South Korea, Mark Dongyeon ShinSeoul National University, South Korea, Yonghyun KimSeoul National University, South Korea, Sungkeun ChoSeoul National University, South Korea, Joonwon ChoiMassachusetts Institute of Technology, USA, Chung-Kil HurSeoul National University, Kwangkeun YiSeoul National University Media Attached | |||||||||||||||||||||||||||||||||||||||||
| 14:50 - 15:15 Talk | Ronghui GuColumbia University, Zhong ShaoYale University, Jieung KimYale University, USA, Xiongnan (Newman) WuYale University, Jérémie Koenig, Vilhelm SjobergYale University, Hao ChenYale University, David CostanzoYale University, Tahina RamananandroMicrosoft Research, n.n. Media Attached | |||||||||||||||||||||||||||||||||||||||||
| 15:15 - 15:40 Talk | Marcelo TaubeTel Aviv University, Israel, Giuliano LosaUniversity of California at Los Angeles, USA, Kenneth L. McMillanMicrosoft Research, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington Media Attached | |||||||||||||||||||||||||||||||||||||||||