Publications

    Jump to Year:
    202520242023202220212020201920182017201620152014201320122011201020092008200720062004

    2025

    1. Julia Butte André Platzer
      Semi-competitive differential game logic
      Automated reasoning with analytic tableaux and related methods - 33rd international conference, TABLEAUX 2025, reykjavík, iceland, september 29 – october 3, 2025, proceedings
      Copy BibTex⧉
    2. Enguerrand Prebet Samuel Teuber André Platzer
      Verification of autonomous neural car control with KeYmaera X
      Rigorous state-based methods - 11th international conference, ABZ 2025, düsseldorf, germany, june 10-13, 2025, proceedings
      Copy BibTex⧉

    2024

    1. CESAR: Control envelope synthesis via angelic refinements
      TACAS
      Copy BibTex⧉   Slides
    2. Noah Abou El Wafa André Platzer
      Complete game logic with sabotage
      LICS
      Copy BibTex⧉
    3. Enguerrand Prebet André Platzer
      Uniform substitution for differential refinement logic
      IJCAR
      Copy BibTex⧉

    2023

    1. Katherine Kosaian Yong Kiam Tan André Platzer
      A first complete algorithm for real quantifier elimination in Isabelle/HOL
      Proceedings of the 12th ACM SIGPLAN international conference on certified programs and proofs
      Copy BibTex⧉
    2. William Simmons André Platzer
      Differential elimination and algebraic invariants of polynomial dynamical systems
      Copy BibTex⧉
    3. Rachel Cleaveland Stefan Mitsch André Platzer
      Formally verified next-generation airborne collision avoidance games in ACAS X
      Copy BibTex⧉
    4. Katherine Kosaian
      Formally verifying algorithms for real quantifier elimination
      Ph.D. dissertation
      Copy BibTex⧉   PDF
    5. Refinements of hybrid dynamical systems logic
      Rigorous state-based methods - 9th international conference, ABZ 2023, nancy, france, proceedings
      Copy BibTex⧉   Slides
    6. Uniform substitution for dynamic logic with communicating hybrid programs
      CADE
      Copy BibTex⧉   Slides

    2022

    1. Deductive verification for ordinary differential equations: Safety, liveness, and stability
      Ph.D. dissertation
      Copy BibTex⧉   PDF
    2. Noah Abou El Wafa André Platzer
      First-order game logic and modal mu-calculus
      Copy BibTex⧉
    3. Weihan Li
      Formal verification of the winning strategies of pursuit-evasion games
      Copy BibTex⧉   PDF
    4. Implicit definitions with differential equations for KeYmaera X - (system description)
      IJCAR
      Copy BibTex⧉   Slides
    5. Learning to find proofs and theorems by learning to refine search strategies
      Advances in neural information processing systems
      Copy BibTex⧉   Slides
    6. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: Sound continuous invariant generation
      Copy BibTex⧉   PDF
    7. Qin Lin Stefan Mitsch André Platzer John M. Dolan
      Safe and resilient practical waypoint-following for autonomous vehicles
      Copy BibTex⧉   PDF
    8. Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces
      Copy BibTex⧉   Slides
    9. Verifying switched system stability with logic
      HSCC ’22: 25th ACM international conference on hybrid systems: Computation and control, milan, italy, may 4 - 6, 2022
      Copy BibTex⧉   Slides

    2021

    1. Katherine Cordwell Yong Kiam Tan André Platzer
      A verified decision procedure for univariate real arithmetic with the BKR algorithm
      12th international conference on interactive theorem proving, ITP 2021, june 29 to july 1, 2021, rome, italy
      Copy BibTex⧉   PDF   Slides
    2. An axiomatic approach to existence and liveness for differential equations
      Copy BibTex⧉   PDF
    3. Deductive stability proofs for ordinary differential equations
      Tools and algorithms for the construction and analysis of systems - 27th international conference, TACAS 2021, held as part of the european joint conferences on theory and practice of software, ETAPS 2021, proceedings, part II
      Copy BibTex⧉   PDF   Slides
    4. Rachel Cleaveland
      Formal verification of next-generation airborne collision avoidance system with adversarial intruder behavior
      Copy BibTex⧉   PDF   Slides
    5. Rose Bohrer
      Practical end-to-end verification of cyber-physical systems
      Ph.D. dissertation
      Copy BibTex⧉   PDF   Slides
    6. Runtime verification of generalized test tables
      NASA formal methods - 13th international symposium, NFM 2021, virtual event, may 24-28, 2021, proceedings
      Copy BibTex⧉
    7. Brandon Bohrer André Platzer
      Structured proofs for adversarial cyber-physical systems
      Copy BibTex⧉   PDF
    8. Switched systems as hybrid programs
      7th IFAC conference on analysis and design of hybrid systems, ADHS 2021, brussels, belgium, july 7-9, 2021
      Copy BibTex⧉
    9. The 28th international conference on automated deduction
      Springer. in , Springer
      Copy BibTex⧉
    10. Matias Scharager Katherine Cordwell Stefan Mitsch André Platzer
      Verified quadratic virtual substitution for real arithmetic
      FM
      Copy BibTex⧉   PDF   Slides

    2020

    1. A retrospective on developing hybrid systems provers in the KeYmaera family - A tale of three provers
      Copy BibTex⧉   PDF
    2. Brandon Bohrer André Platzer
      Constructive game logic
      Programming languages and systems - 29th european symposium on programming, ESOP 2020, held as part of the european joint conferences on theory and practice of software, ETAPS 2020, dublin, ireland, april 25-30, 2020, proceedings
      Copy BibTex⧉   PDF   Slides
    3. Brandon Bohrer André Platzer
      Constructive hybrid games
      IJCAR
      Copy BibTex⧉   PDF   Slides
    4. Differential equation invariance axiomatization
      Copy BibTex⧉   PDF   Slides
    5. Modular Regression verification for reactive systems
      Leveraging applications of formal methods, verification and validation: Engineering principles - 9th international symposium on leveraging applications of formal methods, ISoLA 2020, rhodes, greece, october 20-30, 2020, proceedings, part II
      Copy BibTex⧉
    6. Brandon Bohrer André Platzer
      Refining constructive hybrid games
      5th international conference on formal structures for computation and deduction, FSCD 2020, june 29 - july 5, 2020, paris, france
      Copy BibTex⧉   PDF   Slides
    7. Relational test tables: A practical specification language for evolution and security
      FormaliSE@ICSE 2020: 8th international conference on formal methods in software engineering, seoul, republic of korea, july 13, 2020
      Copy BibTex⧉
    8. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      Relational test tables: A practical specification language for evolution and security
      Copy BibTex⧉
    9. The KeY Approach on Hagrid
      VerifyThis long-term challenge: proceedings
      Copy BibTex⧉
    10. The PGP Key Server: Challenge Manual
      VerifyThis long-term challenge: proceedings
      Copy BibTex⧉
    11. The VerifyThis Collaborative Long Term Challenge
      Copy BibTex⧉
    12. VerifyThis long-term challenge: proceedings
      in , Karlsruhe
      Copy BibTex⧉

    2019

    1. 17th IEEE international conference on industrial informatics, INDIN 2019, helsinki, finland, july 22-25, 2019
      IEEE. in , IEEE
      Copy BibTex⧉
    2. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Andrew Sogokon André Platzer
      A formal safety net for waypoint following in ground robots
      Copy BibTex⧉
    3. An axiomatic approach to liveness for differential equations
      FM
      Copy BibTex⧉   PDF   Slides
    4. Differential equation invariance axiomatization
      Copy BibTex⧉ Preprint
    5. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      CADE
      Copy BibTex⧉   PDF   Slides
    6. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      Copy BibTex⧉   PDF
    7. João Martins André Platzer João Leite
      Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems
      TABLEAUX
      Copy BibTex⧉   PDF   Slides
    8. Formal verification of evolutionary changes
      Copy BibTex⧉
    9. HyPLC: Hybrid programmable logic controller program translation for verification
      ICCPS
      Copy BibTex⧉   PDF
    10. KASTEL industry 4.0 demonstrator: Provably forgetting information in PLC software
      Copy BibTex⧉
    11. KeYmaera X tutorial
      Copy BibTex⧉   PDF
    12. On the preservation of the trust by regression verification of PLC software for cyber-physical systems of systems
      17th IEEE international conference on industrial informatics, INDIN 2019, helsinki, finland, july 22-25, 2019
      Copy BibTex⧉
    13. Overview of logical foundations of cyber-physical systems
      Copy BibTex⧉ Preprint
    14. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: A framework for sound continuous invariant generation
      FM
      Copy BibTex⧉   PDF   Slides
    15. Provably forgetting of information in manufacturing systems: Verification of the KASTEL industry demonstrator
      Copy BibTex⧉
    16. Relational test tables: A practical specification language for evolution and security
      Copy BibTex⧉ Preprint
    17. The logical path to autonomous cyber-physical systems
      QEST
      Copy BibTex⧉   PDF   Slides
    18. Katherine Cordwell André Platzer
      Towards physical hybrid systems
      CADE
      Copy BibTex⧉   PDF   Slides
    19. Uniform substitution at one fell swoop
      CADE
      Copy BibTex⧉   PDF   Slides
    20. Uniform substitution at one fell swoop
      Copy BibTex⧉
    21. Nathan Fulton André Platzer
      Verifiably safe off-model reinforcement learning
      TACAS
      Copy BibTex⧉   PDF

    2018

    1. Andreas Müller Stefan Mitsch Wieland Schwinger André Platzer
      A component-based hybrid systems verification and implementation tool in KeYmaera X (tool demonstration)
      Cyber physical systems. Model-based design - 8th international workshop, CyPhy 2018, and 14th international workshop, WESE 2018, turin, italy, october 4-5, 2018, revised selected papers
      Copy BibTex⧉   PDF
    2. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      LICS
      Copy BibTex⧉   PDF   Slides
    3. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      Copy BibTex⧉   PDF
    4. Achieving delta description of the control software for an automated production system evolution
      14th IEEE international conference on automation science and engineering, CASE 2018, munich, germany, august 20-24, 2018
      Copy BibTex⧉
    5. Sarah Grebing An Thuy Tien Luong Alexander Weigl
      Adding text-based interaction to a direct-manipulation interface for program verification – lessons learned
      13th international workshop on user interfaces for theorem provers (UITP 2018)
      Copy BibTex⧉
    6. Applicability of generalized test tables: A case study using the manufacturing system demonstrator xPPU
      Copy BibTex⧉
    7. Brandon Bohrer Adriel Luo Xue An Chuang André Platzer
      CoasterX: A case study in component-driven hybrid systems proof automation
      6th IFAC conference on analysis and design of hybrid systems, ADHS 2018, oxford, UK, july 11-13, 2018
      Copy BibTex⧉   PDF   Slides
    8. Debugging program verification proof scripts (tool paper)
      Copy BibTex⧉ Preprint
    9. Differential equation axiomatization: The impressive power of differential ghosts
      LICS
      Copy BibTex⧉   PDF   Slides
    10. Logical foundations of cyber-physical systems
      Springer. in , Springer Cham
      Copy BibTex⧉   Slides
    11. Proceedings third workshop on models for formal analysis of real systems and sixth international workshop on verification and program transformation, MARS/VPT@ETAPS 2018, thessaloniki, greece, 20th april 2018
      in ,
      Copy BibTex⧉
    12. Proving equivalence between imperative and MapReduce implementations using program transformations
      Proceedings third workshop on models for formal analysis of real systems and sixth international workshop on verification and program transformation, MARS/VPT@ETAPS 2018, thessaloniki, greece, 20th april 2018
      Copy BibTex⧉
    13. Relational equivalence proofs between imperative and MapReduce algorithms
      Verified software. Theories, tools, and experiments - 10th international conference, VSTTE 2018, oxford, UK, july 18-19, 2018, revised selected papers
      Copy BibTex⧉
    14. Relational equivalence proofs between imperative and MapReduce algorithms
      Copy BibTex⧉ Preprint
    15. Nathan Fulton André Platzer
      Safe AI for CPS
      IEEE international test conference, ITC 2018, phoenix, AZ, USA, october 29 - nov. 1, 2018
      Copy BibTex⧉   PDF   Slides
    16. Nathan Fulton André Platzer
      Safe reinforcement learning via formal methods: Toward safe control through proof and learning
      Proceedings of the thirty-second AAAI conference on artificial intelligence, february 2-7, 2018, new orleans, louisiana, USA.
      Copy BibTex⧉   PDF   Slides Preprint
    17. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Tactical contract composition for hybrid system component verification
      Copy BibTex⧉   PDF
    18. Uniform substitution for differential game logic
      IJCAR
      Copy BibTex⧉   PDF   Slides
    19. Andrew Sogokon Khalil Ghorbal Yong Kiam Tan André Platzer
      Vector barrier certificates and comparison systems
      FM
      Copy BibTex⧉   PDF   Slides
    20. Nathan Fulton
      Verifiably safe autonomy for cyber-physical systems
      Ph.D. dissertation
      Copy BibTex⧉   PDF
    21. Laurent Doyen Goran Frehse George J. Pappas André Platzer
      Verification of hybrid systems
      Copy BibTex⧉   PDF
    22. Verified runtime validation for partially observable hybrid systems
      Copy BibTex⧉
    23. Verified software. Theories, tools, and experiments - 10th international conference, VSTTE 2018, oxford, UK, july 18-19, 2018, revised selected papers
      Springer. in , Springer
      Copy BibTex⧉
    24. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Magnus O. Myreen André Platzer
      VeriPhy: Verified controller executables from verified cyber-physical system models
      PLDI
      Copy BibTex⧉   PDF   Slides
    25. Videos for logical foundations of cyber-physical systems
      Copy BibTex⧉

    2017

    1. 15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      IEEE. in , IEEE
      Copy BibTex⧉
    2. A complete uniform substitution calculus for differential dynamic logic
      Copy BibTex⧉   PDF
    3. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Aurora Schmidt Ryan Gardner Stefan Mitsch André Platzer
      A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system
      Copy BibTex⧉   PDF
    4. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
      Copy BibTex⧉   PDF
    5. Nathan Fulton Stefan Mitsch Brandon Bohrer André Platzer
      Bellerophon: Tactical theorem proving for hybrid systems
      ITP
      Copy BibTex⧉   PDF   Slides
    6. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Change and delay contracts for hybrid system component verification
      FASE
      Copy BibTex⧉   PDF   Slides
    7. Differential hybrid games
      Copy BibTex⧉   PDF
    8. Stefan Mitsch Khalil Ghorbal David Vogelbacher André Platzer
      Formal verification of obstacle avoidance and navigation of ground robots
      Copy BibTex⧉   PDF
    9. Stefan Mitsch Marco Gario Christof J. Budnik Michael Golm André Platzer
      Formal verification of train control with air pressure brakes
      RSSRail
      Copy BibTex⧉   PDF   Slides
    10. Brandon Bohrer Vincent Rahli Ivana Vukotic Marcus Völp André Platzer
      Formally verified differential dynamic logic
      Certified programs and proofs - 6th ACM SIGPLAN conference, CPP 2017, paris, france, january 16-17, 2017
      Copy BibTex⧉   PDF   Slides
    11. Foundations of cyber-physical systems
      Copy BibTex⧉
    12. Generalised test tables: A practical specification language for reactive systems
      Integrated formal methods - 13th international conference, IFM 2017, turin, italy, september 20-22, 2017, proceedings
      Copy BibTex⧉
    13. Generalized test tables: A powerful and intuitive specification language for reactive systems
      15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      Copy BibTex⧉
    14. Generation of monitoring functions in production automation using test specifications
      15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      Copy BibTex⧉
    15. Franz Franchetti Tze Meng Low Stefan Mitsch Juan Paolo Mendoza Liangyan Gui Amarin Phaosawasdi David Padua Soummya Kar José M. F. Moura Mike Franusich Jeremy Johnson André Platzer Manuela Veloso
      High-assurance SPIRAL: End-to-end guarantees for robot and car control
      Copy BibTex⧉   PDF
    16. How to prove ‘all’ differential equation properties
      Copy BibTex⧉   PDF

    2016

    1. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      IFM
      Copy BibTex⧉   PDF   Slides
    2. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      Copy BibTex⧉   PDF
    3. Nathan Fulton André Platzer
      A logic of proofs for differential dynamic logic: Toward independently checkable proof certificates for dynamic logics
      Proceedings of the 2016 conference on certified programs and proofs, CPP 2016, st. Petersburg, FL, USA, january 18-19, 2016
      Copy BibTex⧉   PDF   Slides
    4. Andrew Sogokon Khalil Ghorbal Paul B. Jackson André Platzer
      A method for invariant generation for polynomial continuous systems
      VMCAI
      Copy BibTex⧉   PDF   Slides
    5. A verification-supported evolution approach to assist software application engineers in industrial factory automation
      IEEE international symposium on assembly and manufacturing (ISAM 2016)
      ABSTRACT Copy BibTex⧉
    6. Sarah M. Loos André Platzer
      Differential refinement logic
      LICS
      Copy BibTex⧉   PDF   Slides
    7. Sarah M. Loos
      Differential refinement logic
      Ph.D. dissertation
      Copy BibTex⧉   PDF   Slides
    8. Efficient SAT-based pre-image enumeration for quantitative information flow in programs
      Data privacy management and security assurance - 11th international workshop, DPM 2016 and 5th international workshop, QASA 2016, heraklion, crete, greece, september 26-27, 2016, proceedings
      Copy BibTex⧉
    9. Foundations of cyber-physical systems
      Copy BibTex⧉   PDF
    10. Foundations of cyber-physical systems
      Copy BibTex⧉   Slides
    11. Jan-David Quesel Stefan Mitsch Sarah Loos Nikos Aréchiga André Platzer
      How to model and prove hybrid systems with KeYmaera: A tutorial on safety
      Copy BibTex⧉   PDF
    12. Logic & proofs for cyber-physical systems
      IJCAR
      ABSTRACT Copy BibTex⧉   PDF   Slides
    13. ModelPlex: Verified runtime validation of verified cyber-physical system models
      Copy BibTex⧉   PDF
    14. Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      in ,
      Copy BibTex⧉
    15. Sound probabilistic #SAT with projection
      Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      Copy BibTex⧉
    16. The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving
      3rd workshop on formal integrated development environment
      Copy BibTex⧉   PDF

    2015

    1. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Ryan Gardner Aurora Schmidt Erik Zawadzki André Platzer
      A formally verified hybrid system for the next-generation airborne collision avoidance system
      TACAS
      Copy BibTex⧉   PDF
    2. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking differential invariance of algebraic sets
      VMCAI
      Copy BibTex⧉   PDF   Slides
    3. A uniform substitution calculus for differential dynamic logic
      CADE
      Copy BibTex⧉   PDF   Slides Preprint
    4. Correct system design symposium in honor of ernst-rüdiger olderog on the occasion of his 60th birthday oldenburg, germany, september 8-9, 2015 proceedings
      Springer. in , Springer
      Copy BibTex⧉
    5. Differential game logic
      Copy BibTex⧉   PDF
    6. Annika Peterson
      Formal verification of a controlled flight between two robots: A case study
      Copy BibTex⧉   PDF
    7. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Ryan Gardner Aurora Schmidt Erik Zawadzki André Platzer
      Formal verification of ACAS X, an industrial airborne collision avoidance system
      EMSOFT
      Copy BibTex⧉   PDF
    8. Nikos Arechiga James Kapinski Jyotirmoy V. Deshmukh André Platzer Bruce H. Krogh
      Forward invariant cuts to simplify proofs of safety
      EMSOFT
      Copy BibTex⧉
    9. How to prove hybrid systems and why that matters
      ICCSE
      Copy BibTex⧉   PDF
    10. Nathan Fulton Stefan Mitsch Jan-David Quesel Marcus Völp André Platzer
      KeYmaera X: An axiomatic tactical theorem prover for hybrid systems
      CADE
      Copy BibTex⧉   PDF   Slides
    11. Stefan Mitsch André Platzer Werner Retschitzegger Wieland Schwinger
      Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems
      Copy BibTex⧉   PDF
    12. Proving equivalence between control software variants for Programmable Logic Controllers: Using Regression Verification to Reduce Unneeded Variant Diversity
      IEEE international conference on emerging technologies and factory automation, ETFA
      ABSTRACT Copy BibTex⧉
    13. Regression verification for programmable logic controller software
      Copy BibTex⧉
    14. Regression verification for programmable logic controller software
      Formal methods and software engineering - 17th international conference on formal engineering methods, ICFEM 2015, paris, france, november 3-5, 2015, proceedings
      Copy BibTex⧉
    15. Regression verification for programmable logic controller software
      Thesis
      Copy BibTex⧉
    16. Verified traffic networks: Component-based verification of cyber-physical flow systems
      ITSC
      Copy BibTex⧉   PDF   Slides

    2014

    1. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Ryan Garnder Aurora Schmidt Erik Zawadzki André Platzer
      A formally verified hybrid system for the next-generation airborne collision avoidance system
      Copy BibTex⧉   PDF
    2. Analog and hybrid computation: Dynamical systems and programming languages
      Copy BibTex⧉   PDF Preprint
    3. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      TACAS
      Copy BibTex⧉   PDF   Slides
    4. Stefan Mitsch Grant Olney Passmore André Platzer
      Collaborative verification-driven engineering of hybrid systems
      Copy BibTex⧉   PDF
    5. Differential hybrid games
      Copy BibTex⧉   PDF
    6. Jean-Baptiste Jeannin André Platzer
      dTL^2: Differential temporal dynamic logic with nested temporalities for hybrid systems
      IJCAR
      Copy BibTex⧉   PDF   Slides
    7. Foundations of cyber-physical systems
      Copy BibTex⧉   PDF
    8. Stefan Mitsch Jan-David Quesel André Platzer
      From safety to guilty & from liveness to niceness
      5th workshop on formal methods for robotics and automation
      Copy BibTex⧉   PDF
    9. Khalil Ghorbal Jean-Baptiste Jeannin Erik P. Zawadzki André Platzer Geoffrey J. Gordon Peter Capell
      Hybrid theorem proving of aerospace systems: Applications and challenges
      Copy BibTex⧉   PDF
    10. Khalil Ghorbal Andrew Sogokon André Platzer
      Invariance of conjunctions of polynomial equalities for algebraic differential equations
      SAS
      Copy BibTex⧉   PDF   Slides
    11. ModelPlex: Verified runtime validation of verified cyber-physical system models
      RV
      Copy BibTex⧉   PDF   Slides
    12. ModelPlex: Verified runtime validation of verified cyber-physical system models
      Copy BibTex⧉   PDF
    13. Stefan Mitsch Jan-David Quesel André Platzer
      Refactoring, refinement, and reasoning: A logical characterization for hybrid systems
      FM
      Copy BibTex⧉   PDF   Slides
    14. Akshay Rajhans Ajinkya Bhave Ivan Ruchkin Bruce H. Krogh David Garlan André Platzer Bradley Schmerl
      Supporting heterogeneity in cyber-physical systems architectures
      Copy BibTex⧉
    15. Sarah M. Loos André Platzer
      Teaching cyber-physical systems with logic
      Copy BibTex⧉   PDF

    2013

    1. A complete axiomatization for differential game logic for hybrid games
      Copy BibTex⧉   PDF   Slides
    2. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      IJCAI
      Copy BibTex⧉   PDF Preprint
    3. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      Copy BibTex⧉   PDF
    4. Erik P. Zawadzki Geoffrey J. Gordon André Platzer
      A projection algorithm for strictly monotone linear complementarity problems
      6th NIPS workshop on optimization for machine learning
      Copy BibTex⧉   PDF Preprint
    5. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      ABSTRACT Copy BibTex⧉   PDF
    6. Yanni Kouskoulas David W. Renshaw André Platzer Peter Kazanzides
      Certifying the safe design of a virtual fixture control algorithm for a surgical robot
      Hybrid systems: Computation and control (part of CPS week 2013), HSCC’13, philadelphia, PA, USA, april 8-13, 2013
      Copy BibTex⧉   PDF   Slides
    7. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      Copy BibTex⧉   PDF
    8. Sarah M. Loos David Witmer Peter Steenkiste André Platzer
      Efficiency analysis of formally verified adaptive cruise controllers
      ITSC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    9. Yanni Kouskoulas André Platzer Peter Kazanzides
      Formal methods for robotic system control software
      Copy BibTex⧉   PDF Preprint
    10. Sarah M. Loos David W. Renshaw André Platzer
      Formal verification of distributed aircraft controllers
      Hybrid systems: Computation and control (part of CPS week 2013), HSCC’13, philadelphia, PA, USA, april 8-13, 2013
      Copy BibTex⧉   PDF   Slides
    11. Foundations of cyber-physical systems
      Copy BibTex⧉   PDF
    12. On provably safe obstacle avoidance for autonomous robotic ground vehicles
      Robotics: Science and systems
      Copy BibTex⧉   PDF   Slides
    13. Teaching CPS foundations with contracts
      CPS-ed
      Copy BibTex⧉   PDF   Slides Preprint

    2012

    1. A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems
      Copy BibTex⧉   PDF
    2. A differential operator approach to equational differential invariants
      ITP
      ABSTRACT Copy BibTex⧉   PDF   Slides
    3. Algorithms for Forbidden Pattern Recognition in Transition Diagrams
      Thesis
      Copy BibTex⧉
    4. Differential game logic for hybrid games
      Copy BibTex⧉   PDF
    5. Dynamic logics of dynamical systems
      Copy BibTex⧉
    6. Logical analysis of hybrid systems: A complete answer to a complexity challenge
      DCFS
      Copy BibTex⧉   PDF
    7. Logical analysis of hybrid systems: A complete answer to a complexity challenge
      Copy BibTex⧉   PDF
    8. Logics of dynamical systems
      LICS
      ABSTRACT Copy BibTex⧉   PDF   Slides
    9. David W. Renshaw Sarah Loos André Platzer
      Mechanized safety proofs for disc-constrained aircraft
      Copy BibTex⧉   PDF
    10. Jan-David Quesel André Platzer
      Playing hybrid games with KeYmaera
      IJCAR
      Copy BibTex⧉   PDF   Slides
    11. David Henriques João G. Martins Paolo Zuliani André Platzer Edmund M. Clarke
      Statistical model checking for Markov decision processes
      QEST
      ABSTRACT Copy BibTex⧉   PDF   Slides
    12. The complete proof theory of hybrid systems
      LICS
      ABSTRACT Copy BibTex⧉   PDF   Slides
    13. The structure of differential invariants and differential cut elimination
      ABSTRACT Copy BibTex⧉   PDF
    14. Towards formal verification of freeway traffic control
      ICCPS
      Copy BibTex⧉   PDF   Slides
    15. Nikos Aréchiga Sarah M. Loos André Platzer Bruce H. Krogh
      Using theorem provers to guarantee closed-loop system properties
      ACC
      Copy BibTex⧉   PDF

    2011

    1. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      FM
      Copy BibTex⧉   PDF   Slides
    2. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      Copy BibTex⧉   PDF
    3. Erik P. Zawadzki Geoffrey J. Gordon André Platzer
      An instantiation-based theorem prover for first-order programming
      Proceedings of the 14th international conference on artifical intelligence and statistics (AISTATS) 2011, fort lauderdale, FL, USA
      Copy BibTex⧉   PDF Preprint
    4. David W. Renshaw André Platzer
      Differential invariants and symbolic integration for distributed hybrid systems
      Copy BibTex⧉   PDF
    5. David W. Renshaw Sarah M. Loos André Platzer
      Distributed theorem proving for distributed hybrid systems
      ICFEM
      Copy BibTex⧉   PDF
    6. Logic and compositional verification of hybrid systems (invited tutorial)
      CAV
      ABSTRACT Copy BibTex⧉   PDF   Slides
    7. Quantified differential invariants
      HSCC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    8. Sicun Gao André Platzer Edmund M. Clarke
      Quantifier elimination over finite fields with Gröbner bases
      CAI
      Copy BibTex⧉   PDF
    9. Sarah M. Loos André Platzer
      Safe intersections: At the crossing of hybrid systems and verification
      ITSC
      Copy BibTex⧉   PDF   Slides
    10. João Martins André Platzer João Leite
      Statistical model checking for distributed probabilistic-control hybrid automata with smart grid applications
      ICFEM
      Copy BibTex⧉   PDF   Slides
    11. Stochastic differential dynamic logic for stochastic hybrid programs
      CADE
      ABSTRACT Copy BibTex⧉   PDF   Slides
    12. Stochastic differential dynamic logic for stochastic hybrid systems
      Copy BibTex⧉   PDF
    13. The complete proof theory of hybrid systems
      Copy BibTex⧉   PDF
    14. The structure of differential invariants and differential cut elimination
      Copy BibTex⧉   PDF
    15. Akshay Rajhans Ajinkya Bhave Sarah M. Loos Bruce H. Krogh André Platzer David Garlan
      Using parameters in architectural views to support heterogeneous design and verification
      CDC
      Copy BibTex⧉   PDF

    2010

    1. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      HSCC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    2. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification.
      Copy BibTex⧉   PDF
    3. Differential dynamic logics: Automated theorem proving for hybrid systems
      ABSTRACT Copy BibTex⧉
    4. Differential-algebraic dynamic logic for differential-algebraic programs
      ABSTRACT Copy BibTex⧉   PDF
    5. Logical analysis of hybrid systems: Proving theorems for complex dynamics
      Springer. in , Springer Heidelberg
      Copy BibTex⧉
    6. Quantified differential dynamic logic for distributed hybrid systems
      CSL
      ABSTRACT Copy BibTex⧉   PDF   Slides
    7. Quantified differential dynamic logic for distributed hybrid systems
      Copy BibTex⧉   PDF

    2009

    1. Sumit Kumar Jha Edmund Clarke Christopher Langmead Axel Legay André Platzer Paolo Zuliani
      A Bayesian approach to model checking biological systems
      CMSB
      ABSTRACT Copy BibTex⧉   PDF
    2. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT Copy BibTex⧉   PDF
    3. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      ICFEM
      ABSTRACT Copy BibTex⧉   PDF   Slides
    4. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      Thesis
      Copy BibTex⧉   PDF
    5. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      FM
      ABSTRACT Copy BibTex⧉   PDF   Slides
    6. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      Copy BibTex⧉   PDF
    7. Real world verification
      CADE
      ABSTRACT Copy BibTex⧉   PDF   Slides
    8. Real world verification
      Thesis
      Copy BibTex⧉   PDF
    9. Sumit Kumar Jha Edmund Clarke Christopher Langmead Axel Legay André Platzer Paolo Zuliani
      Statistical model checking for complex stochastic models in systems biology
      Copy BibTex⧉   PDF
    10. Verification of cyberphysical transportation systems
      ABSTRACT Copy BibTex⧉

    2008

    1. Edmund M. Clarke Bruce Krogh André Platzer Raj Rajkumar
      Analysis and verification challenges for cyber-physical transportation systems
      NITRD national workshop for research on transportation cyber-physical systems: Automotive, aviation, and rail
      ABSTRACT Copy BibTex⧉   PDF
    2. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      CAV
      ABSTRACT Copy BibTex⧉   PDF   Slides
    3. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      Copy BibTex⧉   PDF
    4. Differential dynamic logic for hybrid systems.
      ABSTRACT Copy BibTex⧉   PDF
    5. Differential dynamic logics: Automated theorem proving for hybrid systems
      Ph.D. dissertation
      Copy BibTex⧉   PDF   Slides
    6. Differential dynamic logics. Automated theorem proving for hybrid systems
      Proceedings des gemeinsamen workshops der graduiertenkollegs 2008, dagstuhl
      Copy BibTex⧉
    7. André Platzer Jan-David Quesel
      KeYmaera: A hybrid theorem prover for hybrid systems.
      IJCAR
      ABSTRACT Copy BibTex⧉   PDF   Slides
    8. André Platzer Jan-David Quesel
      Logical verification and systematic parametric analysis in train control.
      HSCC
      ABSTRACT Copy BibTex⧉   PDF

    2007

    1. A temporal dynamic logic for verifying hybrid system invariants
      LFCS
      ABSTRACT Copy BibTex⧉   PDF   Slides
    2. A temporal dynamic logic for verifying hybrid system invariants
      Thesis
      Copy BibTex⧉   PDF
    3. Werner Damm Alfred Mikschl Jens Oehlerking Ernst-Rüdiger Olderog Jun Pang André Platzer Marc Segelken Boris Wirtz
      Automating verification of cooperation, control, and design in traffic applications
      Formal methods and hybrid real-time systems
      ABSTRACT Copy BibTex⧉   PDF
    4. Combining deduction and algebraic constraints for hybrid system analysis.
      VERIFY’07 at CADE, bremen, germany
      ABSTRACT Copy BibTex⧉   PDF   Slides Preprint
    5. Differential dynamic logic for verifying parametric hybrid systems.
      TABLEAUX
      ABSTRACT Copy BibTex⧉   PDF   Slides
    6. Differential dynamic logic for verifying parametric hybrid systems.
      Thesis
      Copy BibTex⧉   PDF
    7. Differential logic for hybrid system verification – reasoning about interacting discrete and continuous change
      Dagstuhl “zehn plus eins” – zehn informatik-graduiertenkollegs und ein informatik-forschungskolleg stellen sich vor
      Copy BibTex⧉
    8. Differential logic for reasoning about hybrid systems
      HSCC
      ABSTRACT Copy BibTex⧉   PDF
    9. Stephanie Kemper André Platzer
      SAT-based abstraction refinement for real-time systems
      Formal aspects of component software, third international workshop, FACS 2006, prague, czech republic, proceedings
      ABSTRACT Copy BibTex⧉   PDF   Slides
    10. André Platzer Edmund M. Clarke
      The image computation problem in hybrid systems model checking
      HSCC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    11. Towards a hybrid dynamic logic for hybrid dynamic systems
      ABSTRACT Copy BibTex⧉   PDF   Slides

    2006

    1. Dynamic logic with non-rigid functions: A basis for object-oriented program verification.
      IJCAR
      ABSTRACT Copy BibTex⧉   PDF   Slides

    2004

    1. An object-oriented dynamic logic with updates
      Thesis
      ABSTRACT Copy BibTex⧉   PDF   Slides
    2. Using a program verification calculus for constructing specifications from implementations
      ABSTRACT Copy BibTex⧉   PDF   Slides
    Jump to Category:
    Thesis Report Paper-Conference Manuscript Chapter Book Article-Journal Unknown

    thesis

    1. Katherine Kosaian
      Formally verifying algorithms for real quantifier elimination
      Ph.D. dissertation
      Copy BibTex⧉   PDF
    2. Deductive verification for ordinary differential equations: Safety, liveness, and stability
      Ph.D. dissertation
      Copy BibTex⧉   PDF
    3. Rose Bohrer
      Practical end-to-end verification of cyber-physical systems
      Ph.D. dissertation
      Copy BibTex⧉   PDF   Slides
    4. Nathan Fulton
      Verifiably safe autonomy for cyber-physical systems
      Ph.D. dissertation
      Copy BibTex⧉   PDF
    5. Sarah M. Loos
      Differential refinement logic
      Ph.D. dissertation
      Copy BibTex⧉   PDF   Slides
    6. Regression verification for programmable logic controller software
      Thesis
      Copy BibTex⧉
    7. Algorithms for Forbidden Pattern Recognition in Transition Diagrams
      Thesis
      Copy BibTex⧉
    8. Differential dynamic logics: Automated theorem proving for hybrid systems
      Ph.D. dissertation
      Copy BibTex⧉   PDF   Slides
    9. An object-oriented dynamic logic with updates
      Thesis
      ABSTRACT Copy BibTex⧉   PDF   Slides

    report

    1. Provably forgetting of information in manufacturing systems: Verification of the KASTEL industry demonstrator
      Copy BibTex⧉
    2. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      Copy BibTex⧉   PDF
    3. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      Copy BibTex⧉   PDF
    4. How to prove ‘all’ differential equation properties
      Copy BibTex⧉   PDF
    5. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      Copy BibTex⧉   PDF
    6. Regression verification for programmable logic controller software
      Copy BibTex⧉
    7. ModelPlex: Verified runtime validation of verified cyber-physical system models
      Copy BibTex⧉   PDF
    8. Differential hybrid games
      Copy BibTex⧉   PDF
    9. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Ryan Garnder Aurora Schmidt Erik Zawadzki André Platzer
      A formally verified hybrid system for the next-generation airborne collision avoidance system
      Copy BibTex⧉   PDF
    10. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      Copy BibTex⧉   PDF
    11. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      Copy BibTex⧉   PDF
    12. A complete axiomatization for differential game logic for hybrid games
      Copy BibTex⧉   PDF   Slides
    13. David W. Renshaw Sarah Loos André Platzer
      Mechanized safety proofs for disc-constrained aircraft
      Copy BibTex⧉   PDF
    14. Differential game logic for hybrid games
      Copy BibTex⧉   PDF
    15. The structure of differential invariants and differential cut elimination
      Copy BibTex⧉   PDF
    16. The complete proof theory of hybrid systems
      Copy BibTex⧉   PDF
    17. Stochastic differential dynamic logic for stochastic hybrid systems
      Copy BibTex⧉   PDF
    18. David W. Renshaw André Platzer
      Differential invariants and symbolic integration for distributed hybrid systems
      Copy BibTex⧉   PDF
    19. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      Copy BibTex⧉   PDF
    20. Quantified differential dynamic logic for distributed hybrid systems
      Copy BibTex⧉   PDF
    21. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification.
      Copy BibTex⧉   PDF
    22. Sumit Kumar Jha Edmund Clarke Christopher Langmead Axel Legay André Platzer Paolo Zuliani
      Statistical model checking for complex stochastic models in systems biology
      Copy BibTex⧉   PDF
    23. Real world verification
      Thesis
      Copy BibTex⧉   PDF
    24. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      Copy BibTex⧉   PDF
    25. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      Thesis
      Copy BibTex⧉   PDF
    26. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      Copy BibTex⧉   PDF
    27. Differential dynamic logic for verifying parametric hybrid systems.
      Thesis
      Copy BibTex⧉   PDF
    28. A temporal dynamic logic for verifying hybrid system invariants
      Thesis
      Copy BibTex⧉   PDF

    paper-conference

    1. Enguerrand Prebet Samuel Teuber André Platzer
      Verification of autonomous neural car control with KeYmaera X
      Rigorous state-based methods - 11th international conference, ABZ 2025, düsseldorf, germany, june 10-13, 2025, proceedings
      Copy BibTex⧉
    2. Julia Butte André Platzer
      Semi-competitive differential game logic
      Automated reasoning with analytic tableaux and related methods - 33rd international conference, TABLEAUX 2025, reykjavík, iceland, september 29 – october 3, 2025, proceedings
      Copy BibTex⧉
    3. Enguerrand Prebet André Platzer
      Uniform substitution for differential refinement logic
      IJCAR
      Copy BibTex⧉
    4. Noah Abou El Wafa André Platzer
      Complete game logic with sabotage
      LICS
      Copy BibTex⧉
    5. CESAR: Control envelope synthesis via angelic refinements
      TACAS
      Copy BibTex⧉   Slides
    6. Uniform substitution for dynamic logic with communicating hybrid programs
      CADE
      Copy BibTex⧉   Slides
    7. Refinements of hybrid dynamical systems logic
      Rigorous state-based methods - 9th international conference, ABZ 2023, nancy, france, proceedings
      Copy BibTex⧉   Slides
    8. Katherine Kosaian Yong Kiam Tan André Platzer
      A first complete algorithm for real quantifier elimination in Isabelle/HOL
      Proceedings of the 12th ACM SIGPLAN international conference on certified programs and proofs
      Copy BibTex⧉
    9. Verifying switched system stability with logic
      HSCC ’22: 25th ACM international conference on hybrid systems: Computation and control, milan, italy, may 4 - 6, 2022
      Copy BibTex⧉   Slides
    10. Learning to find proofs and theorems by learning to refine search strategies
      Advances in neural information processing systems
      Copy BibTex⧉   Slides
    11. Implicit definitions with differential equations for KeYmaera X - (system description)
      IJCAR
      Copy BibTex⧉   Slides
    12. Matias Scharager Katherine Cordwell Stefan Mitsch André Platzer
      Verified quadratic virtual substitution for real arithmetic
      FM
      Copy BibTex⧉   PDF   Slides
    13. Switched systems as hybrid programs
      7th IFAC conference on analysis and design of hybrid systems, ADHS 2021, brussels, belgium, july 7-9, 2021
      Copy BibTex⧉
    14. Runtime verification of generalized test tables
      NASA formal methods - 13th international symposium, NFM 2021, virtual event, may 24-28, 2021, proceedings
      Copy BibTex⧉
    15. Deductive stability proofs for ordinary differential equations
      Tools and algorithms for the construction and analysis of systems - 27th international conference, TACAS 2021, held as part of the european joint conferences on theory and practice of software, ETAPS 2021, proceedings, part II
      Copy BibTex⧉   PDF   Slides
    16. Katherine Cordwell Yong Kiam Tan André Platzer
      A verified decision procedure for univariate real arithmetic with the BKR algorithm
      12th international conference on interactive theorem proving, ITP 2021, june 29 to july 1, 2021, rome, italy
      Copy BibTex⧉   PDF   Slides
    17. The PGP Key Server: Challenge Manual
      VerifyThis long-term challenge: proceedings
      Copy BibTex⧉
    18. The KeY Approach on Hagrid
      VerifyThis long-term challenge: proceedings
      Copy BibTex⧉
    19. Relational test tables: A practical specification language for evolution and security
      FormaliSE@ICSE 2020: 8th international conference on formal methods in software engineering, seoul, republic of korea, july 13, 2020
      Copy BibTex⧉
    20. Brandon Bohrer André Platzer
      Refining constructive hybrid games
      5th international conference on formal structures for computation and deduction, FSCD 2020, june 29 - july 5, 2020, paris, france
      Copy BibTex⧉   PDF   Slides
    21. Modular Regression verification for reactive systems
      Leveraging applications of formal methods, verification and validation: Engineering principles - 9th international symposium on leveraging applications of formal methods, ISoLA 2020, rhodes, greece, october 20-30, 2020, proceedings, part II
      Copy BibTex⧉
    22. Brandon Bohrer André Platzer
      Constructive hybrid games
      IJCAR
      Copy BibTex⧉   PDF   Slides
    23. Brandon Bohrer André Platzer
      Constructive game logic
      Programming languages and systems - 29th european symposium on programming, ESOP 2020, held as part of the european joint conferences on theory and practice of software, ETAPS 2020, dublin, ireland, april 25-30, 2020, proceedings
      Copy BibTex⧉   PDF   Slides
    24. Nathan Fulton André Platzer
      Verifiably safe off-model reinforcement learning
      TACAS
      Copy BibTex⧉   PDF
    25. Uniform substitution at one fell swoop
      CADE
      Copy BibTex⧉   PDF   Slides
    26. Katherine Cordwell André Platzer
      Towards physical hybrid systems
      CADE
      Copy BibTex⧉   PDF   Slides
    27. The logical path to autonomous cyber-physical systems
      QEST
      Copy BibTex⧉   PDF   Slides
    28. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: A framework for sound continuous invariant generation
      FM
      Copy BibTex⧉   PDF   Slides
    29. On the preservation of the trust by regression verification of PLC software for cyber-physical systems of systems
      17th IEEE international conference on industrial informatics, INDIN 2019, helsinki, finland, july 22-25, 2019
      Copy BibTex⧉
    30. HyPLC: Hybrid programmable logic controller program translation for verification
      ICCPS
      Copy BibTex⧉   PDF
    31. João Martins André Platzer João Leite
      Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems
      TABLEAUX
      Copy BibTex⧉   PDF   Slides
    32. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      CADE
      Copy BibTex⧉   PDF   Slides
    33. An axiomatic approach to liveness for differential equations
      FM
      Copy BibTex⧉   PDF   Slides
    34. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Magnus O. Myreen André Platzer
      VeriPhy: Verified controller executables from verified cyber-physical system models
      PLDI
      Copy BibTex⧉   PDF   Slides
    35. Andrew Sogokon Khalil Ghorbal Yong Kiam Tan André Platzer
      Vector barrier certificates and comparison systems
      FM
      Copy BibTex⧉   PDF   Slides
    36. Uniform substitution for differential game logic
      IJCAR
      Copy BibTex⧉   PDF   Slides
    37. Nathan Fulton André Platzer
      Safe reinforcement learning via formal methods: Toward safe control through proof and learning
      Proceedings of the thirty-second AAAI conference on artificial intelligence, february 2-7, 2018, new orleans, louisiana, USA.
      Copy BibTex⧉   PDF   Slides Preprint
    38. Nathan Fulton André Platzer
      Safe AI for CPS
      IEEE international test conference, ITC 2018, phoenix, AZ, USA, october 29 - nov. 1, 2018
      Copy BibTex⧉   PDF   Slides
    39. Relational equivalence proofs between imperative and MapReduce algorithms
      Verified software. Theories, tools, and experiments - 10th international conference, VSTTE 2018, oxford, UK, july 18-19, 2018, revised selected papers
      Copy BibTex⧉
    40. Proving equivalence between imperative and MapReduce implementations using program transformations
      Proceedings third workshop on models for formal analysis of real systems and sixth international workshop on verification and program transformation, MARS/VPT@ETAPS 2018, thessaloniki, greece, 20th april 2018
      Copy BibTex⧉
    41. Differential equation axiomatization: The impressive power of differential ghosts
      LICS
      Copy BibTex⧉   PDF   Slides
    42. Brandon Bohrer Adriel Luo Xue An Chuang André Platzer
      CoasterX: A case study in component-driven hybrid systems proof automation
      6th IFAC conference on analysis and design of hybrid systems, ADHS 2018, oxford, UK, july 11-13, 2018
      Copy BibTex⧉   PDF   Slides
    43. Sarah Grebing An Thuy Tien Luong Alexander Weigl
      Adding text-based interaction to a direct-manipulation interface for program verification – lessons learned
      13th international workshop on user interfaces for theorem provers (UITP 2018)
      Copy BibTex⧉
    44. Achieving delta description of the control software for an automated production system evolution
      14th IEEE international conference on automation science and engineering, CASE 2018, munich, germany, august 20-24, 2018
      Copy BibTex⧉
    45. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      LICS
      Copy BibTex⧉   PDF   Slides
    46. Andreas Müller Stefan Mitsch Wieland Schwinger André Platzer
      A component-based hybrid systems verification and implementation tool in KeYmaera X (tool demonstration)
      Cyber physical systems. Model-based design - 8th international workshop, CyPhy 2018, and 14th international workshop, WESE 2018, turin, italy, october 4-5, 2018, revised selected papers
      Copy BibTex⧉   PDF
    47. Generation of monitoring functions in production automation using test specifications
      15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      Copy BibTex⧉
    48. Generalized test tables: A powerful and intuitive specification language for reactive systems
      15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      Copy BibTex⧉
    49. Generalised test tables: A practical specification language for reactive systems
      Integrated formal methods - 13th international conference, IFM 2017, turin, italy, september 20-22, 2017, proceedings
      Copy BibTex⧉
    50. Brandon Bohrer Vincent Rahli Ivana Vukotic Marcus Völp André Platzer
      Formally verified differential dynamic logic
      Certified programs and proofs - 6th ACM SIGPLAN conference, CPP 2017, paris, france, january 16-17, 2017
      Copy BibTex⧉   PDF   Slides
    51. Stefan Mitsch Marco Gario Christof J. Budnik Michael Golm André Platzer
      Formal verification of train control with air pressure brakes
      RSSRail
      Copy BibTex⧉   PDF   Slides
    52. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Change and delay contracts for hybrid system component verification
      FASE
      Copy BibTex⧉   PDF   Slides
    53. Nathan Fulton Stefan Mitsch Brandon Bohrer André Platzer
      Bellerophon: Tactical theorem proving for hybrid systems
      ITP
      Copy BibTex⧉   PDF   Slides
    54. The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving
      3rd workshop on formal integrated development environment
      Copy BibTex⧉   PDF
    55. Sound probabilistic #SAT with projection
      Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      Copy BibTex⧉
    56. Logic & proofs for cyber-physical systems
      IJCAR
      ABSTRACT Copy BibTex⧉   PDF   Slides
    57. Efficient SAT-based pre-image enumeration for quantitative information flow in programs
      Data privacy management and security assurance - 11th international workshop, DPM 2016 and 5th international workshop, QASA 2016, heraklion, crete, greece, september 26-27, 2016, proceedings
      Copy BibTex⧉
    58. Sarah M. Loos André Platzer
      Differential refinement logic
      LICS
      Copy BibTex⧉   PDF   Slides
    59. A verification-supported evolution approach to assist software application engineers in industrial factory automation
      IEEE international symposium on assembly and manufacturing (ISAM 2016)
      ABSTRACT Copy BibTex⧉
    60. Andrew Sogokon Khalil Ghorbal Paul B. Jackson André Platzer
      A method for invariant generation for polynomial continuous systems
      VMCAI
      Copy BibTex⧉   PDF   Slides
    61. Nathan Fulton André Platzer
      A logic of proofs for differential dynamic logic: Toward independently checkable proof certificates for dynamic logics
      Proceedings of the 2016 conference on certified programs and proofs, CPP 2016, st. Petersburg, FL, USA, january 18-19, 2016
      Copy BibTex⧉   PDF   Slides
    62. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      IFM
      Copy BibTex⧉   PDF   Slides
    63. Verified traffic networks: Component-based verification of cyber-physical flow systems
      ITSC
      Copy BibTex⧉   PDF   Slides
    64. Regression verification for programmable logic controller software
      Formal methods and software engineering - 17th international conference on formal engineering methods, ICFEM 2015, paris, france, november 3-5, 2015, proceedings
      Copy BibTex⧉
    65. Proving equivalence between control software variants for Programmable Logic Controllers: Using Regression Verification to Reduce Unneeded Variant Diversity
      IEEE international conference on emerging technologies and factory automation, ETFA
      ABSTRACT Copy BibTex⧉
    66. Nathan Fulton Stefan Mitsch Jan-David Quesel Marcus Völp André Platzer
      KeYmaera X: An axiomatic tactical theorem prover for hybrid systems
      CADE
      Copy BibTex⧉   PDF   Slides
    67. How to prove hybrid systems and why that matters
      ICCSE
      Copy BibTex⧉   PDF
    68. Nikos Arechiga James Kapinski Jyotirmoy V. Deshmukh André Platzer Bruce H. Krogh
      Forward invariant cuts to simplify proofs of safety
      EMSOFT
      Copy BibTex⧉
    69. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Ryan Gardner Aurora Schmidt Erik Zawadzki André Platzer
      Formal verification of ACAS X, an industrial airborne collision avoidance system
      EMSOFT
      Copy BibTex⧉   PDF
    70. A uniform substitution calculus for differential dynamic logic
      CADE
      Copy BibTex⧉   PDF   Slides Preprint
    71. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking differential invariance of algebraic sets
      VMCAI
      Copy BibTex⧉   PDF   Slides
    72. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Ryan Gardner Aurora Schmidt Erik Zawadzki André Platzer
      A formally verified hybrid system for the next-generation airborne collision avoidance system
      TACAS
      Copy BibTex⧉   PDF
    73. Stefan Mitsch Jan-David Quesel André Platzer
      Refactoring, refinement, and reasoning: A logical characterization for hybrid systems
      FM
      Copy BibTex⧉   PDF   Slides
    74. ModelPlex: Verified runtime validation of verified cyber-physical system models
      RV
      Copy BibTex⧉   PDF   Slides
    75. Khalil Ghorbal Andrew Sogokon André Platzer
      Invariance of conjunctions of polynomial equalities for algebraic differential equations
      SAS
      Copy BibTex⧉   PDF   Slides
    76. Stefan Mitsch Jan-David Quesel André Platzer
      From safety to guilty & from liveness to niceness
      5th workshop on formal methods for robotics and automation
      Copy BibTex⧉   PDF
    77. Jean-Baptiste Jeannin André Platzer
      dTL^2: Differential temporal dynamic logic with nested temporalities for hybrid systems
      IJCAR
      Copy BibTex⧉   PDF   Slides
    78. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      TACAS
      Copy BibTex⧉   PDF   Slides
    79. Teaching CPS foundations with contracts
      CPS-ed
      Copy BibTex⧉   PDF   Slides Preprint
    80. On provably safe obstacle avoidance for autonomous robotic ground vehicles
      Robotics: Science and systems
      Copy BibTex⧉   PDF   Slides
    81. Sarah M. Loos David W. Renshaw André Platzer
      Formal verification of distributed aircraft controllers
      Hybrid systems: Computation and control (part of CPS week 2013), HSCC’13, philadelphia, PA, USA, april 8-13, 2013
      Copy BibTex⧉   PDF   Slides
    82. Sarah M. Loos David Witmer Peter Steenkiste André Platzer
      Efficiency analysis of formally verified adaptive cruise controllers
      ITSC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    83. Yanni Kouskoulas David W. Renshaw André Platzer Peter Kazanzides
      Certifying the safe design of a virtual fixture control algorithm for a surgical robot
      Hybrid systems: Computation and control (part of CPS week 2013), HSCC’13, philadelphia, PA, USA, april 8-13, 2013
      Copy BibTex⧉   PDF   Slides
    84. Erik P. Zawadzki Geoffrey J. Gordon André Platzer
      A projection algorithm for strictly monotone linear complementarity problems
      6th NIPS workshop on optimization for machine learning
      Copy BibTex⧉   PDF Preprint
    85. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      IJCAI
      Copy BibTex⧉   PDF Preprint
    86. Nikos Aréchiga Sarah M. Loos André Platzer Bruce H. Krogh
      Using theorem provers to guarantee closed-loop system properties
      ACC
      Copy BibTex⧉   PDF
    87. Towards formal verification of freeway traffic control
      ICCPS
      Copy BibTex⧉   PDF   Slides
    88. The complete proof theory of hybrid systems
      LICS
      ABSTRACT Copy BibTex⧉   PDF   Slides
    89. David Henriques João G. Martins Paolo Zuliani André Platzer Edmund M. Clarke
      Statistical model checking for Markov decision processes
      QEST
      ABSTRACT Copy BibTex⧉   PDF   Slides
    90. Jan-David Quesel André Platzer
      Playing hybrid games with KeYmaera
      IJCAR
      Copy BibTex⧉   PDF   Slides
    91. Logics of dynamical systems
      LICS
      ABSTRACT Copy BibTex⧉   PDF   Slides
    92. Logical analysis of hybrid systems: A complete answer to a complexity challenge
      DCFS
      Copy BibTex⧉   PDF
    93. A differential operator approach to equational differential invariants
      ITP
      ABSTRACT Copy BibTex⧉   PDF   Slides
    94. Akshay Rajhans Ajinkya Bhave Sarah M. Loos Bruce H. Krogh André Platzer David Garlan
      Using parameters in architectural views to support heterogeneous design and verification
      CDC
      Copy BibTex⧉   PDF
    95. Stochastic differential dynamic logic for stochastic hybrid programs
      CADE
      ABSTRACT Copy BibTex⧉   PDF   Slides
    96. João Martins André Platzer João Leite
      Statistical model checking for distributed probabilistic-control hybrid automata with smart grid applications
      ICFEM
      Copy BibTex⧉   PDF   Slides
    97. Sarah M. Loos André Platzer
      Safe intersections: At the crossing of hybrid systems and verification
      ITSC
      Copy BibTex⧉   PDF   Slides
    98. Sicun Gao André Platzer Edmund M. Clarke
      Quantifier elimination over finite fields with Gröbner bases
      CAI
      Copy BibTex⧉   PDF
    99. Quantified differential invariants
      HSCC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    100. Logic and compositional verification of hybrid systems (invited tutorial)
      CAV
      ABSTRACT Copy BibTex⧉   PDF   Slides
    101. David W. Renshaw Sarah M. Loos André Platzer
      Distributed theorem proving for distributed hybrid systems
      ICFEM
      Copy BibTex⧉   PDF
    102. Erik P. Zawadzki Geoffrey J. Gordon André Platzer
      An instantiation-based theorem prover for first-order programming
      Proceedings of the 14th international conference on artifical intelligence and statistics (AISTATS) 2011, fort lauderdale, FL, USA
      Copy BibTex⧉   PDF Preprint
    103. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      FM
      Copy BibTex⧉   PDF   Slides
    104. Quantified differential dynamic logic for distributed hybrid systems
      CSL
      ABSTRACT Copy BibTex⧉   PDF   Slides
    105. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      HSCC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    106. Real world verification
      CADE
      ABSTRACT Copy BibTex⧉   PDF   Slides
    107. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      FM
      ABSTRACT Copy BibTex⧉   PDF   Slides
    108. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      ICFEM
      ABSTRACT Copy BibTex⧉   PDF   Slides
    109. Sumit Kumar Jha Edmund Clarke Christopher Langmead Axel Legay André Platzer Paolo Zuliani
      A Bayesian approach to model checking biological systems
      CMSB
      ABSTRACT Copy BibTex⧉   PDF
    110. André Platzer Jan-David Quesel
      Logical verification and systematic parametric analysis in train control.
      HSCC
      ABSTRACT Copy BibTex⧉   PDF
    111. André Platzer Jan-David Quesel
      KeYmaera: A hybrid theorem prover for hybrid systems.
      IJCAR
      ABSTRACT Copy BibTex⧉   PDF   Slides
    112. Differential dynamic logics. Automated theorem proving for hybrid systems
      Proceedings des gemeinsamen workshops der graduiertenkollegs 2008, dagstuhl
      Copy BibTex⧉
    113. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      CAV
      ABSTRACT Copy BibTex⧉   PDF   Slides
    114. Edmund M. Clarke Bruce Krogh André Platzer Raj Rajkumar
      Analysis and verification challenges for cyber-physical transportation systems
      NITRD national workshop for research on transportation cyber-physical systems: Automotive, aviation, and rail
      ABSTRACT Copy BibTex⧉   PDF
    115. André Platzer Edmund M. Clarke
      The image computation problem in hybrid systems model checking
      HSCC
      ABSTRACT Copy BibTex⧉   PDF   Slides
    116. Stephanie Kemper André Platzer
      SAT-based abstraction refinement for real-time systems
      Formal aspects of component software, third international workshop, FACS 2006, prague, czech republic, proceedings
      ABSTRACT Copy BibTex⧉   PDF   Slides
    117. Differential logic for reasoning about hybrid systems
      HSCC
      ABSTRACT Copy BibTex⧉   PDF
    118. Differential logic for hybrid system verification – reasoning about interacting discrete and continuous change
      Dagstuhl “zehn plus eins” – zehn informatik-graduiertenkollegs und ein informatik-forschungskolleg stellen sich vor
      Copy BibTex⧉
    119. Differential dynamic logic for verifying parametric hybrid systems.
      TABLEAUX
      ABSTRACT Copy BibTex⧉   PDF   Slides
    120. Combining deduction and algebraic constraints for hybrid system analysis.
      VERIFY’07 at CADE, bremen, germany
      ABSTRACT Copy BibTex⧉   PDF   Slides Preprint
    121. Werner Damm Alfred Mikschl Jens Oehlerking Ernst-Rüdiger Olderog Jun Pang André Platzer Marc Segelken Boris Wirtz
      Automating verification of cooperation, control, and design in traffic applications
      Formal methods and hybrid real-time systems
      ABSTRACT Copy BibTex⧉   PDF
    122. A temporal dynamic logic for verifying hybrid system invariants
      LFCS
      ABSTRACT Copy BibTex⧉   PDF   Slides
    123. Dynamic logic with non-rigid functions: A basis for object-oriented program verification.
      IJCAR
      ABSTRACT Copy BibTex⧉   PDF   Slides

    manuscript

    1. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      Relational test tables: A practical specification language for evolution and security
      Copy BibTex⧉
    2. Sarah M. Loos André Platzer
      Teaching cyber-physical systems with logic
      Copy BibTex⧉   PDF

    chapter

    1. The VerifyThis Collaborative Long Term Challenge
      Copy BibTex⧉
    2. A retrospective on developing hybrid systems provers in the KeYmaera family - A tale of three provers
      Copy BibTex⧉   PDF
    3. Formal verification of evolutionary changes
      Copy BibTex⧉
    4. Laurent Doyen Goran Frehse George J. Pappas André Platzer
      Verification of hybrid systems
      Copy BibTex⧉   PDF

    book

    1. The 28th international conference on automated deduction
      Springer. in , Springer
      Copy BibTex⧉
    2. VerifyThis long-term challenge: proceedings
      in , Karlsruhe
      Copy BibTex⧉
    3. 17th IEEE international conference on industrial informatics, INDIN 2019, helsinki, finland, july 22-25, 2019
      IEEE. in , IEEE
      Copy BibTex⧉
    4. Verified software. Theories, tools, and experiments - 10th international conference, VSTTE 2018, oxford, UK, july 18-19, 2018, revised selected papers
      Springer. in , Springer
      Copy BibTex⧉
    5. Proceedings third workshop on models for formal analysis of real systems and sixth international workshop on verification and program transformation, MARS/VPT@ETAPS 2018, thessaloniki, greece, 20th april 2018
      in ,
      Copy BibTex⧉
    6. Logical foundations of cyber-physical systems
      Springer. in , Springer Cham
      Copy BibTex⧉   Slides
    7. 15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      IEEE. in , IEEE
      Copy BibTex⧉
    8. Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      in ,
      Copy BibTex⧉
    9. Correct system design symposium in honor of ernst-rüdiger olderog on the occasion of his 60th birthday oldenburg, germany, september 8-9, 2015 proceedings
      Springer. in , Springer
      Copy BibTex⧉
    10. Logical analysis of hybrid systems: Proving theorems for complex dynamics
      Springer. in , Springer Heidelberg
      Copy BibTex⧉

    article-journal

    1. Rachel Cleaveland Stefan Mitsch André Platzer
      Formally verified next-generation airborne collision avoidance games in ACAS X
      Copy BibTex⧉
    2. William Simmons André Platzer
      Differential elimination and algebraic invariants of polynomial dynamical systems
      Copy BibTex⧉
    3. Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces
      Copy BibTex⧉   Slides
    4. Qin Lin Stefan Mitsch André Platzer John M. Dolan
      Safe and resilient practical waypoint-following for autonomous vehicles
      Copy BibTex⧉   PDF
    5. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: Sound continuous invariant generation
      Copy BibTex⧉   PDF
    6. Noah Abou El Wafa André Platzer
      First-order game logic and modal mu-calculus
      Copy BibTex⧉
    7. Brandon Bohrer André Platzer
      Structured proofs for adversarial cyber-physical systems
      Copy BibTex⧉   PDF
    8. An axiomatic approach to existence and liveness for differential equations
      Copy BibTex⧉   PDF
    9. Differential equation invariance axiomatization
      Copy BibTex⧉   PDF   Slides
    10. Uniform substitution at one fell swoop
      Copy BibTex⧉
    11. Relational test tables: A practical specification language for evolution and security
      Copy BibTex⧉ Preprint
    12. Overview of logical foundations of cyber-physical systems
      Copy BibTex⧉ Preprint
    13. Differential equation invariance axiomatization
      Copy BibTex⧉ Preprint
    14. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Andrew Sogokon André Platzer
      A formal safety net for waypoint following in ground robots
      Copy BibTex⧉
    15. Verified runtime validation for partially observable hybrid systems
      Copy BibTex⧉
    16. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Tactical contract composition for hybrid system component verification
      Copy BibTex⧉   PDF
    17. Relational equivalence proofs between imperative and MapReduce algorithms
      Copy BibTex⧉ Preprint
    18. Debugging program verification proof scripts (tool paper)
      Copy BibTex⧉ Preprint
    19. Applicability of generalized test tables: A case study using the manufacturing system demonstrator xPPU
      Copy BibTex⧉
    20. Franz Franchetti Tze Meng Low Stefan Mitsch Juan Paolo Mendoza Liangyan Gui Amarin Phaosawasdi David Padua Soummya Kar José M. F. Moura Mike Franusich Jeremy Johnson André Platzer Manuela Veloso
      High-assurance SPIRAL: End-to-end guarantees for robot and car control
      Copy BibTex⧉   PDF
    21. Stefan Mitsch Khalil Ghorbal David Vogelbacher André Platzer
      Formal verification of obstacle avoidance and navigation of ground robots
      Copy BibTex⧉   PDF
    22. Differential hybrid games
      Copy BibTex⧉   PDF
    23. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
      Copy BibTex⧉   PDF
    24. Jean-Baptiste Jeannin Khalil Ghorbal Yanni Kouskoulas Aurora Schmidt Ryan Gardner Stefan Mitsch André Platzer
      A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system
      Copy BibTex⧉   PDF
    25. A complete uniform substitution calculus for differential dynamic logic
      Copy BibTex⧉   PDF
    26. ModelPlex: Verified runtime validation of verified cyber-physical system models
      Copy BibTex⧉   PDF
    27. Jan-David Quesel Stefan Mitsch Sarah Loos Nikos Aréchiga André Platzer
      How to model and prove hybrid systems with KeYmaera: A tutorial on safety
      Copy BibTex⧉   PDF
    28. Stefan Mitsch André Platzer Werner Retschitzegger Wieland Schwinger
      Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems
      Copy BibTex⧉   PDF
    29. Differential game logic
      Copy BibTex⧉   PDF
    30. Akshay Rajhans Ajinkya Bhave Ivan Ruchkin Bruce H. Krogh David Garlan André Platzer Bradley Schmerl
      Supporting heterogeneity in cyber-physical systems architectures
      Copy BibTex⧉
    31. Khalil Ghorbal Jean-Baptiste Jeannin Erik P. Zawadzki André Platzer Geoffrey J. Gordon Peter Capell
      Hybrid theorem proving of aerospace systems: Applications and challenges
      Copy BibTex⧉   PDF
    32. Stefan Mitsch Grant Olney Passmore André Platzer
      Collaborative verification-driven engineering of hybrid systems
      Copy BibTex⧉   PDF
    33. Analog and hybrid computation: Dynamical systems and programming languages
      Copy BibTex⧉   PDF Preprint
    34. Yanni Kouskoulas André Platzer Peter Kazanzides
      Formal methods for robotic system control software
      Copy BibTex⧉   PDF Preprint
    35. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      ABSTRACT Copy BibTex⧉   PDF
    36. The structure of differential invariants and differential cut elimination
      ABSTRACT Copy BibTex⧉   PDF
    37. Logical analysis of hybrid systems: A complete answer to a complexity challenge
      Copy BibTex⧉   PDF
    38. Dynamic logics of dynamical systems
      Copy BibTex⧉
    39. A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems
      Copy BibTex⧉   PDF
    40. Differential-algebraic dynamic logic for differential-algebraic programs
      ABSTRACT Copy BibTex⧉   PDF
    41. Differential dynamic logics: Automated theorem proving for hybrid systems
      ABSTRACT Copy BibTex⧉
    42. Verification of cyberphysical transportation systems
      ABSTRACT Copy BibTex⧉
    43. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT Copy BibTex⧉   PDF
    44. Differential dynamic logic for hybrid systems.
      ABSTRACT Copy BibTex⧉   PDF
    45. Towards a hybrid dynamic logic for hybrid dynamic systems
      ABSTRACT Copy BibTex⧉   PDF   Slides

    1. Weihan Li
      Formal verification of the winning strategies of pursuit-evasion games
      Copy BibTex⧉   PDF
    2. Rachel Cleaveland
      Formal verification of next-generation airborne collision avoidance system with adversarial intruder behavior
      Copy BibTex⧉   PDF   Slides
    3. KeYmaera X tutorial
      Copy BibTex⧉   PDF
    4. KASTEL industry 4.0 demonstrator: Provably forgetting information in PLC software
      Copy BibTex⧉
    5. Videos for logical foundations of cyber-physical systems
      Copy BibTex⧉
    6. Foundations of cyber-physical systems
      Copy BibTex⧉
    7. Foundations of cyber-physical systems
      Copy BibTex⧉   Slides
    8. Foundations of cyber-physical systems
      Copy BibTex⧉   PDF
    9. Annika Peterson
      Formal verification of a controlled flight between two robots: A case study
      Copy BibTex⧉   PDF
    10. Foundations of cyber-physical systems
      Copy BibTex⧉   PDF
    11. Foundations of cyber-physical systems
      Copy BibTex⧉   PDF
    12. Using a program verification calculus for constructing specifications from implementations
      ABSTRACT Copy BibTex⧉   PDF   Slides