We stand with Ukraine

We stand with Ukraine

André Platzer

Orcid: 0000-0001-7238-5710

Affiliations:

Karlsruhe Institute of Technology, Germany
Carnegie Mellon University, Computer Science Department, Pittsburgh, PA, USA
Carl von Ossietzky University, Oldenburg, Germany (PhD 2008)

According to our database¹, André Platzer authored at least 160 papers between 2006 and 2025.

Collaborative distances:

Dijkstra number² of three.
Erdős number³ of four.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Links

Online presence:

On csauthors.net:

Bibliography

2025

Hybrid dynamical systems logic and its refinements.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2025

2024

Axiomatization of Compact Initial Value Problems: Open Properties.

[BibT_eX]

[DOI]

,

CoRR, 2024

Complete Dynamic Logic of Communicating Hybrid Programs.

[BibT_eX]

[DOI]

,

,

CoRR, 2024

Provably Safe Neural Network Controllers via Differential Dynamic Logic.

[BibT_eX]

[DOI]

,

,

CoRR, 2024

The Significance of Symbolic Logic for Scientific Education.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods Teaching - 6th Formal Methods Teaching Workshop, 2024

CESAR: Control Envelope Synthesis via Angelic Refinements.

[BibT_eX]

[DOI]

,

Jonathan Laurent

,

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

Complete Game Logic with Sabotage.

[BibT_eX]

[DOI]

Noah Abou El Wafa

,

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

Intersymbolic AI - Interlinking Symbolic AI and Subsymbolic AI.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies, 2024

Uniform Substitution for Differential Refinement Logic.

[BibT_eX]

[DOI]

Enguerrand Prebet

,

Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

2023

Formally Verified Next-generation Airborne Collision Avoidance Games in ACAS X.

[BibT_eX]

[DOI]

Rachel Cleaveland

,

,

ACM Trans. Embed. Comput. Syst., 2023

A Usage-Aware Sequent Calculus for Differential Dynamic Logic.

[BibT_eX]

[DOI]

,

,

CoRR, 2023

Dynamic Logic of Communicating Hybrid Programs.

[BibT_eX]

[DOI]

,

,

CoRR, 2023

Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems.

[BibT_eX]

[DOI]

William Simmons

,

CoRR, 2023

Refinements of Hybrid Dynamical Systems Logic.

[BibT_eX]

[DOI]

Proceedings of the Rigorous State-Based Methods - 9th International Conference, 2023

Theorem Proving and Computer Algebra for Hybrid Systems (Keynote Abstract).

[BibT_eX]

[DOI]

Proceedings of the 8th SC-Square Workshop co-located with the 48th International Symposium on Symbolic and Algebraic Computation, 2023

Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs.

[BibT_eX]

[DOI]

,

,

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Verified Train Controllers for the Federal Railroad Administration Train Kinematics Model: Balancing Competing Brake and Track Forces.

[BibT_eX]

[DOI]

,

,

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022

Correction to: Differential Dynamic Logic for Hybrid Systems.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles.

[BibT_eX]

[DOI]

,

,

,

IEEE Control. Syst. Lett., 2022

Learning to Find Proofs and Theorems by Learning to Refine Search Strategies.

[BibT_eX]

[DOI]

Jonathan Laurent

,

CoRR, 2022

First-Order Game Logic and Modal Mu-Calculus.

[BibT_eX]

[DOI]

Noah Abou El Wafa

,

CoRR, 2022

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.

[BibT_eX]

[DOI]

Katherine Cordwell

,

,

Arch. Formal Proofs, 2022

Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis.

[BibT_eX]

[DOI]

Jonathan Laurent

,

Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022

Verifying Switched System Stability With Logic.

[BibT_eX]

[DOI]

,

,

Proceedings of the HSCC '22: 25th ACM International Conference on Hybrid Systems: Computation and Control, Milan, Italy, May 4, 2022

Implicit Definitions with Differential Equations for KeYmaera X - (System Description).

[BibT_eX]

[DOI]

James Gallicchio

,

,

,

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Structured Proofs for Adversarial Cyber-Physical Systems.

[BibT_eX]

[DOI]

,

ACM Trans. Embed. Comput. Syst., 2021

Correction to: How to model and prove hybrid systems with KeYmaera: a tutorial on safety.

[BibT_eX]

[DOI]

Jan-David Quesel

,

,

,

Nikos Aréchiga

,

Int. J. Softw. Tools Technol. Transf., 2021

Pegasus: sound continuous invariant generation.

