Publications

    Jump to Year:
    20242023202220212020201920182017201620152014201320122011201020092008200720062004

    2024

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

    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
      ABSTRACT
    2. William Simmons André Platzer
      Differential elimination and algebraic invariants of polynomial dynamical systems
      ABSTRACT
    3. Rachel Cleaveland Stefan Mitsch André Platzer
      Formally verified next-generation airborne collision avoidance games in ACAS X
      ABSTRACT
    4. Katherine Kosaian
      Formally verifying algorithms for real quantifier elimination
      Ph.D. dissertation
      ABSTRACT   PDF
    5. Refinements of hybrid dynamical systems logic
      Rigorous state-based methods - 9th international conference, ABZ 2023, nancy, france, proceedings
      ABSTRACT   Slides
    6. Uniform substitution for dynamic logic with communicating hybrid programs
      CADE
      ABSTRACT   Slides

    2022

    1. Deductive verification for ordinary differential equations: Safety, liveness, and stability
      Ph.D. dissertation
      ABSTRACT   PDF
    2. Noah Abou El Wafa André Platzer
      First-order game logic and modal mu-calculus
      ABSTRACT
    3. Weihan Li
      Formal verification of the winning strategies of pursuit-evasion games
      ABSTRACT   PDF
    4. Implicit definitions with differential equations for KeYmaera X - (system description)
      IJCAR
      ABSTRACT   Slides
    5. Learning to find proofs and theorems by learning to refine search strategies
      Advances in neural information processing systems
      ABSTRACT   Slides
    6. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: Sound continuous invariant generation
      ABSTRACT   PDF
    7. Qin Lin Stefan Mitsch André Platzer John M. Dolan
      Safe and resilient practical waypoint-following for autonomous vehicles
      ABSTRACT   PDF
    8. Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces
      ABSTRACT   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
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    2. An axiomatic approach to existence and liveness for differential equations
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    4. Rachel Cleaveland
      Formal verification of next-generation airborne collision avoidance system with adversarial intruder behavior
      ABSTRACT   PDF   Slides
    5. Rose Bohrer
      Practical end-to-end verification of cyber-physical systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides
    6. Runtime verification of generalized test tables
      NASA formal methods - 13th international symposium, NFM 2021, virtual event, may 24-28, 2021, proceedings
      ABSTRACT
    7. Brandon Bohrer André Platzer
      Structured proofs for adversarial cyber-physical systems
      ABSTRACT   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
      ABSTRACT
    9. The 28th international conference on automated deduction
      Springer. in , Springer
      ABSTRACT
    10. Matias Scharager Katherine Cordwell Stefan Mitsch André Platzer
      Verified quadratic virtual substitution for real arithmetic
      FM
      ABSTRACT   PDF   Slides

    2020

    1. A retrospective on developing hybrid systems provers in the KeYmaera family - A tale of three provers
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    3. Brandon Bohrer André Platzer
      Constructive hybrid games
      IJCAR
      ABSTRACT   PDF   Slides
    4. Differential equation invariance axiomatization
      ABSTRACT   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
      ABSTRACT
    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
      ABSTRACT   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
      ABSTRACT
    8. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      Relational test tables: A practical specification language for evolution and security
      ABSTRACT
    9. The KeY Approach on Hagrid
      VerifyThis long-term challenge: proceedings
      ABSTRACT
    10. The VerifyThis Collaborative Long Term Challenge
      ABSTRACT
    11. VerifyThis long-term challenge: proceedings
      in , Karlsruhe
      ABSTRACT

    2019

    1. 17th IEEE international conference on industrial informatics, INDIN 2019, helsinki, finland, july 22-25, 2019
      IEEE. in , IEEE
      ABSTRACT
    2. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Andrew Sogokon André Platzer
      A formal safety net for waypoint following in ground robots
      ABSTRACT
    3. An axiomatic approach to liveness for differential equations
      FM
      ABSTRACT   PDF   Slides
    4. Differential equation invariance axiomatization
      ABSTRACT Preprint
    5. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      CADE
      ABSTRACT   PDF   Slides
    6. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      ABSTRACT   PDF
    7. João Martins André Platzer João Leite
      Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems
      TABLEAUX
      ABSTRACT   PDF   Slides
    8. Formal verification of evolutionary changes
      ABSTRACT
    9. HyPLC: Hybrid programmable logic controller program translation for verification
      ICCPS
      ABSTRACT   PDF
    10. KASTEL industry 4.0 demonstrator: Provably forgetting information in PLC software
      ABSTRACT
    11. KeYmaera X tutorial
      ABSTRACT   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
      ABSTRACT
    13. Overview of logical foundations of cyber-physical systems
      ABSTRACT Preprint
    14. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: A framework for sound continuous invariant generation
      FM
      ABSTRACT   PDF   Slides
    15. Provably forgetting of information in manufacturing systems: Verification of the KASTEL industry demonstrator
      ABSTRACT
    16. Relational test tables: A practical specification language for evolution and security
      ABSTRACT Preprint
    17. The logical path to autonomous cyber-physical systems
      QEST
      ABSTRACT   PDF   Slides
    18. Katherine Cordwell André Platzer
      Towards physical hybrid systems
      CADE
      ABSTRACT   PDF   Slides
    19. Uniform substitution at one fell swoop
      CADE
      ABSTRACT   PDF   Slides
    20. Uniform substitution at one fell swoop
      ABSTRACT
    21. Nathan Fulton André Platzer
      Verifiably safe off-model reinforcement learning
      TACAS
      ABSTRACT   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
      ABSTRACT   PDF
    2. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      LICS
      ABSTRACT   PDF   Slides
    3. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      ABSTRACT   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
      ABSTRACT
    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)
      ABSTRACT
    6. Applicability of generalized test tables: A case study using the manufacturing system demonstrator xPPU
      ABSTRACT
    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
      ABSTRACT   PDF   Slides
    8. Debugging program verification proof scripts (tool paper)
      ABSTRACT Preprint
    9. Differential equation axiomatization: The impressive power of differential ghosts
      LICS
      ABSTRACT   PDF   Slides
    10. Logical foundations of cyber-physical systems
      Springer. in , Springer Cham
      ABSTRACT   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 ,
      ABSTRACT
    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
      ABSTRACT
    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
      ABSTRACT
    14. Relational equivalence proofs between imperative and MapReduce algorithms
      ABSTRACT Preprint
    15. Nathan Fulton André Platzer
      Safe AI for CPS
      IEEE international test conference, ITC 2018, phoenix, AZ, USA, october 29 - nov. 1, 2018
      ABSTRACT   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.
      ABSTRACT   PDF   Slides Preprint
    17. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Tactical contract composition for hybrid system component verification
      ABSTRACT   PDF
    18. Uniform substitution for differential game logic
      IJCAR
      ABSTRACT   PDF   Slides
    19. Andrew Sogokon Khalil Ghorbal Yong Kiam Tan André Platzer
      Vector barrier certificates and comparison systems
      FM
      ABSTRACT   PDF   Slides
    20. Nathan Fulton
      Verifiably safe autonomy for cyber-physical systems
      Ph.D. dissertation
      ABSTRACT   PDF
    21. Laurent Doyen Goran Frehse George J. Pappas André Platzer
      Verification of hybrid systems
      ABSTRACT   PDF
    22. Verified runtime validation for partially observable hybrid systems
      ABSTRACT
    23. Verified software. Theories, tools, and experiments - 10th international conference, VSTTE 2018, oxford, UK, july 18-19, 2018, revised selected papers
      Springer. in , Springer
      ABSTRACT
    24. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Magnus O. Myreen André Platzer
      VeriPhy: Verified controller executables from verified cyber-physical system models
      PLDI
      ABSTRACT   PDF   Slides
    25. Videos for logical foundations of cyber-physical systems
      ABSTRACT

    2017

    1. 15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      IEEE. in , IEEE
      ABSTRACT
    2. A complete uniform substitution calculus for differential dynamic logic
      ABSTRACT   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
      ABSTRACT   PDF
    4. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
      ABSTRACT   PDF
    5. Nathan Fulton Stefan Mitsch Brandon Bohrer André Platzer
      Bellerophon: Tactical theorem proving for hybrid systems
      ITP
      ABSTRACT   PDF   Slides
    6. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Change and delay contracts for hybrid system component verification
      FASE
      ABSTRACT   PDF   Slides
    7. Differential hybrid games
      ABSTRACT   PDF
    8. Stefan Mitsch Khalil Ghorbal David Vogelbacher André Platzer
      Formal verification of obstacle avoidance and navigation of ground robots
      ABSTRACT   PDF
    9. Stefan Mitsch Marco Gario Christof J. Budnik Michael Golm André Platzer
      Formal verification of train control with air pressure brakes
      RSSRail
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    11. Foundations of cyber-physical systems
      ABSTRACT
    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
      ABSTRACT
    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
      ABSTRACT
    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
      ABSTRACT
    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
      ABSTRACT   PDF
    16. How to prove ‘all’ differential equation properties
      ABSTRACT   PDF

    2016

    1. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      IFM
      ABSTRACT   PDF   Slides
    2. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    4. Andrew Sogokon Khalil Ghorbal Paul B. Jackson André Platzer
      A method for invariant generation for polynomial continuous systems
      VMCAI
      ABSTRACT   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
    6. Sarah M. Loos André Platzer
      Differential refinement logic
      LICS
      ABSTRACT   PDF   Slides
    7. Sarah M. Loos
      Differential refinement logic
      Ph.D. dissertation
      ABSTRACT   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
      ABSTRACT
    9. Foundations of cyber-physical systems
      ABSTRACT   PDF
    10. Foundations of cyber-physical systems
      ABSTRACT   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
      ABSTRACT   PDF
    12. Logic & proofs for cyber-physical systems
      IJCAR
      ABSTRACT   PDF   Slides
    13. ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   PDF
    14. Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      in ,
      ABSTRACT
    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
      ABSTRACT
    16. The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving
      3rd workshop on formal integrated development environment
      ABSTRACT   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
      ABSTRACT   PDF
    2. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking differential invariance of algebraic sets
      VMCAI
      ABSTRACT   PDF   Slides
    3. A uniform substitution calculus for differential dynamic logic
      CADE
      ABSTRACT   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
      ABSTRACT
    5. Differential game logic
      ABSTRACT   PDF
    6. Annika Peterson
      Formal verification of a controlled flight between two robots: A case study
      ABSTRACT   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
      ABSTRACT   PDF
    8. Nikos Arechiga James Kapinski Jyotirmoy V. Deshmukh André Platzer Bruce H. Krogh
      Forward invariant cuts to simplify proofs of safety
      EMSOFT
      ABSTRACT
    9. How to prove hybrid systems and why that matters
      ICCSE
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    11. Stefan Mitsch André Platzer Werner Retschitzegger Wieland Schwinger
      Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems
      ABSTRACT   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
    13. Regression verification for programmable logic controller software
      ABSTRACT
    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
      ABSTRACT
    15. Regression verification for programmable logic controller software
      Thesis
      ABSTRACT
    16. Verified traffic networks: Component-based verification of cyber-physical flow systems
      ITSC
      ABSTRACT   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
      ABSTRACT   PDF
    2. Analog and hybrid computation: Dynamical systems and programming languages
      ABSTRACT   PDF Preprint
    3. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      TACAS
      ABSTRACT   PDF   Slides
    4. Stefan Mitsch Grant Olney Passmore André Platzer
      Collaborative verification-driven engineering of hybrid systems
      ABSTRACT   PDF
    5. Differential hybrid games
      ABSTRACT   PDF
    6. Jean-Baptiste Jeannin André Platzer
      dTL^2: Differential temporal dynamic logic with nested temporalities for hybrid systems
      IJCAR
      ABSTRACT   PDF   Slides
    7. Foundations of cyber-physical systems
      ABSTRACT   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
      ABSTRACT   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
      ABSTRACT   PDF
    10. Khalil Ghorbal Andrew Sogokon André Platzer
      Invariance of conjunctions of polynomial equalities for algebraic differential equations
      SAS
      ABSTRACT   PDF   Slides
    11. ModelPlex: Verified runtime validation of verified cyber-physical system models
      RV
      ABSTRACT   PDF   Slides
    12. ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   PDF
    13. Stefan Mitsch Jan-David Quesel André Platzer
      Refactoring, refinement, and reasoning: A logical characterization for hybrid systems
      FM
      ABSTRACT   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
      ABSTRACT
    15. Sarah M. Loos André Platzer
      Teaching cyber-physical systems with logic
      ABSTRACT   PDF

    2013

    1. A complete axiomatization for differential game logic for hybrid games
      ABSTRACT   PDF   Slides
    2. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      IJCAI
      ABSTRACT   PDF Preprint
    3. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      ABSTRACT   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
      ABSTRACT   PDF Preprint
    5. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    7. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      ABSTRACT   PDF
    8. Sarah M. Loos David Witmer Peter Steenkiste André Platzer
      Efficiency analysis of formally verified adaptive cruise controllers
      ITSC
      ABSTRACT   PDF   Slides
    9. Yanni Kouskoulas André Platzer Peter Kazanzides
      Formal methods for robotic system control software
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    11. Foundations of cyber-physical systems
      ABSTRACT   PDF
    12. On provably safe obstacle avoidance for autonomous robotic ground vehicles
      Robotics: Science and systems
      ABSTRACT   PDF   Slides
    13. Teaching CPS foundations with contracts
      CPS-ed
      ABSTRACT   PDF   Slides Preprint

    2012

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

    2011

    1. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      FM
      ABSTRACT   PDF   Slides
    2. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      ABSTRACT   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
      ABSTRACT   PDF Preprint
    4. David W. Renshaw André Platzer
      Differential invariants and symbolic integration for distributed hybrid systems
      ABSTRACT   PDF
    5. David W. Renshaw Sarah M. Loos André Platzer
      Distributed theorem proving for distributed hybrid systems
      ICFEM
      ABSTRACT   PDF
    6. Logic and compositional verification of hybrid systems (invited tutorial)
      CAV
      ABSTRACT   PDF   Slides
    7. Quantified differential invariants
      HSCC
      ABSTRACT   PDF   Slides
    8. Sicun Gao André Platzer Edmund M. Clarke
      Quantifier elimination over finite fields with Gröbner bases
      CAI
      ABSTRACT   PDF
    9. Sarah M. Loos André Platzer
      Safe intersections: At the crossing of hybrid systems and verification
      ITSC
      ABSTRACT   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
      ABSTRACT   PDF   Slides
    11. Stochastic differential dynamic logic for stochastic hybrid programs
      CADE
      ABSTRACT   PDF   Slides
    12. Stochastic differential dynamic logic for stochastic hybrid systems
      ABSTRACT   PDF
    13. The complete proof theory of hybrid systems
      ABSTRACT   PDF
    14. The structure of differential invariants and differential cut elimination
      ABSTRACT   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
      ABSTRACT   PDF

    2010

    1. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      HSCC
      ABSTRACT   PDF   Slides
    2. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification.
      ABSTRACT   PDF
    3. Differential dynamic logics: Automated theorem proving for hybrid systems
      ABSTRACT
    4. Differential-algebraic dynamic logic for differential-algebraic programs
      ABSTRACT   PDF
    5. Logical analysis of hybrid systems: Proving theorems for complex dynamics
      Springer. in , Springer Heidelberg
      ABSTRACT
    6. Quantified differential dynamic logic for distributed hybrid systems
      CSL
      ABSTRACT   PDF   Slides
    7. Quantified differential dynamic logic for distributed hybrid systems
      ABSTRACT   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   PDF
    2. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT   PDF
    3. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      ICFEM
      ABSTRACT   PDF   Slides
    4. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      Thesis
      ABSTRACT   PDF
    5. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      FM
      ABSTRACT   PDF   Slides
    6. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      ABSTRACT   PDF
    7. Real world verification
      CADE
      ABSTRACT   PDF   Slides
    8. Real world verification
      Thesis
      ABSTRACT   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
      ABSTRACT   PDF
    10. Verification of cyberphysical transportation systems
      ABSTRACT

    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   PDF
    2. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      CAV
      ABSTRACT   PDF   Slides
    3. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT   PDF
    4. Differential dynamic logic for hybrid systems.
      ABSTRACT   PDF
    5. Differential dynamic logics: Automated theorem proving for hybrid systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides
    6. Differential dynamic logics. Automated theorem proving for hybrid systems
      Proceedings des gemeinsamen workshops der graduiertenkollegs 2008, dagstuhl
      ABSTRACT
    7. André Platzer Jan-David Quesel
      KeYmaera: A hybrid theorem prover for hybrid systems.
      IJCAR
      ABSTRACT   PDF   Slides
    8. André Platzer Jan-David Quesel
      Logical verification and systematic parametric analysis in train control.
      HSCC
      ABSTRACT   PDF

    2007

    1. A temporal dynamic logic for verifying hybrid system invariants
      LFCS
      ABSTRACT   PDF   Slides
    2. A temporal dynamic logic for verifying hybrid system invariants
      Thesis
      ABSTRACT   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   PDF
    4. Combining deduction and algebraic constraints for hybrid system analysis.
      VERIFY’07 at CADE, bremen, germany
      ABSTRACT   PDF   Slides Preprint
    5. Differential dynamic logic for verifying parametric hybrid systems.
      TABLEAUX
      ABSTRACT   PDF   Slides
    6. Differential dynamic logic for verifying parametric hybrid systems.
      Thesis
      ABSTRACT   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
      ABSTRACT
    8. Differential logic for reasoning about hybrid systems
      HSCC
      ABSTRACT   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   PDF   Slides
    10. André Platzer Edmund M. Clarke
      The image computation problem in hybrid systems model checking
      HSCC
      ABSTRACT   PDF   Slides
    11. Towards a hybrid dynamic logic for hybrid dynamic systems
      ABSTRACT   PDF   Slides

    2006

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

    2004

    1. Using a program verification calculus for constructing specifications from implementations
      ABSTRACT   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
      ABSTRACT   PDF
    2. Deductive verification for ordinary differential equations: Safety, liveness, and stability
      Ph.D. dissertation
      ABSTRACT   PDF
    3. Rose Bohrer
      Practical end-to-end verification of cyber-physical systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides
    4. Nathan Fulton
      Verifiably safe autonomy for cyber-physical systems
      Ph.D. dissertation
      ABSTRACT   PDF
    5. Sarah M. Loos
      Differential refinement logic
      Ph.D. dissertation
      ABSTRACT   PDF   Slides
    6. Regression verification for programmable logic controller software
      Thesis
      ABSTRACT
    7. Algorithms for Forbidden Pattern Recognition in Transition Diagrams
      Thesis
      ABSTRACT
    8. Differential dynamic logics: Automated theorem proving for hybrid systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides

    report

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

    paper-conference

    1. Enguerrand Prebet André Platzer
      Uniform substitution for differential refinement logic
      IJCAR
      ABSTRACT
    2. Noah Abou El Wafa André Platzer
      Complete game logic with sabotage
      LICS
      ABSTRACT
    3. CESAR: Control envelope synthesis via angelic refinements
      TACAS
      ABSTRACT   Slides
    4. Uniform substitution for dynamic logic with communicating hybrid programs
      CADE
      ABSTRACT   Slides
    5. Refinements of hybrid dynamical systems logic
      Rigorous state-based methods - 9th international conference, ABZ 2023, nancy, france, proceedings
      ABSTRACT   Slides
    6. 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
      ABSTRACT
    7. Verifying switched system stability with logic
      HSCC ’22: 25th ACM international conference on hybrid systems: Computation and control, milan, italy, may 4 - 6, 2022
      ABSTRACT   Slides
    8. Learning to find proofs and theorems by learning to refine search strategies
      Advances in neural information processing systems
      ABSTRACT   Slides
    9. Implicit definitions with differential equations for KeYmaera X - (system description)
      IJCAR
      ABSTRACT   Slides
    10. Matias Scharager Katherine Cordwell Stefan Mitsch André Platzer
      Verified quadratic virtual substitution for real arithmetic
      FM
      ABSTRACT   PDF   Slides
    11. Switched systems as hybrid programs
      7th IFAC conference on analysis and design of hybrid systems, ADHS 2021, brussels, belgium, july 7-9, 2021
      ABSTRACT
    12. Runtime verification of generalized test tables
      NASA formal methods - 13th international symposium, NFM 2021, virtual event, may 24-28, 2021, proceedings
      ABSTRACT
    13. 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
      ABSTRACT   PDF   Slides
    14. 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
      ABSTRACT   PDF   Slides
    15. The KeY Approach on Hagrid
      VerifyThis long-term challenge: proceedings
      ABSTRACT
    16. 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
      ABSTRACT
    17. 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
      ABSTRACT   PDF   Slides
    18. 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
      ABSTRACT
    19. Brandon Bohrer André Platzer
      Constructive hybrid games
      IJCAR
      ABSTRACT   PDF   Slides
    20. 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
      ABSTRACT   PDF   Slides
    21. Nathan Fulton André Platzer
      Verifiably safe off-model reinforcement learning
      TACAS
      ABSTRACT   PDF
    22. Uniform substitution at one fell swoop
      CADE
      ABSTRACT   PDF   Slides
    23. Katherine Cordwell André Platzer
      Towards physical hybrid systems
      CADE
      ABSTRACT   PDF   Slides
    24. The logical path to autonomous cyber-physical systems
      QEST
      ABSTRACT   PDF   Slides
    25. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: A framework for sound continuous invariant generation
      FM
      ABSTRACT   PDF   Slides
    26. 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
      ABSTRACT
    27. HyPLC: Hybrid programmable logic controller program translation for verification
      ICCPS
      ABSTRACT   PDF
    28. João Martins André Platzer João Leite
      Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems
      TABLEAUX
      ABSTRACT   PDF   Slides
    29. Brandon Bohrer Manuel Fernández André Platzer
      dL_\iota: Definite descriptions in differential dynamic logic
      CADE
      ABSTRACT   PDF   Slides
    30. An axiomatic approach to liveness for differential equations
      FM
      ABSTRACT   PDF   Slides
    31. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Magnus O. Myreen André Platzer
      VeriPhy: Verified controller executables from verified cyber-physical system models
      PLDI
      ABSTRACT   PDF   Slides
    32. Andrew Sogokon Khalil Ghorbal Yong Kiam Tan André Platzer
      Vector barrier certificates and comparison systems
      FM
      ABSTRACT   PDF   Slides
    33. Uniform substitution for differential game logic
      IJCAR
      ABSTRACT   PDF   Slides
    34. 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.
      ABSTRACT   PDF   Slides Preprint
    35. Nathan Fulton André Platzer
      Safe AI for CPS
      IEEE international test conference, ITC 2018, phoenix, AZ, USA, october 29 - nov. 1, 2018
      ABSTRACT   PDF   Slides
    36. 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
      ABSTRACT
    37. 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
      ABSTRACT
    38. Differential equation axiomatization: The impressive power of differential ghosts
      LICS
      ABSTRACT   PDF   Slides
    39. 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
      ABSTRACT   PDF   Slides
    40. 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)
      ABSTRACT
    41. 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
      ABSTRACT
    42. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      LICS
      ABSTRACT   PDF   Slides
    43. 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
      ABSTRACT   PDF
    44. 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
      ABSTRACT
    45. 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
      ABSTRACT
    46. 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
      ABSTRACT
    47. 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
      ABSTRACT   PDF   Slides
    48. Stefan Mitsch Marco Gario Christof J. Budnik Michael Golm André Platzer
      Formal verification of train control with air pressure brakes
      RSSRail
      ABSTRACT   PDF   Slides
    49. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Change and delay contracts for hybrid system component verification
      FASE
      ABSTRACT   PDF   Slides
    50. Nathan Fulton Stefan Mitsch Brandon Bohrer André Platzer
      Bellerophon: Tactical theorem proving for hybrid systems
      ITP
      ABSTRACT   PDF   Slides
    51. The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving
      3rd workshop on formal integrated development environment
      ABSTRACT   PDF
    52. 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
      ABSTRACT
    53. Logic & proofs for cyber-physical systems
      IJCAR
      ABSTRACT   PDF   Slides
    54. 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
      ABSTRACT
    55. Sarah M. Loos André Platzer
      Differential refinement logic
      LICS
      ABSTRACT   PDF   Slides
    56. A verification-supported evolution approach to assist software application engineers in industrial factory automation
      IEEE international symposium on assembly and manufacturing (ISAM 2016)
      ABSTRACT
    57. Andrew Sogokon Khalil Ghorbal Paul B. Jackson André Platzer
      A method for invariant generation for polynomial continuous systems
      VMCAI
      ABSTRACT   PDF   Slides
    58. 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
      ABSTRACT   PDF   Slides
    59. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      A component-based approach to hybrid systems safety verification
      IFM
      ABSTRACT   PDF   Slides
    60. Verified traffic networks: Component-based verification of cyber-physical flow systems
      ITSC
      ABSTRACT   PDF   Slides
    61. 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
      ABSTRACT
    62. 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
    63. Nathan Fulton Stefan Mitsch Jan-David Quesel Marcus Völp André Platzer
      KeYmaera X: An axiomatic tactical theorem prover for hybrid systems
      CADE
      ABSTRACT   PDF   Slides
    64. How to prove hybrid systems and why that matters
      ICCSE
      ABSTRACT   PDF
    65. Nikos Arechiga James Kapinski Jyotirmoy V. Deshmukh André Platzer Bruce H. Krogh
      Forward invariant cuts to simplify proofs of safety
      EMSOFT
      ABSTRACT
    66. 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
      ABSTRACT   PDF
    67. A uniform substitution calculus for differential dynamic logic
      CADE
      ABSTRACT   PDF   Slides Preprint
    68. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking differential invariance of algebraic sets
      VMCAI
      ABSTRACT   PDF   Slides
    69. 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
      ABSTRACT   PDF
    70. Stefan Mitsch Jan-David Quesel André Platzer
      Refactoring, refinement, and reasoning: A logical characterization for hybrid systems
      FM
      ABSTRACT   PDF   Slides
    71. ModelPlex: Verified runtime validation of verified cyber-physical system models
      RV
      ABSTRACT   PDF   Slides
    72. Khalil Ghorbal Andrew Sogokon André Platzer
      Invariance of conjunctions of polynomial equalities for algebraic differential equations
      SAS
      ABSTRACT   PDF   Slides
    73. Stefan Mitsch Jan-David Quesel André Platzer
      From safety to guilty & from liveness to niceness
      5th workshop on formal methods for robotics and automation
      ABSTRACT   PDF
    74. Jean-Baptiste Jeannin André Platzer
      dTL^2: Differential temporal dynamic logic with nested temporalities for hybrid systems
      IJCAR
      ABSTRACT   PDF   Slides
    75. Khalil Ghorbal André Platzer
      Characterizing algebraic invariants by differential radical invariants
      TACAS
      ABSTRACT   PDF   Slides
    76. Teaching CPS foundations with contracts
      CPS-ed
      ABSTRACT   PDF   Slides Preprint
    77. On provably safe obstacle avoidance for autonomous robotic ground vehicles
      Robotics: Science and systems
      ABSTRACT   PDF   Slides
    78. 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
      ABSTRACT   PDF   Slides
    79. Sarah M. Loos David Witmer Peter Steenkiste André Platzer
      Efficiency analysis of formally verified adaptive cruise controllers
      ITSC
      ABSTRACT   PDF   Slides
    80. 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
      ABSTRACT   PDF   Slides
    81. 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
      ABSTRACT   PDF Preprint
    82. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      IJCAI
      ABSTRACT   PDF Preprint
    83. Nikos Aréchiga Sarah M. Loos André Platzer Bruce H. Krogh
      Using theorem provers to guarantee closed-loop system properties
      ACC
      ABSTRACT   PDF
    84. Towards formal verification of freeway traffic control
      ICCPS
      ABSTRACT   PDF   Slides
    85. The complete proof theory of hybrid systems
      LICS
      ABSTRACT   PDF   Slides
    86. David Henriques João G. Martins Paolo Zuliani André Platzer Edmund M. Clarke
      Statistical model checking for Markov decision processes
      QEST
      ABSTRACT   PDF   Slides
    87. Jan-David Quesel André Platzer
      Playing hybrid games with KeYmaera
      IJCAR
      ABSTRACT   PDF   Slides
    88. Logics of dynamical systems
      LICS
      ABSTRACT   PDF   Slides
    89. Logical analysis of hybrid systems: A complete answer to a complexity challenge
      DCFS
      ABSTRACT   PDF
    90. A differential operator approach to equational differential invariants
      ITP
      ABSTRACT   PDF   Slides
    91. 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
      ABSTRACT   PDF
    92. Stochastic differential dynamic logic for stochastic hybrid programs
      CADE
      ABSTRACT   PDF   Slides
    93. João Martins André Platzer João Leite
      Statistical model checking for distributed probabilistic-control hybrid automata with smart grid applications
      ICFEM
      ABSTRACT   PDF   Slides
    94. Sarah M. Loos André Platzer
      Safe intersections: At the crossing of hybrid systems and verification
      ITSC
      ABSTRACT   PDF   Slides
    95. Sicun Gao André Platzer Edmund M. Clarke
      Quantifier elimination over finite fields with Gröbner bases
      CAI
      ABSTRACT   PDF
    96. Quantified differential invariants
      HSCC
      ABSTRACT   PDF   Slides
    97. Logic and compositional verification of hybrid systems (invited tutorial)
      CAV
      ABSTRACT   PDF   Slides
    98. David W. Renshaw Sarah M. Loos André Platzer
      Distributed theorem proving for distributed hybrid systems
      ICFEM
      ABSTRACT   PDF
    99. 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
      ABSTRACT   PDF Preprint
    100. Sarah M. Loos André Platzer Ligia Nistor
      Adaptive cruise control: Hybrid, distributed, and now formally verified
      FM
      ABSTRACT   PDF   Slides
    101. Quantified differential dynamic logic for distributed hybrid systems
      CSL
      ABSTRACT   PDF   Slides
    102. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      HSCC
      ABSTRACT   PDF   Slides
    103. Real world verification
      CADE
      ABSTRACT   PDF   Slides
    104. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      FM
      ABSTRACT   PDF   Slides
    105. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      ICFEM
      ABSTRACT   PDF   Slides
    106. Sumit Kumar Jha Edmund Clarke Christopher Langmead Axel Legay André Platzer Paolo Zuliani
      A Bayesian approach to model checking biological systems
      CMSB
      ABSTRACT   PDF
    107. André Platzer Jan-David Quesel
      Logical verification and systematic parametric analysis in train control.
      HSCC
      ABSTRACT   PDF
    108. André Platzer Jan-David Quesel
      KeYmaera: A hybrid theorem prover for hybrid systems.
      IJCAR
      ABSTRACT   PDF   Slides
    109. Differential dynamic logics. Automated theorem proving for hybrid systems
      Proceedings des gemeinsamen workshops der graduiertenkollegs 2008, dagstuhl
      ABSTRACT
    110. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      CAV
      ABSTRACT   PDF   Slides
    111. 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   PDF
    112. André Platzer Edmund M. Clarke
      The image computation problem in hybrid systems model checking
      HSCC
      ABSTRACT   PDF   Slides
    113. 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   PDF   Slides
    114. Differential logic for reasoning about hybrid systems
      HSCC
      ABSTRACT   PDF
    115. 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
      ABSTRACT
    116. Differential dynamic logic for verifying parametric hybrid systems.
      TABLEAUX
      ABSTRACT   PDF   Slides
    117. Combining deduction and algebraic constraints for hybrid system analysis.
      VERIFY’07 at CADE, bremen, germany
      ABSTRACT   PDF   Slides Preprint
    118. 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   PDF
    119. A temporal dynamic logic for verifying hybrid system invariants
      LFCS
      ABSTRACT   PDF   Slides
    120. Dynamic logic with non-rigid functions: A basis for object-oriented program verification.
      IJCAR
      ABSTRACT   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
      ABSTRACT
    2. Sarah M. Loos André Platzer
      Teaching cyber-physical systems with logic
      ABSTRACT   PDF

    chapter

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

    book

    1. The 28th international conference on automated deduction
      Springer. in , Springer
      ABSTRACT
    2. VerifyThis long-term challenge: proceedings
      in , Karlsruhe
      ABSTRACT
    3. 17th IEEE international conference on industrial informatics, INDIN 2019, helsinki, finland, july 22-25, 2019
      IEEE. in , IEEE
      ABSTRACT
    4. Verified software. Theories, tools, and experiments - 10th international conference, VSTTE 2018, oxford, UK, july 18-19, 2018, revised selected papers
      Springer. in , Springer
      ABSTRACT
    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 ,
      ABSTRACT
    6. Logical foundations of cyber-physical systems
      Springer. in , Springer Cham
      ABSTRACT   Slides
    7. 15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      IEEE. in , IEEE
      ABSTRACT
    8. Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      in ,
      ABSTRACT
    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
      ABSTRACT
    10. Logical analysis of hybrid systems: Proving theorems for complex dynamics
      Springer. in , Springer Heidelberg
      ABSTRACT

    article-journal

    1. Rachel Cleaveland Stefan Mitsch André Platzer
      Formally verified next-generation airborne collision avoidance games in ACAS X
      ABSTRACT
    2. William Simmons André Platzer
      Differential elimination and algebraic invariants of polynomial dynamical systems
      ABSTRACT
    3. Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces
      ABSTRACT   Slides
    4. Qin Lin Stefan Mitsch André Platzer John M. Dolan
      Safe and resilient practical waypoint-following for autonomous vehicles
      ABSTRACT   PDF
    5. Andrew Sogokon Stefan Mitsch Yong Kiam Tan Katherine Cordwell André Platzer
      Pegasus: Sound continuous invariant generation
      ABSTRACT   PDF
    6. Noah Abou El Wafa André Platzer
      First-order game logic and modal mu-calculus
      ABSTRACT
    7. Brandon Bohrer André Platzer
      Structured proofs for adversarial cyber-physical systems
      ABSTRACT   PDF
    8. An axiomatic approach to existence and liveness for differential equations
      ABSTRACT   PDF
    9. Differential equation invariance axiomatization
      ABSTRACT   PDF   Slides
    10. Uniform substitution at one fell swoop
      ABSTRACT
    11. Relational test tables: A practical specification language for evolution and security
      ABSTRACT Preprint
    12. Overview of logical foundations of cyber-physical systems
      ABSTRACT Preprint
    13. Differential equation invariance axiomatization
      ABSTRACT Preprint
    14. Brandon Bohrer Yong Kiam Tan Stefan Mitsch Andrew Sogokon André Platzer
      A formal safety net for waypoint following in ground robots
      ABSTRACT
    15. Verified runtime validation for partially observable hybrid systems
      ABSTRACT
    16. Andreas Müller Stefan Mitsch Werner Retschitzegger Wieland Schwinger André Platzer
      Tactical contract composition for hybrid system component verification
      ABSTRACT   PDF
    17. Relational equivalence proofs between imperative and MapReduce algorithms
      ABSTRACT Preprint
    18. Debugging program verification proof scripts (tool paper)
      ABSTRACT Preprint
    19. Applicability of generalized test tables: A case study using the manufacturing system demonstrator xPPU
      ABSTRACT
    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
      ABSTRACT   PDF
    21. Stefan Mitsch Khalil Ghorbal David Vogelbacher André Platzer
      Formal verification of obstacle avoidance and navigation of ground robots
      ABSTRACT   PDF
    22. Differential hybrid games
      ABSTRACT   PDF
    23. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
      ABSTRACT   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
      ABSTRACT   PDF
    25. A complete uniform substitution calculus for differential dynamic logic
      ABSTRACT   PDF
    26. ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   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
      ABSTRACT   PDF
    28. Stefan Mitsch André Platzer Werner Retschitzegger Wieland Schwinger
      Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems
      ABSTRACT   PDF
    29. Differential game logic
      ABSTRACT   PDF
    30. Akshay Rajhans Ajinkya Bhave Ivan Ruchkin Bruce H. Krogh David Garlan André Platzer Bradley Schmerl
      Supporting heterogeneity in cyber-physical systems architectures
      ABSTRACT
    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
      ABSTRACT   PDF
    32. Stefan Mitsch Grant Olney Passmore André Platzer
      Collaborative verification-driven engineering of hybrid systems
      ABSTRACT   PDF
    33. Analog and hybrid computation: Dynamical systems and programming languages
      ABSTRACT   PDF Preprint
    34. Yanni Kouskoulas André Platzer Peter Kazanzides
      Formal methods for robotic system control software
      ABSTRACT   PDF Preprint
    35. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      ABSTRACT   PDF
    36. The structure of differential invariants and differential cut elimination
      ABSTRACT   PDF
    37. Logical analysis of hybrid systems: A complete answer to a complexity challenge
      ABSTRACT   PDF
    38. Dynamic logics of dynamical systems
      ABSTRACT
    39. A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems
      ABSTRACT   PDF
    40. Differential-algebraic dynamic logic for differential-algebraic programs
      ABSTRACT   PDF
    41. Differential dynamic logics: Automated theorem proving for hybrid systems
      ABSTRACT
    42. Verification of cyberphysical transportation systems
      ABSTRACT
    43. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT   PDF
    44. Differential dynamic logic for hybrid systems.
      ABSTRACT   PDF
    45. Towards a hybrid dynamic logic for hybrid dynamic systems
      ABSTRACT   PDF   Slides

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