model-pitfalls-dL v1.0.0

Supplementary hybrid programs and KeYmaeara X proofs for the paper titled 'On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic' by Yuvaraj Selvaraj, Jonas Krook, Wolfgang Ahrendt, and Martin Fabian.

The GitHub repository contains examples of faulty models, proofs for the theorems to identify such faulty models, and the correct models where the faults have been rectified.

The paper has been accepted for publication in LNCS series as part of ICFEM 2022 proceedings.