[BibT_eX]

[DOI]

,

,

,

Katherine Cordwell

,

Formal Methods Syst. Des., 2021

An axiomatic approach to existence and liveness for differential equations.

[BibT_eX]

[DOI]

,

Formal Aspects Comput., 2021

Verified Quadratic Virtual Substitution for Real Arithmetic.

[BibT_eX]

[DOI]

Matias Scharager

,

Katherine Cordwell

,

,

Arch. Formal Proofs, 2021

The BKR Decision Procedure for Univariate Real Arithmetic.

[BibT_eX]

[DOI]

Katherine Cordwell

,

,

Arch. Formal Proofs, 2021

Deductive Stability Proofs for Ordinary Differential Equations.

[BibT_eX]

[DOI]

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm.

[BibT_eX]

[DOI]

Katherine Cordwell

,

,

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Switched Systems as Hybrid Programs.

[BibT_eX]

[DOI]

,

Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems, 2021

2020

A Retrospective on Developing Hybrid System Provers in the KeYmaera Family - A Tale of Three Provers.

[BibT_eX]

[DOI]

,

Proceedings of the Deductive Software Verification: Future Perspectives, 2020

Differential Equation Invariance Axiomatization.

[BibT_eX]

[DOI]

,

J. ACM, 2020

Refining Constructive Hybrid Games.

[BibT_eX]

[DOI]

,

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Constructive Game Logic.

[BibT_eX]

[DOI]

,

Proceedings of the Programming Languages and Systems, 2020

Constructive Hybrid Games.

[BibT_eX]

[DOI]

,

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

A Formal Safety Net for Waypoint-Following in Ground Robots.

[BibT_eX]

[DOI]

,

,

,

,

IEEE Robotics Autom. Lett., 2019

Overview of Logical Foundations of Cyber-Physical Systems.

[BibT_eX]

[DOI]

CoRR, 2019

Toward Structured Proofs for Dynamic Logics.

[BibT_eX]

[DOI]

,

CoRR, 2019

Differential Game Logic.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2019

Verifiably Safe Off-Model Reinforcement Learning.

[BibT_eX]

[DOI]

,

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.

[BibT_eX]

[DOI]

João G. Martins

,

,

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

The Logical Path to Autonomous Cyber-Physical Systems.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

,

,

Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, 2019

HyPLC: hybrid programmable logic controller program translation for verification.

[BibT_eX]

[DOI]

,

,

Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, 2019

An Axiomatic Approach to Liveness for Differential Equations.

[BibT_eX]

[DOI]

,

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Pegasus: A Framework for Sound Continuous Invariant Generation.

[BibT_eX]

[DOI]

,

,

,

Katherine Cordwell

,

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Verifiably safe SCUBA diving using commodity sensors: work-in-progress.

[BibT_eX]

[DOI]

,

Karim Elmaaroufi

,

,

Proceedings of the International Conference on Embedded Software Companion, 2019

Uniform Substitution at One Fell Swoop.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 27, 2019

Towards Physical Hybrid Systems.

[BibT_eX]

[DOI]

Katherine Cordwell

,

Proceedings of the Automated Deduction - CADE 27, 2019

dL<sub>ι</sub>: Definite Descriptions in Differential Dynamic Logic.

[BibT_eX]

[DOI]

,

Manuel Fernández

,

Proceedings of the Automated Deduction - CADE 27, 2019

2018

Verification of Hybrid Systems.

[BibT_eX]

[DOI]

,

,

George J. Pappas

,

Proceedings of the Handbook of Model Checking., 2018

Tactical contract composition for hybrid system component verification.

[BibT_eX]

[DOI]

Andreas Müller

,

,

Werner Retschitzegger

,

Wieland Schwinger

,

Int. J. Softw. Tools Technol. Transf., 2018

Verified Runtime Validation for Partially Observable Hybrid Systems.

[BibT_eX]

[DOI]

,

CoRR, 2018

VeriPhy: verified controller executables from verified cyber-physical system models.

[BibT_eX]

[DOI]

,

,

,

Magnus O. Myreen

,

Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2018

Differential Equation Axiomatization: The Impressive Power of Differential Ghosts.

[BibT_eX]

[DOI]

,

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.

[BibT_eX]

[DOI]

,

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Safe AI for CPS (Invited Paper).

[BibT_eX]

[DOI]

,

Proceedings of the IEEE International Test Conference, 2018

Vector Barrier Certificates and Comparison Systems.

[BibT_eX]

[DOI]

