André Platzer

According to our database1, André Platzer authored at least 127 papers between 2006 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2020
Differential Equation Invariance Axiomatization.
J. ACM, 2020

Pegasus: Sound Continuous Invariant Generation.
CoRR, 2020

An Axiomatic Approach to Existence and Liveness for Differential Equations.
CoRR, 2020

Refining Constructive Hybrid Games.
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Constructive Game Logic.
Proceedings of the Programming Languages and Systems, 2020

Constructive Hybrid Games.
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
A Formal Safety Net for Waypoint-Following in Ground Robots.
IEEE Robotics Autom. Lett., 2019

Overview of Logical Foundations of Cyber-Physical Systems.
CoRR, 2019

Toward Structured Proofs for Dynamic Logics.
CoRR, 2019

Verifiably Safe Off-Model Reinforcement Learning.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

The Logical Path to Autonomous Cyber-Physical Systems.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

Toward multi-task support and security analyses in PLC program translation for verification: poster abstract.
Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, 2019

HyPLC: hybrid programmable logic controller program translation for verification.
Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, 2019

An Axiomatic Approach to Liveness for Differential Equations.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Pegasus: A Framework for Sound Continuous Invariant Generation.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Verifiably safe SCUBA diving using commodity sensors: work-in-progress.
Proceedings of the International Conference on Embedded Software Companion, 2019

Uniform Substitution at One Fell Swoop.
Proceedings of the Automated Deduction - CADE 27, 2019

Towards Physical Hybrid Systems.
Proceedings of the Automated Deduction - CADE 27, 2019

dL<sub>ι</sub>: Definite Descriptions in Differential Dynamic Logic.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
Verification of Hybrid Systems.
Proceedings of the Handbook of Model Checking., 2018

Tactical contract composition for hybrid system component verification.
Int. J. Softw. Tools Technol. Transf., 2018

Verified Runtime Validation for Partially Observable Hybrid Systems.
CoRR, 2018

VeriPhy: verified controller executables from verified cyber-physical system models.
Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Safe AI for CPS (Invited Paper).
Proceedings of the IEEE International Test Conference, 2018

Vector Barrier Certificates and Comparison Systems.
Proceedings of the Formal Methods - 22nd International Symposium, 2018

A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration).
Proceedings of the Cyber Physical Systems. Model-Based Design - 8th International Workshop, 2018

Uniform Substitution for Differential Game Logic.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving.
Proceedings of the ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2018

CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation.
Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 2018

Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning.
Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

Logical Foundations of Cyber-Physical Systems
Springer, ISBN: 978-3-319-63587-3, 2018

2017
Differential Hybrid Games.
ACM Trans. Comput. Log., 2017

A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system.
Int. J. Softw. Tools Technol. Transf., 2017

A Complete Uniform Substitution Calculus for Differential Dynamic Logic.
J. Autom. Reasoning, 2017

Formal verification of obstacle avoidance and navigation of ground robots.
I. J. Robotics Res., 2017

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets.
Comput. Lang. Syst. Struct., 2017

Formal Verification of Train Control with Air Pressure Brakes.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2017

Bellerophon: Tactical Theorem Proving for Hybrid Systems.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Change and Delay Contracts for Hybrid System Component Verification.
Proceedings of the Fundamental Approaches to Software Engineering, 2017

A Benchmark for Component-based Hybrid Systems Safety Verification.
Proceedings of the ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2017

Formally verified differential dynamic logic.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016
How to model and prove hybrid systems with KeYmaera: a tutorial on safety.
Int. J. Softw. Tools Technol. Transf., 2016

ModelPlex: verified runtime validation of verified cyber-physical system models.
Formal Methods Syst. Des., 2016

The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving.
Proceedings of the Third Workshop on Formal Integrated Development Environment, 2016

A Method for Invariant Generation for Polynomial Continuous Systems.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Keynote talk I: How to prove hybrid systems.
Proceedings of the 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, 2016

Differential Refinement Logic.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

A Component-Based Approach to Hybrid Systems Safety Verification.
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logics.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Logic & Proofs for Cyber-Physical Systems.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015
Differential Game Logic.
ACM Trans. Comput. Log., 2015

Numerically-aided Deductive Safety Proof for a Powertrain Control System.
Electron. Notes Theor. Comput. Sci., 2015

Logic-Based Modeling Approaches for Qualitative and Hybrid Reasoning in Dynamic Spatial Systems.
ACM Comput. Surv., 2015

A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems.
Proceedings of the IEEE 18th International Conference on Intelligent Transportation Systems, 2015

Proving Hybrid Systems.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Formal verification of ACAS X, an industrial airborne collision avoidance system.
Proceedings of the 2015 International Conference on Embedded Software, 2015

Forward invariant cuts to simplify proofs of safety.
Proceedings of the 2015 International Conference on Embedded Software, 2015

A Uniform Substitution Calculus for Differential Dynamic Logic.
Proceedings of the Automated Deduction - CADE-25, 2015

KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems.
Proceedings of the Automated Deduction - CADE-25, 2015

Ernst-Rüdiger Olderog: A Life for Meaning.
Proceedings of the Correct System Design, 2015

