混成系统验证

dL/KeYmaera

  1. CADE
    KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems Fulton, Nathan, Mitsch, Stefan, Quesel, Jan-David, Völp, Marcus, and Platzer, André In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 2015
  2. ITP
    Bellerophon: Tactical Theorem Proving for Hybrid Systems Fulton, Nathan, Mitsch, Stefan, Bohrer, Brandon, and Platzer, André In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brası́lia, Brazil, September 26-29, 2017, Proceedings 2017
  3. PLDI
    VeriPhy: verified controller executables from verified cyber-physical system models Bohrer, Brandon, Tan, Yong Kiam, Mitsch, Stefan, Myreen, Magnus O., and Platzer, André In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018 2018

HCSP/HHL

  1. ICFEM
    An Improved HHL Prover: An Interactive Theorem Prover for Hybrid Systems Wang, Shuling, Zhan, Naijun, and Zou, Liang In Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings 2015