,

,

,

Proceedings of the Formal Methods - 22nd International Symposium, 2018

A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration).

[BibT_eX]

[DOI]

Andreas Müller

,

,

Wieland Schwinger

,

Proceedings of the Cyber Physical Systems. Model-Based Design - 8th International Workshop, 2018

Uniform Substitution for Differential Game Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving.

[BibT_eX]

[DOI]

,

,

,

,

,

,

,

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.

[BibT_eX]

[DOI]

,

,

,

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.

[BibT_eX]

[DOI]

,

Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, 2018

Logical Foundations of Cyber-Physical Systems

[BibT_eX]

[DOI]

Springer, ISBN: 978-3-319-63587-3, 2018

2017

Differential Hybrid Games.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2017

A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system.

[BibT_eX]

[DOI]

Jean-Baptiste Jeannin

,

,

Yanni Kouskoulas

,

Aurora C. Schmidt

,

Ryan W. Gardner

,

,

Int. J. Softw. Tools Technol. Transf., 2017

A Complete Uniform Substitution Calculus for Differential Dynamic Logic.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Formal verification of obstacle avoidance and navigation of ground robots.

[BibT_eX]

[DOI]

,

,

David Vogelbacher

,

Int. J. Robotics Res., 2017

A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets.

[BibT_eX]

[DOI]

,

,

Comput. Lang. Syst. Struct., 2017

Formal Verification of Train Control with Air Pressure Brakes.

[BibT_eX]

[DOI]

,

,

Christof J. Budnik

,

,

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2017

Bellerophon: Tactical Theorem Proving for Hybrid Systems.

[BibT_eX]

[DOI]

,

,

,

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Change and Delay Contracts for Hybrid System Component Verification.

[BibT_eX]

[DOI]

Andreas Müller

,

,

Werner Retschitzegger

,

Wieland Schwinger

,

Proceedings of the Fundamental Approaches to Software Engineering, 2017

A Benchmark for Component-based Hybrid Systems Safety Verification.

[BibT_eX]

[DOI]

Andreas Müller

,

,

Werner Retschitzegger

,

Wieland Schwinger

,

Proceedings of the ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems, 2017

Formally verified differential dynamic logic.

[BibT_eX]

[DOI]

,

,

,

,

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.

[BibT_eX]

[DOI]

Jan-David Quesel

,

,

,

Nikos Aréchiga

,

Int. J. Softw. Tools Technol. Transf., 2016

ModelPlex: verified runtime validation of verified cyber-physical system models.

[BibT_eX]

[DOI]

,

Formal Methods Syst. Des., 2016

The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving.

[BibT_eX]

[DOI]

,

Proceedings of the Third Workshop on Formal Integrated Development Environment, 2016

A Method for Invariant Generation for Polynomial Continuous Systems.

[BibT_eX]

[DOI]

,

,

Paul B. Jackson

,

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Keynote talk I: How to prove hybrid systems.

[BibT_eX]

[DOI]

Proceedings of the 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, 2016

Differential Refinement Logic.

[BibT_eX]

[DOI]

,

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

A Component-Based Approach to Hybrid Systems Safety Verification.

[BibT_eX]

[DOI]

Andreas Müller

,

,

Werner Retschitzegger

,

Wieland Schwinger

,

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.

[BibT_eX]

[DOI]

,

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Logic & Proofs for Cyber-Physical Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

2015

Logic-Based Modeling Approaches for Qualitative and Hybrid Reasoning in Dynamic Spatial Systems.

[BibT_eX]

[DOI]

,

,

Werner Retschitzegger

,

Wieland Schwinger

ACM Comput. Surv., 2015

A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets.

[BibT_eX]

[DOI]

,

,

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System.

[BibT_eX]

[DOI]

Jean-Baptiste Jeannin

,

,

Yanni Kouskoulas

,

Ryan W. Gardner

,

Aurora C. Schmidt

,

,

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.

[BibT_eX]

[DOI]

Andreas Müller

,

,

Proceedings of the IEEE 18th International Conference on Intelligent Transportation Systems, 2015

Proving Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Formal verification of ACAS X, an industrial airborne collision avoidance system.

[BibT_eX]

[DOI]

Jean-Baptiste Jeannin

,

,

Yanni Kouskoulas

,

Ryan W. Gardner

,

Aurora C. Schmidt

,

,

Proceedings of the 2015 International Conference on Embedded Software, 2015

Forward invariant cuts to simplify proofs of safety.

[BibT_eX]