2014
Supporting Heterogeneity in Cyber-Physical Systems Architectures.
IEEE Trans. Autom. Control., 2014

Collaborative Verification-Driven Engineering of Hybrid Systems.
Mathematics in Computer Science, 2014

Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges.
J. Aerosp. Inf. Syst., 2014

Analog and Hybrid Computation: Dynamical Systems and Programming Languages.
Bull. EATCS, 2014

Characterizing Algebraic Invariants by Differential Radical Invariants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations.
Proceedings of the Static Analysis - 21st International Symposium, 2014

Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems.
Proceedings of the FM 2014: Formal Methods, 2014

dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems.
Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013
Bayesian statistical model checking with application to Stateflow/Simulink verification.
Formal Methods Syst. Des., 2013

On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles.
Proceedings of the Robotics: Science and Systems IX, Technische Universität Berlin, Berlin, Germany, June 24, 2013

Efficiency analysis of formally verified adaptive cruise controllers.
Proceedings of the 16th International IEEE Conference on Intelligent Transportation Systems, 2013

A Generalization of SAT and #SAT for Robust Policy Evaluation.
Proceedings of the IJCAI 2013, 2013

Formal verification of distributed aircraft controllers.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
Proceedings of the 16th international conference on Hybrid systems: computation and control, 2013

2012
Logical Analysis of Hybrid Systems: A Answer to a Complexity Challenge.
J. Autom. Lang. Comb., 2012

A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems
Log. Methods Comput. Sci., 2012

Dynamic Logics of Dynamical Systems
CoRR, 2012

Statistical Model Checking for Markov Decision Processes.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

The Complete Proof Theory of Hybrid Systems.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Logics of Dynamical Systems.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

A Differential Operator Approach to Equational Differential Invariants - (Invited Paper).
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Towards Formal Verification of Freeway Traffic Control.
Proceedings of the 2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, 2012

Logical Analysis of Hybrid Systems - A Complete Answer to a Complexity Challenge.
Proceedings of the Descriptional Complexity of Formal Systems, 2012

Playing Hybrid Games with KeYmaera.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Using theorem provers to guarantee closed-loop system properties.
Proceedings of the American Control Conference, 2012

2011
An Instantiation-Based Theorem Prover for First-Order Programming.
Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, 2011

The Structure of Differential Invariants and Differential Cut Elimination
Log. Methods Comput. Sci., 2011

Safe intersections: At the crossing of hybrid systems and verification.
Proceedings of the 14th International IEEE Conference on Intelligent Transportation Systems, 2011

Distributed Theorem Proving for Distributed Hybrid Systems.
Proceedings of the Formal Methods and Software Engineering, 2011

Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications.
Proceedings of the Formal Methods and Software Engineering, 2011

Quantified differential invariants.
Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified.
Proceedings of the FM 2011: Formal Methods, 2011

Using parameters in architectural views to support heterogeneous design and verification.
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial).
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Quantifier Elimination over Finite Fields Using Gröbner Bases.
Proceedings of the Algebraic Informatics - 4th International Conference, 2011

Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
Differential-algebraic Dynamic Logic for Differential-algebraic Programs.
J. Log. Comput., 2010

Differential Dynamic Logics.
Künstliche Intell., 2010

Bayesian statistical model checking with application to Simulink/Stateflow verification.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Quantified Differential Dynamic Logic for Distributed Hybrid Systems.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Real Analysis for Complex Systems.
Proceedings of the 6th International Verification Workshop, 2010

Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics.
Springer, ISBN: 978-3-642-14508-7, 2010

2009
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods Syst. Des., 2009

Verification of Cyberphysical Transportation Systems.
IEEE Intell. Syst., 2009

European Train Control System: A Case Study in Formal Verification.
Proceedings of the Formal Methods and Software Engineering, 2009

Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
Proceedings of the FM 2009: Formal Methods, 2009

A Bayesian Approach to Model Checking Biological Systems.
Proceedings of the Computational Methods in Systems Biology, 7th International Conference, 2009

Real World Verification.
Proceedings of the Automated Deduction, 2009

2008
Differential dynamic logics - automated theorem proving for hybrid systems.
PhD thesis, 2008

Differential Dynamic Logic for Hybrid Systems.
J. Autom. Reasoning, 2008

Logical Verification and Systematic Parametric Analysis in Train Control.
Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Differential Dynamic Logic: Automated Theorem Proving for Hybrid Systems.
Proceedings of the Ausgezeichnete Informatikdissertationen 2008, 2008

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems.
Electron. Notes Theor. Comput. Sci., 2007

SAT-based Abstraction Refinement for Real-time Systems.
Electron. Notes Theor. Comput. Sci., 2007

Differential Dynamic Logic for Verifying Parametric Hybrid Systems.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

The Image Computation Problem in Hybrid Systems Model Checking.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Differential Logic for Reasoning About Hybrid Systems.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Combining Deduction and Algebraic Constraints for Hybrid System Analysis.
Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

Automating Verification of Cooperation, Control, and Design in Traffic Applications.
Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006
Dynamic Logic with Non-rigid Functions.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006


  Loading...