Publications

    Jump to Year:
    ⊙ 2024 ⊙ 2023 ⊙ 2022 ⊙ 2021 ⊙ 2020 ⊙ 2019 ⊙ 2018 ⊙ 2017 ⊙ 2016 ⊙ 2015 ⊙ 2014 ⊙ 2013 ⊙ 2012 ⊙ 2011 ⊙ 2010 ⊙ 2009 ⊙ 2008 ⊙ 2007 ⊙ 2006 ⊙ 2004 ⊙

    2024

    1. Aditi Kabra Jonathan Laurent Stefan Mitsch André Platzer
      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. André Platzer
      Refinements of hybrid dynamical systems logic
      Rigorous state-based methods - 9th international conference, ABZ 2023, nancy, france, proceedings
      ABSTRACT   Slides
    6. Marvin Brieger Stefan Mitsch André Platzer
      Uniform substitution for dynamic logic with communicating hybrid programs
      CADE
      ABSTRACT   Slides

    2022

    1. Yong Kiam Tan
      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. James Gallicchio Yong Kiam Tan Stefan Mitsch André Platzer
      Implicit definitions with differential equations for KeYmaera X - (system description)
      IJCAR
      ABSTRACT   Slides
    5. Jonathan Laurent André Platzer
      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 Field (line: 4188, key: `refname`): `FM'19`
    7. Qin Lin Stefan Mitsch André Platzer John M. Dolan
      Safe and resilient practical waypoint-following for autonomous vehicles
      ABSTRACT   PDF
    8. Aditi Kabra Stefan Mitsch André Platzer
      Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces
      ABSTRACT   Slides
    9. Yong Kiam Tan Stefan Mitsch André Platzer
      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. Yong Kiam Tan André Platzer
      An axiomatic approach to existence and liveness for differential equations
      ABSTRACT   PDF Field (line: 4210, key: `refname`): `FM'19`
    3. Yong Kiam Tan André Platzer
      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 Field (line: 4307, key: `refname`): `TECS'23`
    5. Rose Bohrer
      Practical end-to-end verification of cyber-physical systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides
    6. Alexander Weigl Mattias Ulbrich Shmuel S. Tyszberowicz Jonas Klamroth
      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. Yong Kiam Tan André Platzer
      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. Stefan Mitsch André Platzer
      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. André Platzer Yong Kiam Tan
      Differential equation invariance axiomatization
      ABSTRACT   PDF   Slides
    5. Alexander Weigl Mattias Ulbrich Daniel Lentzsch
      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. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      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. Stijn Gouw Mattias Ulbrich Alexander Weigl
      The KeY Approach on Hagrid
      VerifyThis long-term challenge: proceedings
      ABSTRACT
    10. Marieke Huisman Raúl E. Monti Mattias Ulbrich Alexander Weigl
      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. Yong Kiam Tan André Platzer
      An axiomatic approach to liveness for differential equations
      FM
      ABSTRACT   PDF   Slides Field (line: 3920, key: `refname`): `FAC'21`
    4. André Platzer Yong Kiam Tan
      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 TR
    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. Bernhard Beckert Jakob Mund Mattias Ulbrich Alexander Weigl
      Formal verification of evolutionary changes
      ABSTRACT
    9. Luis Garcia Stefan Mitsch André Platzer
      HyPLC: Hybrid programmable logic controller program translation for verification
      ICCPS
      ABSTRACT   PDF
    10. Alexander Weigl
      KASTEL industry 4.0 demonstrator: Provably forgetting information in PLC software
      ABSTRACT
    11. André Platzer
      KeYmaera X tutorial
      ABSTRACT   PDF
    12. Suhyun Cha Mattias Ulbrich Alexander Weigl Bernhard Beckert Kathrin Land Birgit Vogel-Heuser
      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. André Platzer
      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 Field (line: 3954, key: `refname`): `FMSD`
    15. Alexander Weigl
      Provably forgetting of information in manufacturing systems: Verification of the KASTEL industry demonstrator
      ABSTRACT
    16. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      Relational test tables: A practical specification language for evolution and security
      ABSTRACT Preprint
    17. André Platzer
      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. André Platzer
      Uniform substitution at one fell swoop
      CADE
      ABSTRACT   PDF   Slides
    20. André Platzer
      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 TR
    4. Suhyun Cha Alexander Weigl Mattias Ulbrich Bernhard Beckert Birgit Vogel-Heuser
      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. Suhyun Cha Alexander Weigl Mattias Ulbrich Bernhard Beckert Birgit Vogel-Heuser
      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. Bernhard Beckert Sarah Grebing Alexander Weigl
      Debugging program verification proof scripts (tool paper)
      ABSTRACT Preprint
    9. André Platzer Yong Kiam Tan
      Differential equation axiomatization: The impressive power of differential ghosts
      LICS
      ABSTRACT   PDF   Slides Field (line: 3625, key: `refname`): `JACM'20`
    10. André Platzer
      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. Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl
      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. Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl
      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. Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl
      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 Field (line: 3718, key: `refname`): `FASE'17`
    18. André Platzer
      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. Stefan Mitsch André Platzer
      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. André Platzer
      Videos for logical foundations of cyber-physical systems
      ABSTRACT Field (line: 3511, key: `refname`): `Textbook`

    2017

    1. 15th IEEE international conference on industrial informatics, INDIN 2017, emden, germany, july 24-26, 2017
      IEEE. in , IEEE
      ABSTRACT
    2. André Platzer
      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 Field (line: 3037, key: `refname`): `TACAS'15`
    4. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets
      ABSTRACT   PDF Field (line: 3104, key: `refname`): `VMCAI'15`
    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 Field (line: 3434, key: `refname`): `STTT'18`
    7. André Platzer
      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. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT Field (line: 3393, key: `refname`): `textbook`
    12. Bernhard Beckert Suhyun Cha Mattias Ulbrich Birgit Vogel-Heuser Alexander Weigl
      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. Alexander Weigl Franziska Wiebe Mattias Ulbrich Sebastian Ulewicz Suhyun Cha Michael Kirsten Bernhard Beckert Birgit Vogel-Heuser
      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. Suhyun Cha Sebastian Ulewicz Birgit Vogel-Heuser Alexander Weigl Mattias Ulbrich Bernhard Beckert
      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. André Platzer Yong Kiam Tan
      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 TR
    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. Sebastian Ulewicz Mattias Ulbrich Alexander Weigl Michael Kirsten Franziska Wiebe Bernhard Beckert Birgit Vogel-Heuser
      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. Alexander Weigl
      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. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   PDF Field (line: 3269, key: `refname`): `textbook`
    10. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   Slides Field (line: 3257, key: `refname`): `textbook`
    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. André Platzer
      Logic & proofs for cyber-physical systems
      IJCAR
      ABSTRACT   PDF   Slides
    13. Stefan Mitsch André Platzer
      ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   PDF Field (line: 3124, key: `refname`): `RV'14`
    14. Proceedings 14th international workshop quantitative aspects of programming languages and systems, QAPL 2016, eindhoven, the netherlands, april 2-3, 2016
      in ,
      ABSTRACT
    15. Vladimir Klebanov Alexander Weigl Jörg Weisbarth
      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. Stefan Mitsch André Platzer
      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 Field (line: 2805, key: `refname`): `STTT'17`
    2. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking differential invariance of algebraic sets
      VMCAI
      ABSTRACT   PDF   Slides Field (line: 2717, key: `refname`): `ComLan'17`
    3. André Platzer
      A uniform substitution calculus for differential dynamic logic
      CADE
      ABSTRACT   PDF   Slides Preprint Field (line: 2851, key: `refname`): `JAR'17`
    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. André Platzer
      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. André Platzer
      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. Sebastian Ulewicz Birgit Vogel-Heuser Mattias Ulbrich Alexander Weigl Bernhard Beckert
      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. Bernhard Beckert Mattias Ulbrich Birgit Vogel-Heuser Alexander Weigl
      Regression verification for programmable logic controller software
      ABSTRACT
    14. Bernhard Beckert Mattias Ulbrich Birgit Vogel-Heuser Alexander Weigl
      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. Alexander Sebastian Weigl
      Regression verification for programmable logic controller software
      Thesis
      ABSTRACT
    16. Andreas Müller Stefan Mitsch André Platzer
      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. André Platzer
      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. André Platzer
      Differential hybrid games
      ABSTRACT   PDF TR
    6. Jean-Baptiste Jeannin André Platzer
      dTL^2: Differential temporal dynamic logic with nested temporalities for hybrid systems
      IJCAR
      ABSTRACT   PDF   Slides
    7. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   PDF Field (line: 2773, key: `refname`): `textbook`
    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. Stefan Mitsch André Platzer
      ModelPlex: Verified runtime validation of verified cyber-physical system models
      RV
      ABSTRACT   PDF   Slides Field (line: 2646, key: `refname`): `FMSD'16`
    12. Stefan Mitsch André Platzer
      ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   PDF TR
    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. André Platzer
      A complete axiomatization for differential game logic for hybrid games
      ABSTRACT   PDF   Slides TR
    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 TR
    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 TR
    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. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   PDF Field (line: 2513, key: `refname`): `textbook`
    12. Stefan Mitsch Khalil Ghorbal André Platzer
      On provably safe obstacle avoidance for autonomous robotic ground vehicles
      Robotics: Science and systems
      ABSTRACT   PDF   Slides Field (line: 2284, key: `refname`): `IJRR'17`
    13. André Platzer
      Teaching CPS foundations with contracts
      CPS-ed
      ABSTRACT   PDF   Slides Preprint

    2012

    1. André Platzer
      A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems
      ABSTRACT   PDF Field (line: 1975, key: `refname`): `CSL'10`
    2. André Platzer
      A differential operator approach to equational differential invariants
      ITP
      ABSTRACT   PDF   Slides
    3. Alexander Weigl
      Algorithms for Forbidden Pattern Recognition in Transition Diagrams
      Thesis
      ABSTRACT
    4. André Platzer
      Differential game logic for hybrid games
      ABSTRACT   PDF TR
    5. André Platzer
      Dynamic logics of dynamical systems
      ABSTRACT
    6. André Platzer
      Logical analysis of hybrid systems: A complete answer to a complexity challenge
      DCFS
      ABSTRACT   PDF
    7. André Platzer
      Logical analysis of hybrid systems: A complete answer to a complexity challenge
      ABSTRACT   PDF
    8. André Platzer
      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 TR
    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. André Platzer
      The complete proof theory of hybrid systems
      LICS
      ABSTRACT   PDF   Slides
    13. André Platzer
      The structure of differential invariants and differential cut elimination
      ABSTRACT   PDF
    14. Stefan Mitsch Sarah M. Loos André Platzer
      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 TR
    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. André Platzer
      Logic and compositional verification of hybrid systems (invited tutorial)
      CAV
      ABSTRACT   PDF   Slides
    7. André Platzer
      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. André Platzer
      Stochastic differential dynamic logic for stochastic hybrid programs
      CADE
      ABSTRACT   PDF   Slides
    12. André Platzer
      Stochastic differential dynamic logic for stochastic hybrid systems
      ABSTRACT   PDF TR
    13. André Platzer
      The complete proof theory of hybrid systems
      ABSTRACT   PDF TR
    14. André Platzer
      The structure of differential invariants and differential cut elimination
      ABSTRACT   PDF TR
    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 Field (line: 1726, key: `refname`): `TAC'14`

    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 TR
    3. André Platzer
      Differential dynamic logics: Automated theorem proving for hybrid systems
      ABSTRACT
    4. André Platzer
      Differential-algebraic dynamic logic for differential-algebraic programs
      ABSTRACT   PDF Field (line: 606, key: `refname`): `TABLEAUX'07`
    5. André Platzer
      Logical analysis of hybrid systems: Proving theorems for complex dynamics
      Springer. in , Springer Heidelberg
      ABSTRACT
    6. André Platzer
      Quantified differential dynamic logic for distributed hybrid systems
      CSL
      ABSTRACT   PDF   Slides Field (line: 1306, key: `refname`): `LMCS'12`
    7. André Platzer
      Quantified differential dynamic logic for distributed hybrid systems
      ABSTRACT   PDF TR

    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 Field (line: 834, key: `refname`): `CAV'08`
    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 TR
    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 TR
    7. André Platzer Jan-David Quesel Philipp Rümmer
      Real world verification
      CADE
      ABSTRACT   PDF   Slides
    8. André Platzer Jan-David Quesel Philipp Rümmer
      Real world verification
      Thesis
      ABSTRACT   PDF TR
    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 TR
    10. André Platzer
      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 Field (line: 688, key: `refname`): `FMSD'09`
    3. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT   PDF TR
    4. André Platzer
      Differential dynamic logic for hybrid systems.
      ABSTRACT   PDF
    5. André Platzer
      Differential dynamic logics: Automated theorem proving for hybrid systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides Field (line: 790, key: `refname`): `ebook`
    6. André Platzer
      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. André Platzer
      A temporal dynamic logic for verifying hybrid system invariants
      LFCS
      ABSTRACT   PDF   Slides
    2. André Platzer
      A temporal dynamic logic for verifying hybrid system invariants
      Thesis
      ABSTRACT   PDF TR
    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. André Platzer
      Combining deduction and algebraic constraints for hybrid system analysis.
      VERIFY’07 at CADE, bremen, germany
      ABSTRACT   PDF   Slides Preprint
    5. André Platzer
      Differential dynamic logic for verifying parametric hybrid systems.
      TABLEAUX
      ABSTRACT   PDF   Slides
    6. André Platzer
      Differential dynamic logic for verifying parametric hybrid systems.
      Thesis
      ABSTRACT   PDF TR
    7. André Platzer
      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. André Platzer
      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. André Platzer
      Towards a hybrid dynamic logic for hybrid dynamic systems
      ABSTRACT   PDF   Slides

    2006

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

    2004

    1. André Platzer
      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. Yong Kiam Tan
      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. Alexander Sebastian Weigl
      Regression verification for programmable logic controller software
      Thesis
      ABSTRACT
    7. Alexander Weigl
      Algorithms for Forbidden Pattern Recognition in Transition Diagrams
      Thesis
      ABSTRACT
    8. André Platzer
      Differential dynamic logics: Automated theorem proving for hybrid systems
      Ph.D. dissertation
      ABSTRACT   PDF   Slides Field (line: 790, key: `refname`): `ebook`

    report

    1. Alexander Weigl
      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 TR
    3. Brandon Bohrer André Platzer
      A hybrid, dynamic logic for hybrid-dynamic information flow
      ABSTRACT   PDF TR
    4. André Platzer Yong Kiam Tan
      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 TR
    6. Bernhard Beckert Mattias Ulbrich Birgit Vogel-Heuser Alexander Weigl
      Regression verification for programmable logic controller software
      ABSTRACT
    7. Stefan Mitsch André Platzer
      ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   PDF TR
    8. André Platzer
      Differential hybrid games
      ABSTRACT   PDF TR
    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 TR
    11. Erik P. Zawadzki André Platzer Geoffrey J. Gordon
      A generalization of SAT and #SAT for policy evaluation
      ABSTRACT   PDF TR
    12. André Platzer
      A complete axiomatization for differential game logic for hybrid games
      ABSTRACT   PDF   Slides TR
    13. David W. Renshaw Sarah Loos André Platzer
      Mechanized safety proofs for disc-constrained aircraft
      ABSTRACT   PDF TR
    14. André Platzer
      Differential game logic for hybrid games
      ABSTRACT   PDF TR
    15. André Platzer
      The structure of differential invariants and differential cut elimination
      ABSTRACT   PDF TR
    16. André Platzer
      The complete proof theory of hybrid systems
      ABSTRACT   PDF TR
    17. André Platzer
      Stochastic differential dynamic logic for stochastic hybrid systems
      ABSTRACT   PDF TR
    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 TR
    20. André Platzer
      Quantified differential dynamic logic for distributed hybrid systems
      ABSTRACT   PDF TR
    21. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification.
      ABSTRACT   PDF TR
    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 TR
    23. André Platzer Jan-David Quesel Philipp Rümmer
      Real world verification
      Thesis
      ABSTRACT   PDF TR
    24. André Platzer Edmund M. Clarke
      Formal verification of curved flight collision avoidance maneuvers: A case study
      ABSTRACT   PDF TR
    25. André Platzer Jan-David Quesel
      European Train Control System: A case study in formal verification
      Thesis
      ABSTRACT   PDF TR
    26. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT   PDF TR
    27. André Platzer
      Differential dynamic logic for verifying parametric hybrid systems.
      Thesis
      ABSTRACT   PDF TR
    28. André Platzer
      A temporal dynamic logic for verifying hybrid system invariants
      Thesis
      ABSTRACT   PDF TR

    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. Aditi Kabra Jonathan Laurent Stefan Mitsch André Platzer
      CESAR: Control envelope synthesis via angelic refinements
      TACAS
      ABSTRACT   Slides
    4. Marvin Brieger Stefan Mitsch André Platzer
      Uniform substitution for dynamic logic with communicating hybrid programs
      CADE
      ABSTRACT   Slides
    5. André Platzer
      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. Yong Kiam Tan Stefan Mitsch André Platzer
      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. Jonathan Laurent André Platzer
      Learning to find proofs and theorems by learning to refine search strategies
      Advances in neural information processing systems
      ABSTRACT   Slides
    9. James Gallicchio Yong Kiam Tan Stefan Mitsch André Platzer
      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. Yong Kiam Tan André Platzer
      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. Alexander Weigl Mattias Ulbrich Shmuel S. Tyszberowicz Jonas Klamroth
      Runtime verification of generalized test tables
      NASA formal methods - 13th international symposium, NFM 2021, virtual event, may 24-28, 2021, proceedings
      ABSTRACT
    13. Yong Kiam Tan André Platzer
      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. Stijn Gouw Mattias Ulbrich Alexander Weigl
      The KeY Approach on Hagrid
      VerifyThis long-term challenge: proceedings
      ABSTRACT
    16. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      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. Alexander Weigl Mattias Ulbrich Daniel Lentzsch
      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. André Platzer
      Uniform substitution at one fell swoop
      CADE
      ABSTRACT   PDF   Slides
    23. Katherine Cordwell André Platzer
      Towards physical hybrid systems
      CADE
      ABSTRACT   PDF   Slides
    24. André Platzer
      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 Field (line: 3954, key: `refname`): `FMSD`
    26. Suhyun Cha Mattias Ulbrich Alexander Weigl Bernhard Beckert Kathrin Land Birgit Vogel-Heuser
      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. Luis Garcia Stefan Mitsch André Platzer
      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. Yong Kiam Tan André Platzer
      An axiomatic approach to liveness for differential equations
      FM
      ABSTRACT   PDF   Slides Field (line: 3920, key: `refname`): `FAC'21`
    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. André Platzer
      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. Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl
      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. Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl
      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. André Platzer Yong Kiam Tan
      Differential equation axiomatization: The impressive power of differential ghosts
      LICS
      ABSTRACT   PDF   Slides Field (line: 3625, key: `refname`): `JACM'20`
    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. Suhyun Cha Alexander Weigl Mattias Ulbrich Bernhard Beckert Birgit Vogel-Heuser
      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. Suhyun Cha Sebastian Ulewicz Birgit Vogel-Heuser Alexander Weigl Mattias Ulbrich Bernhard Beckert
      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. Alexander Weigl Franziska Wiebe Mattias Ulbrich Sebastian Ulewicz Suhyun Cha Michael Kirsten Bernhard Beckert Birgit Vogel-Heuser
      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. Bernhard Beckert Suhyun Cha Mattias Ulbrich Birgit Vogel-Heuser Alexander Weigl
      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 Field (line: 3434, key: `refname`): `STTT'18`
    50. Nathan Fulton Stefan Mitsch Brandon Bohrer André Platzer
      Bellerophon: Tactical theorem proving for hybrid systems
      ITP
      ABSTRACT   PDF   Slides
    51. Stefan Mitsch André Platzer
      The KeYmaera X proof IDE: Concepts on usability in hybrid systems theorem proving
      3rd workshop on formal integrated development environment
      ABSTRACT   PDF
    52. Vladimir Klebanov Alexander Weigl Jörg Weisbarth
      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. André Platzer
      Logic & proofs for cyber-physical systems
      IJCAR
      ABSTRACT   PDF   Slides
    54. Alexander Weigl
      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. Sebastian Ulewicz Mattias Ulbrich Alexander Weigl Michael Kirsten Franziska Wiebe Bernhard Beckert Birgit Vogel-Heuser
      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. Andreas Müller Stefan Mitsch André Platzer
      Verified traffic networks: Component-based verification of cyber-physical flow systems
      ITSC
      ABSTRACT   PDF   Slides
    61. Bernhard Beckert Mattias Ulbrich Birgit Vogel-Heuser Alexander Weigl
      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. Sebastian Ulewicz Birgit Vogel-Heuser Mattias Ulbrich Alexander Weigl Bernhard Beckert
      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. André Platzer
      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. André Platzer
      A uniform substitution calculus for differential dynamic logic
      CADE
      ABSTRACT   PDF   Slides Preprint Field (line: 2851, key: `refname`): `JAR'17`
    68. Khalil Ghorbal Andrew Sogokon André Platzer
      A hierarchy of proof rules for checking differential invariance of algebraic sets
      VMCAI
      ABSTRACT   PDF   Slides Field (line: 2717, key: `refname`): `ComLan'17`
    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 Field (line: 2805, key: `refname`): `STTT'17`
    70. Stefan Mitsch Jan-David Quesel André Platzer
      Refactoring, refinement, and reasoning: A logical characterization for hybrid systems
      FM
      ABSTRACT   PDF   Slides
    71. Stefan Mitsch André Platzer
      ModelPlex: Verified runtime validation of verified cyber-physical system models
      RV
      ABSTRACT   PDF   Slides Field (line: 2646, key: `refname`): `FMSD'16`
    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. André Platzer
      Teaching CPS foundations with contracts
      CPS-ed
      ABSTRACT   PDF   Slides Preprint
    77. Stefan Mitsch Khalil Ghorbal André Platzer
      On provably safe obstacle avoidance for autonomous robotic ground vehicles
      Robotics: Science and systems
      ABSTRACT   PDF   Slides Field (line: 2284, key: `refname`): `IJRR'17`
    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. Stefan Mitsch Sarah M. Loos André Platzer
      Towards formal verification of freeway traffic control
      ICCPS
      ABSTRACT   PDF   Slides
    85. André Platzer
      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. André Platzer
      Logics of dynamical systems
      LICS
      ABSTRACT   PDF   Slides
    89. André Platzer
      Logical analysis of hybrid systems: A complete answer to a complexity challenge
      DCFS
      ABSTRACT   PDF
    90. André Platzer
      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 Field (line: 1726, key: `refname`): `TAC'14`
    92. André Platzer
      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. André Platzer
      Quantified differential invariants
      HSCC
      ABSTRACT   PDF   Slides
    97. André Platzer
      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. André Platzer
      Quantified differential dynamic logic for distributed hybrid systems
      CSL
      ABSTRACT   PDF   Slides Field (line: 1306, key: `refname`): `LMCS'12`
    102. Paolo Zuliani André Platzer Edmund M. Clarke
      Bayesian statistical model checking with application to Simulink/Stateflow verification
      HSCC
      ABSTRACT   PDF   Slides
    103. André Platzer Jan-David Quesel Philipp Rümmer
      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. André Platzer
      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 Field (line: 688, key: `refname`): `FMSD'09`
    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. André Platzer
      Differential logic for reasoning about hybrid systems
      HSCC
      ABSTRACT   PDF
    115. André Platzer
      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. André Platzer
      Differential dynamic logic for verifying parametric hybrid systems.
      TABLEAUX
      ABSTRACT   PDF   Slides
    117. André Platzer
      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. André Platzer
      A temporal dynamic logic for verifying hybrid system invariants
      LFCS
      ABSTRACT   PDF   Slides
    120. Bernhard Beckert André Platzer
      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. Marieke Huisman Raúl E. Monti Mattias Ulbrich Alexander Weigl
      The VerifyThis Collaborative Long Term Challenge
      ABSTRACT
    2. Stefan Mitsch André Platzer
      A retrospective on developing hybrid systems provers in the KeYmaera family - A tale of three provers
      ABSTRACT   PDF
    3. Bernhard Beckert Jakob Mund Mattias Ulbrich Alexander Weigl
      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. André Platzer
      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. André Platzer
      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. Aditi Kabra Stefan Mitsch André Platzer
      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 Field (line: 4188, key: `refname`): `FM'19`
    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. Yong Kiam Tan André Platzer
      An axiomatic approach to existence and liveness for differential equations
      ABSTRACT   PDF Field (line: 4210, key: `refname`): `FM'19`
    9. André Platzer Yong Kiam Tan
      Differential equation invariance axiomatization
      ABSTRACT   PDF   Slides
    10. André Platzer
      Uniform substitution at one fell swoop
      ABSTRACT
    11. Alexander Weigl Mattias Ulbrich Suhyun Cha Bernhard Beckert Birgit Vogel-Heuser
      Relational test tables: A practical specification language for evolution and security
      ABSTRACT Preprint
    12. André Platzer
      Overview of logical foundations of cyber-physical systems
      ABSTRACT Preprint
    13. André Platzer Yong Kiam Tan
      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. Stefan Mitsch André Platzer
      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 Field (line: 3718, key: `refname`): `FASE'17`
    17. Bernhard Beckert Timo Bingmann Moritz Kiefer Peter Sanders Mattias Ulbrich Alexander Weigl
      Relational equivalence proofs between imperative and MapReduce algorithms
      ABSTRACT Preprint
    18. Bernhard Beckert Sarah Grebing Alexander Weigl
      Debugging program verification proof scripts (tool paper)
      ABSTRACT Preprint
    19. Suhyun Cha Alexander Weigl Mattias Ulbrich Bernhard Beckert Birgit Vogel-Heuser
      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. André Platzer
      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 Field (line: 3104, key: `refname`): `VMCAI'15`
    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 Field (line: 3037, key: `refname`): `TACAS'15`
    25. André Platzer
      A complete uniform substitution calculus for differential dynamic logic
      ABSTRACT   PDF
    26. Stefan Mitsch André Platzer
      ModelPlex: Verified runtime validation of verified cyber-physical system models
      ABSTRACT   PDF Field (line: 3124, key: `refname`): `RV'14`
    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. André Platzer
      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. André Platzer
      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. André Platzer
      The structure of differential invariants and differential cut elimination
      ABSTRACT   PDF
    37. André Platzer
      Logical analysis of hybrid systems: A complete answer to a complexity challenge
      ABSTRACT   PDF
    38. André Platzer
      Dynamic logics of dynamical systems
      ABSTRACT
    39. André Platzer
      A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems
      ABSTRACT   PDF Field (line: 1975, key: `refname`): `CSL'10`
    40. André Platzer
      Differential-algebraic dynamic logic for differential-algebraic programs
      ABSTRACT   PDF Field (line: 606, key: `refname`): `TABLEAUX'07`
    41. André Platzer
      Differential dynamic logics: Automated theorem proving for hybrid systems
      ABSTRACT
    42. André Platzer
      Verification of cyberphysical transportation systems
      ABSTRACT
    43. André Platzer Edmund M. Clarke
      Computing differential invariants of hybrid systems as fixedpoints
      ABSTRACT   PDF Field (line: 834, key: `refname`): `CAV'08`
    44. André Platzer
      Differential dynamic logic for hybrid systems.
      ABSTRACT   PDF
    45. André Platzer
      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 Field (line: 4307, key: `refname`): `TECS'23`
    3. André Platzer
      KeYmaera X tutorial
      ABSTRACT   PDF
    4. Alexander Weigl
      KASTEL industry 4.0 demonstrator: Provably forgetting information in PLC software
      ABSTRACT
    5. André Platzer
      Videos for logical foundations of cyber-physical systems
      ABSTRACT Field (line: 3511, key: `refname`): `Textbook`
    6. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT Field (line: 3393, key: `refname`): `textbook`
    7. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   Slides Field (line: 3257, key: `refname`): `textbook`
    8. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   PDF Field (line: 3269, key: `refname`): `textbook`
    9. Annika Peterson
      Formal verification of a controlled flight between two robots: A case study
      ABSTRACT   PDF
    10. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   PDF Field (line: 2773, key: `refname`): `textbook`
    11. André Platzer
      Foundations of cyber-physical systems
      ABSTRACT   PDF Field (line: 2513, key: `refname`): `textbook`
    12. André Platzer
      Using a program verification calculus for constructing specifications from implementations
      ABSTRACT   PDF   Slides