[DOI]

Nikos Aréchiga

,

,

Jyotirmoy V. Deshmukh

,

,

Proceedings of the 2015 International Conference on Embedded Software, 2015

A Uniform Substitution Calculus for Differential Dynamic Logic.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-25, 2015

KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems.

[BibT_eX]

[DOI]

,

,

Jan-David Quesel

,

,

Proceedings of the Automated Deduction - CADE-25, 2015

Ernst-Rüdiger Olderog: A Life for Meaning.

[BibT_eX]

[DOI]

Proceedings of the Correct System Design, 2015

2014

Supporting Heterogeneity in Cyber-Physical Systems Architectures.

[BibT_eX]

[DOI]

,

,

,

,

,

,

Bradley R. Schmerl

IEEE Trans. Autom. Control., 2014

Collaborative Verification-Driven Engineering of Hybrid Systems.

[BibT_eX]

[DOI]

,

Grant Olney Passmore

,

Math. Comput. Sci., 2014

Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges.

[BibT_eX]

[DOI]

,

Jean-Baptiste Jeannin

,

,

,

Geoffrey J. Gordon

,

J. Aerosp. Inf. Syst., 2014

Numerically-aided Deductive Safety Proof for a Powertrain Control System.

[BibT_eX]

[DOI]

Nikos Aréchiga

,

,

Jyotirmoy V. Deshmukh

,

,

Proceedings of the Seventh and Eighth International Workshops on Numerical Software Verification, 2014

Analog and Hybrid Computation: Dynamical Systems and Programming Languages.

[BibT_eX]

[DOI]

Bull. EATCS, 2014

Characterizing Algebraic Invariants by Differential Radical Invariants.

[BibT_eX]

[DOI]

,

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations.

[BibT_eX]

[DOI]

,

,

Proceedings of the Static Analysis - 21st International Symposium, 2014

Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems.

[BibT_eX]

[DOI]

,

Jan-David Quesel

,

Proceedings of the FM 2014: Formal Methods, 2014

dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems.

[BibT_eX]

[DOI]

Jean-Baptiste Jeannin

,

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Bayesian statistical model checking with application to Stateflow/Simulink verification.

[BibT_eX]

[DOI]

,

,

Edmund M. Clarke

Formal Methods Syst. Des., 2013

On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles.

[BibT_eX]

[DOI]

,

,

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.

[BibT_eX]

[DOI]

,

,

Peter Steenkiste

,

Proceedings of the 16th International IEEE Conference on Intelligent Transportation Systems, 2013

A Generalization of SAT and #SAT for Robust Policy Evaluation.

[BibT_eX]

[DOI]

Erik Peter Zawadzki

,

,

Geoffrey J. Gordon

Proceedings of the IJCAI 2013, 2013

Formal verification of distributed aircraft controllers.

[BibT_eX]

[DOI]

,

David W. Renshaw

,

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.

[BibT_eX]

[DOI]

Yanni Kouskoulas

,

David W. Renshaw

,

,

Peter Kazanzides

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.

[BibT_eX]

[DOI]

J. Autom. Lang. Comb., 2012

A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Dynamic Logics of Dynamical Systems

[BibT_eX]

[DOI]

CoRR, 2012

Statistical Model Checking for Markov Decision Processes.

[BibT_eX]

[DOI]

David Henriques

,

João G. Martins

,

,

,

Edmund M. Clarke

Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

The Complete Proof Theory of Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Logics of Dynamical Systems.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

A Differential Operator Approach to Equational Differential Invariants - (Invited Paper).

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Towards Formal Verification of Freeway Traffic Control.

[BibT_eX]

[DOI]

,

,

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.

[BibT_eX]

[DOI]

Proceedings of the Descriptional Complexity of Formal Systems, 2012

Playing Hybrid Games with KeYmaera.

[BibT_eX]

[DOI]

Jan-David Quesel

,

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Using theorem provers to guarantee closed-loop system properties.

[BibT_eX]

[DOI]

Nikos Aréchiga

,

,

,

Proceedings of the American Control Conference, 2012

2011

An Instantiation-Based Theorem Prover for First-Order Programming.

[BibT_eX]

[DOI]

,

Geoffrey J. Gordon

,

Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, 2011

The Structure of Differential Invariants and Differential Cut Elimination

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

Safe intersections: At the crossing of hybrid systems and verification.

[BibT_eX]

[DOI]

,

Proceedings of the 14th International IEEE Conference on Intelligent Transportation Systems, 2011

Distributed Theorem Proving for Distributed Hybrid Systems.

[BibT_eX]

[DOI]

David W. Renshaw

,

,

Proceedings of the Formal Methods and Software Engineering, 2011

Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications.

[BibT_eX]

[DOI]

João G. Martins

,

,

Proceedings of the Formal Methods and Software Engineering, 2011

Quantified differential invariants.

[BibT_eX]

[DOI]

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

Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified.

[BibT_eX]

[DOI]

,

,

Proceedings of the FM 2011: Formal Methods, 2011

Using parameters in architectural views to support heterogeneous design and verification.

[BibT_eX]

[DOI]

,

,

,

,

,

Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

Logic and Compositional Verification of Hybrid Systems - (Invited Tutorial).

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Quantifier Elimination over Finite Fields Using Gröbner Bases.

[BibT_eX]

[DOI]

,

,

Edmund M. Clarke

Proceedings of the Algebraic Informatics - 4th International Conference, 2011

Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

J. Log. Comput., 2010

Differential Dynamic Logics.

[BibT_eX]

[DOI]

Künstliche Intell., 2010

Bayesian statistical model checking with application to Simulink/Stateflow verification.

[BibT_eX]

[DOI]

,

,

Edmund M. Clarke

Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Quantified Differential Dynamic Logic for Distributed Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Real Analysis for Complex Systems.

[BibT_eX]

[DOI]

Proceedings of the 6th International Verification Workshop, 2010

Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics.

[BibT_eX]

[DOI]

Springer, ISBN: 978-3-642-14508-7, 2010

2009

Computing differential invariants of hybrid systems as fixedpoints.

[BibT_eX]

[DOI]

,

Edmund M. Clarke

Formal Methods Syst. Des., 2009

Verification of Cyberphysical Transportation Systems.

[BibT_eX]

[DOI]

IEEE Intell. Syst., 2009

European Train Control System: A Case Study in Formal Verification.

[BibT_eX]

[DOI]

,

Jan-David Quesel

Proceedings of the Formal Methods and Software Engineering, 2009

Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.

[BibT_eX]

[DOI]

,

Edmund M. Clarke

Proceedings of the FM 2009: Formal Methods, 2009

A Bayesian Approach to Model Checking Biological Systems.

[BibT_eX]

[DOI]

Sumit Kumar Jha

,

Edmund M. Clarke

,

Christopher James Langmead

,

,

,

Proceedings of the Computational Methods in Systems Biology, 7th International Conference, 2009

Real World Verification.

[BibT_eX]

[DOI]

,

Jan-David Quesel

,

Philipp Rümmer

Proceedings of the Automated Deduction, 2009

2008

Differential dynamic logics - automated theorem proving for hybrid systems.

[BibT_eX]

[DOI]

PhD thesis, 2008

Differential Dynamic Logic for Hybrid Systems.

[BibT_eX]

[DOI]

J. Autom. Reason., 2008

Logical Verification and Systematic Parametric Analysis in Train Control.

[BibT_eX]

[DOI]

,

Jan-David Quesel

Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Differentielle dynamische Logiken: Automatisches Beweisen für hybride Systeme [Differential Dynamic Logic: Automated Theorem Proving for Hybrid Systems].

[BibT_eX]

[DOI]

Proceedings of the Ausgezeichnete Informatikdissertationen 2008, 2008

KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description).

[BibT_eX]

[DOI]

,

Jan-David Quesel

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Differential Dynamic Logic for Verifying Parametric Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2007

A Temporal Dynamic Logic for Verifying Hybrid System Invariants.

[BibT_eX]

[DOI]

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

The Image Computation Problem in Hybrid Systems Model Checking.

[BibT_eX]

[DOI]

,

Edmund M. Clarke

Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Differential Logic for Reasoning About Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Combining Deduction and Algebraic Constraints for Hybrid System Analysis.

[BibT_eX]

[DOI]

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

Automating Verification of Cooperation, Control, and Design in Traffic Applications.

[BibT_eX]

[DOI]

,

,

Jens Oehlerking

,

Ernst-Rüdiger Olderog

,

,

,

,

Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006

Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Hybrid Logic, 2006

SAT-based Abstraction Refinement for Real-time Systems.

[BibT_eX]

[DOI]

Stephanie Kemper

,

Proceedings of the Third International Workshop on Formal Aspects of Component Software, 2006

Dynamic Logic with Non-rigid Functions.

[BibT_eX]

[DOI]

Bernhard Beckert

,

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

Loading...