### BibTeX Database Entries

@MISC{Platzer_2004, author = {Andr{\'e} Platzer}, title = {Using a Program Verification Calculus for Constructing Specifications from Implementations}, howpublished = {Minor thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems}, OPTmonth = {Feb}, year = {2004}, school = {University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems}, pages = {83}, abstract = { In this thesis we examine the possibility of automatically constructing the program specification from an implementation, both from a theoretical perspective and as a practical approach with a sequent calculus. As a setting for program specifications we choose dynamic logic for the Java programming language. We show that---despite the undecidable nature of program analysis---the strongest specification of any program can always be constructed algorithmically. Further we outline a practical approach embedded into a sequent calculus for dynamic logic and with a higher focus on readability. Therefor, the central aspect of describing unbounded state changes incorporates the concept of modifies lists for expressing the modifiable portion of the state space. The underlying deductions are carried out by the theorem prover of the KeY System. }, pdf = {http://symbolaris.com/logic/Minoranthe.pdf}, }

@MASTERSTHESIS{Platzer_2004b, author = {Andr{\'e} Platzer}, title = {An Object-oriented Dynamic Logic with Updates}, school = {University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems}, year = {2004}, OPTmonth = {Sep}, pages = {193}, abstract = { With the goal of this thesis being to create a dynamic logic for object-oriented languages, ODL is developed along with a sound and relatively complete calculus. The dynamic logic contains only the absolute logical essentials of object-orientation, yet still allows a ``natural'' representation of all other features of common object-oriented programming languages. ODL is an extension of a dynamic logic for imperative While programs by function modification and dynamic type checks. A generalisation of substitutions, called updates, constitute the central technical device for dealing with object aliasing arising from function modification and for retaining a manageable calculus in practical application scenarios. Further, object enumerators realise object creation in a natural yet powerful way. Finally, completeness is proven relative to first-order arithmetic. Along with the soundness result, this proof constitutes the central part of this thesis and even copes with states containing uncomputable functions.}, pdf = {http://i12www.ira.uka.de/~key/doc/2004/odlMasterThesis.pdf}, }

@INPROCEEDINGS{DBLP:conf/cade/BeckertP06, author = {Bernhard Beckert and Andr{\'e} Platzer}, title = {Dynamic Logic with Non-rigid Functions: A Basis for Object-oriented Program Verification.}, booktitle = {IJCAR}, longbooktitle = {Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, Proceedings}, year = {2006}, pages = {266-280}, doi = {10.1007/11814771_23}, editor = {Ulrich Furbach and Natarajan Shankar}, publisher = {Springer}, series = {LNCS}, volume = {4130}, isbn = {3-540-37187-7}, issn = {0302-9743}, subseries = {LNAI}, keywords = {dynamic logic, sequent calculus, program logic, software verification, logical foundations of programming languages, object-orientation}, abstract = { We introduce a dynamic logic that is enriched by non-rigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, non-rigid functions allow to embed notions of object-orientation in dynamic logic, thereby forming a basis for verification of object-oriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essential aspects of the complex verification system KeY and, hence, constitutes a foundation for object-oriented verification with the principles of reasoning that underly the successful KeY case studies.}, }

@INPROCEEDINGS{DBLP:journals/entcs/Platzer07, author = {Andr{\'e} Platzer}, title = {Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems}, booktitle = {International Workshop on Hybrid Logic, HyLo'06, Seattle, USA, Proceedings}, year = {2007}, editor = {Patrick Blackburn and Thomas Bolander and Torben Bra\"{u}ner and Valeria de Paiva and J{\o}rgen Villadsen}, series = {ENTCS}, journal = {Electr. Notes Theor. Comput. Sci.}, issn = {1571-0661}, volume = {174}, number = {6}, month = {Jun}, pages = {63-77}, doi = {10.1016/j.entcs.2006.11.026}, pdf = {http://symbolaris.com/pub/hdL.pdf}, keywords = {hybrid logic, dynamic logic, sequent calculus, compositional verification, real-time hybrid dynamic systems}, abstract = { We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.}, }

@INPROCEEDINGS{DBLP:journals/entcs/KemperP07, author = {Stephanie Kemper and Andr{\'e} Platzer}, title = {{SAT}-based Abstraction Refinement for Real-time Systems}, booktitle = {Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings}, year = {2007}, editor = {Frank S. de Boer and Vladimir Mencl}, journal = {Electr. Notes Theor. Comput. Sci.}, volume = {182}, series = {ENTCS}, issn = {1571-0661}, pages = {107-122}, doi = {10.1016/j.entcs.2006.09.034}, annote = {Appeared as UNU-IIST Report No.~344 \url{http://www.iist.unu.edu/newrh/III/1/docs/techreports/report344.html}}, keywords = {abstraction refinement, model checking, real-time systems, SAT, Craig interpolation}, abstract = { In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic with linear arithmetic and prove correctness. With this logical representation, we achieve a linear-size representation of parallel composition and introduce a quick abstraction technique that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexample-guided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logic-based abstraction refinement.} }

@INPROCEEDINGS{DBLP:conf/hybrid/Platzer07, author = {Andr{\'e} Platzer}, title = {Differential Logic for Reasoning about Hybrid Systems}, booktitle = {HSCC}, longbooktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings}, year = {2007}, pages = {746-749}, doi = {10.1007/978-3-540-71493-4_75}, editor = {Alberto Bemporad and Antonio Bicchi and Giorgio Buttazzo}, publisher = {Springer}, series = {LNCS}, volume = {4416}, isbn = {978-3-540-71492-7}, keywords = {dynamic logic, hybrid systems, parametric verification}, abstract = { We propose a first-order dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using first-order variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components.} }

@INPROCEEDINGS{DBLP:conf/hybrid/PlatzerC07, author = {Andr{\'e} Platzer and Edmund M. Clarke}, title = {The Image Computation Problem in Hybrid Systems Model Checking}, booktitle = {HSCC}, longbooktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings}, year = {2007}, pages = {473-486}, doi = {10.1007/978-3-540-71493-4_37}, editor = {Alberto Bemporad and Antonio Bicchi and Giorgio Buttazzo}, publisher = {Springer}, series = {LNCS}, volume = {4416}, isbn = {978-3-540-71492-7}, keywords = {model checking, hybrid systems, image computation}, abstract = { In this paper, we analyze limits of approximation techniques for (non-linear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance.}, }

@INPROCEEDINGS{DBLP:conf/lfcs/Platzer07, author = {Andr{\'e} Platzer}, title = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants}, booktitle = {LFCS}, longbooktitle = {Logical Foundations of Computer Science, 5th International Symposium, LFCS'07, New York, USA, June 4-7, 2007, Proceedings}, year = {2007}, pages = {457-471}, doi = {10.1007/978-3-540-72734-7_32}, editor = {Sergei N. Art{\"e}mov and Anil Nerode}, publisher = {Springer}, series = {LNCS}, volume = {4514}, isbn = {978-3-540-72732-3}, keywords = {dynamic logic, temporal logic, sequent calculus, logic for hybrid systems, deductive verification of embedded systems}, abstract = { We combine first-order dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints. } }

@TECHREPORT{DBLP:conf/lfcs/Platzer07:TR, author = {Andr{\'e} Platzer}, title = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants}, number = {12}, year = {2007}, month = {Feb}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {Reports of {SFB/TR~14 AVACS}}, OPTtype = {Reports of {SFB/TR~14 AVACS}}, series = {ATR}, note = {ISSN: 1860-9821, http://www.avacs.org.}, pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_012.pdf}, }

@INPROCEEDINGS{Platzer2007Dagstuhl, author = {Andr{\'e} Platzer}, title = {Differential Logic for Hybrid System Verification -- Reasoning about Interacting Discrete and Continuous Change}, booktitle = {Dagstuhl ``zehn plus eins'' -- Zehn Informatik-Graduiertenkollegs und ein Informatik-Forschungskolleg stellen sich vor}, year = {2007}, pages = {80}, address = {Aachen}, month = {Jun}, publisher = {Verlagshaus Mainz} }

@INPROCEEDINGS{DBLP:conf/tableaux/Platzer07, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logic for Verifying Parametric Hybrid Systems.}, booktitle = {TABLEAUX}, longbooktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, 16th International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings}, year = {2007}, pages = {216-232}, doi = {10.1007/978-3-540-73099-6_17}, editor = {Nicola Olivetti}, volume = {4548}, series = {LNCS}, publisher = {Springer}, isbn = {978-3-540-73098-9}, keywords = {dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination}, abstract = { We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.} }

@TECHREPORT{DBLP:conf/tableaux/Platzer07:TR, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logic for Verifying Parametric Hybrid Systems.}, number = {15}, year = {2007}, month = {May}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {Reports of {SFB/TR~14 AVACS}}, OPTtype = {Reports of {SFB/TR~14 AVACS}}, series = {ATR}, note = {ISSN: 1860-9821, http://www.avacs.org.}, pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_015.pdf}, }

@INPROCEEDINGS{DBLP:conf/verify/Platzer07, author = {Andr{\'e} Platzer}, title = {Combining Deduction and Algebraic Constraints for Hybrid System Analysis.}, booktitle = {VERIFY'07 at CADE, Bremen, Germany}, longbooktitle = {4th International Verification Workshop VERIFY'07, at CADE-21, Bremen, Germany, July 15-16, 2007}, year = {2007}, pages = {164-178}, editor = {Bernhard Beckert}, volume = {259}, publisher = {CEUR-WS.org}, series = {CEUR Workshop Proceedings}, issn = {1613-0073}, pdf = {http://ceur-ws.org/Vol-259/paper14.pdf}, keywords = {modular prover combination, analytic tableaux, verification of hybrid systems, dynamic logic}, abstract = { We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.} }

@INPROCEEDINGS{DBLP:conf/birthday/DammMOOPPSW07, author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and Ernst-R{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc Segelken and Boris Wirtz}, title = {Automating Verification of Cooperation, Control, and Design in Traffic Applications}, booktitle = {Formal Methods and Hybrid Real-Time Systems}, longbooktitle = {Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bj{\o}rner and Chaochen Zhou on the Occasion of Their 70th Birthdays}, year = {2007}, pages = {115-169}, doi = {10.1007/978-3-540-75221-9_6}, editor = {Cliff B. Jones and Zhiming Liu and Jim Woodcock}, publisher = {Springer}, series = {LNCS}, volume = {4700}, isbn = {978-3-540-75220-2}, keywords = {}, abstract = { We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.}, }

@ARTICLE{DBLP:journals/jar/Platzer08, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logic for Hybrid Systems.}, journal = {J. Autom. Reas.}, longjournal = {Journal of Automated Reasoning}, year = {2008}, volume = {41}, number = {2}, pages = {143-189}, doi = {10.1007/s10817-008-9103-8}, issn = {0168-7433}, keywords = {dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems}, abstract = { Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well-suited for verifying realistic hybrid systems with parametric system dynamics. } }

@INPROCEEDINGS{DBLP:conf/hybrid/PlatzerQ08, author = {Andr{\'e} Platzer and Jan-David Quesel}, title = {Logical Verification and Systematic Parametric Analysis in Train Control.}, booktitle = {HSCC}, longbooktitle = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings}, year = {2008}, pages = {646-649}, doi = {10.1007/978-3-540-78929-1_55}, editor = {Magnus Egerstedt and Bud Mishra}, publisher = {Springer}, series = {LNCS}, volume = {4981}, isbn = {978-3-540-78928-4}, keywords = {parametric verification, logic for hybrid systems, symbolic decomposition}, abstract = { We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logic-based decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.} }

@ARTICLE{DBLP:journals/logcom/Platzer10, author = {Andr{\'e} Platzer}, title = {Differential-algebraic Dynamic Logic for Differential-algebraic Programs}, journal = {J. Log. Comput.}, longjournal = {Journal of Logic and Computation}, year = {2010}, volume = {20}, number = {1}, pages = {309-352}, note = {Advance Access published on November 18, 2008}, doi = {10.1093/logcom/exn070}, keywords = {dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving}, abstract = { We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with which differential-algebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.}, }

@TECHREPORT{DBLP:conf/cav/PlatzerC08:TR, author = {Andr{\'e} Platzer and Edmund M. Clarke}, title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints}, number = {CMU-CS-08-103}, year = {2008}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2008/CMU-CS-08-103.pdf} }

@INPROCEEDINGS{Platzer2008Dagstuhl, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logics. Automated Theorem Proving for Hybrid Systems}, booktitle = {Proceedings des gemeinsamen Workshops der Graduiertenkollegs 2008, Dagstuhl}, year = {2008}, editor = {Malte Diehl and Henrik Lipskoch and Roland Meyer and Christian Storm}, series = {Trustworthy Software Systems}, pages = {29}, address = {Berlin}, month = {may}, publisher = {Gito Verlag}, isbn = {978-3-940019-39-4}, location = {May 19--21, 2008, Dagstuhl, Germany} }

@INPROCEEDINGS{DBLP:conf/cav/PlatzerC08, author = {Andr{\'e} Platzer and Edmund M. Clarke}, title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints}, booktitle = {CAV}, longbooktitle = {Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings}, year = {2008}, pages = {176-189}, month = {}, editor = {Aarti Gupta and Sharad Malik}, publisher = {Springer}, series = {LNCS}, volume = {5123}, isbn = {978-3-540-70543-7}, doi = {10.1007/978-3-540-70545-1_17}, keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine}, abstract = { We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.} }

@INPROCEEDINGS{DBLP:conf/cade/PlatzerQ08, author = {Andr{\'e} Platzer and Jan-David Quesel}, title = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.}, booktitle = {IJCAR}, longbooktitle = {Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings}, year = {2008}, pages = {171-178}, editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek}, publisher = {Springer}, series = {LNCS}, volume = {5195}, isbn = {978-3-540-71069-1}, issn = {0302-9743}, subseries = {LNAI}, doi = {10.1007/978-3-540-71070-7_15}, keywords = {dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems}, abstract = { KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.} }

@PHDTHESIS{Platzer08, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems}, school = {Department of Computing Science, University of Oldenburg}, year = {2008}, pages = {299}, }

@INPROCEEDINGS{ClarkeKPR08, author = {Edmund M. Clarke and Bruce Krogh and Andr{\'e} Platzer and Raj Rajkumar}, title = {Analysis and Verification Challenges for Cyber-Physical Transportation Systems}, year = {2008}, booktitle = {NITRD National Workshop for Research on Transportation Cyber-Physical Systems: Automotive, Aviation, and Rail}, pdf = {http://www.ee.washington.edu/research/nsl/aar-cps/AndrePlatzer-20081020163241.pdf}, abstract = { Substantial technological and engineering advances in various disciplines make it possible more than ever before to provide autonomous control choices for cars, trains, and aircraft. Correct automatic control can improve overall safety tremendously. Yet, ensuring a safe operation of those control assistants under all circumstances requires analysis techniques that are prepared for the rising complexity resulting from combinations of several computerized safety measures. We identify cases where cyber-physical transportation systems pose particularly demanding challenges for future research in formal analysis techniques.} }

@ARTICLE{DBLP:journals/fmsd/PlatzerC09, author = {Andr{\'e} Platzer and Edmund M. Clarke}, title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints}, journal = {Form. Methods Syst. Des.}, longjournal = {Formal Methods in System Design}, year = {2009}, volume = {35}, number = {1}, pages = {98-120}, doi = {10.1007/s10703-009-0079-8}, keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine}, abstract = { We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. With this compositional approach we exploit locality in system designs. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control and car control.} }

@INPROCEEDINGS{DBLP:conf/cade/PlatzerQR09, author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer}, title = {Real World Verification}, booktitle = {CADE}, longbooktitle = {International Conference on Automated Deduction, CADE'09, Montreal, Canada, Proceedings}, year = {2009}, pages = {485-501}, editor = {Renate A. Schmidt}, publisher = {Springer}, series = {LNCS}, volume = {5663}, doi = {10.1007/978-3-642-02959-2_35}, keywords = {real-closed fields, decision procedures, hybrid systems, software verification}, abstract = { Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gr\"obner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gr\"obner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.} }

@ARTICLE{DBLP:journals/ki/Platzer10, author = {Andr{\'e} Platzer}, title = {Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems}, journal = {K\"unstliche Intelligenz}, year = {2010}, volume = {24}, number = {1}, doi = {10.1007/s13218-010-0014-6}, pages = {75-77}, issn = {0933-1875}, abstract = { Designing and analyzing hybrid systems, which are models for complex physical systems, is expensive and error-prone. The dissertation presented in this article introduces a verification logic that is suitable for analyzing the behavior of hybrid systems. It presents a proof calculus and a new deductive verification tool for hybrid systems that has been used successfully to verify aircraft and train control.} }

@TECHREPORT{DBLP:conf/cmsb/JhaCLLPZ09:TR, author = {Sumit Kumar Jha and Edmund Clarke and Christopher Langmead and Axel Legay and Andr{\'e} Platzer and Paolo Zuliani}, title = {Statistical Model Checking for Complex Stochastic Models in Systems Biology}, number = {CMU-CS-09-110}, year = {2009}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2009/CMU-CS-09-110.pdf} }

@INPROCEEDINGS{DBLP:conf/cmsb/JhaCLLPZ09, author = {Sumit Kumar Jha and Edmund Clarke and Christopher Langmead and Axel Legay and Andr{\'e} Platzer and Paolo Zuliani}, title = {A {Bayesian} Approach to Model Checking Biological Systems}, booktitle = {CMSB}, year = {2009}, pages = {218-234}, editor = {Pierpaolo Degano and Roberto Gorrieri}, longbooktitle = {Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {5688}, doi = {10.1007/978-3-642-03845-7_15}, abstract = { Recently, there has been considerable interest in the use of Model Checking for Systems Biology. Unfortunately, the state space of stochastic biological models is often too large for classical Model Checking techniques. For these models, a statistical approach to Model Checking has been shown to be an effective alternative. Extending our earlier work, we present the first algorithm for performing statistical Model Checking using Bayesian Sequential Hypothesis Testing. We show that our Bayesian approach outperforms current statistical Model Checking techniques, which rely on tests from Classical (aka Frequentist) statistics, by requiring fewer system simulations. Another advantage of our approach is the ability to incorporate prior Biological knowledge about the model being verified. We demonstrate our algorithm on a variety of models from the Systems Biology literature and show that it enables faster verification than state-of-the-art techniques, even when no prior knowledge is available.} }

@TECHREPORT{DBLP:conf/cade/PlatzerQR09:TR, author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer}, title = {Real World Verification}, number = {52}, year = {2009}, month = {Jun}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {Reports of {SFB/TR~14 AVACS}}, OPTtype = {Reports of {SFB/TR~14 AVACS}}, series = {ATR}, note = {ISSN: 1860-9821, http://www.avacs.org.}, pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_052.pdf}, }

@ARTICLE{DBLP:journals/expert/Platzer09, author = {Andr{\'e} Platzer}, title = {Verification of Cyberphysical Transportation Systems}, journal = {IEEE Intelligent Systems}, volume = {24}, number = {4}, year = {2009}, pages = {10-13}, doi = {10.1109/MIS.2009.81}, issn = {1541-1672}, keywords = {cyber-physical transportation systems, train control, air traffic control, logic-based analysis, verification}, abstract = { Cyberphysical system technology has an important share in modern intelligent transportation systems, including next generation flight, rail, and car control. This control technology is intended to help improve performance objectives like throughput and improve overall system safety. To ensure that these transportation systems operate correctly, new analysis techniques are needed that consider physical movement combined with computational control to establish properties like collision freedom. Logic-based analysis can verify the correct functioning of these cyberphysical systems.} }

@INPROCEEDINGS{DBLP:conf/fm/PlatzerC09, author = {Andr{\'e} Platzer and Edmund M. Clarke}, title = {Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study}, booktitle = {FM}, year = {2009}, pages = {547-562}, doi = {10.1007/978-3-642-05089-3_35}, editor = {Ana Cavalcanti and Dennis Dams}, longbooktitle = {FM 2009: Formal Methods, 16th International Symposium on Formal Methods, Eindhoven, Netherlands, November 2-6, 2009, Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {5850}, keywords = {formal verification of hybrid systems, deduction, air traffic control, logic for hybrid systems}, abstract = { Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the control choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we analyze collision freedom of roundabout maneuvers in air traffic control, where appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We show that formal verification of hybrid systems can scale to curved flight maneuvers required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver and verify safety properties by compositional verification.} }

@TECHREPORT{DBLP:conf/fm/PlatzerC09:TR, author = {Andr{\'e} Platzer and Edmund M. Clarke}, title = {Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study}, number = {CMU-CS-09-147}, year = {2009}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2008/CMU-CS-09-147.pdf} }

@INPROCEEDINGS{DBLP:conf/icfem/PlatzerQ09, author = {Andr{\'e} Platzer and Jan-David Quesel}, title = {{European Train Control System}: A Case Study in Formal Verification}, booktitle = {ICFEM}, year = {2009}, pages = {246-265}, doi = {10.1007/978-3-642-10373-5_13}, editor = {Karin Breitman and Ana Cavalcanti}, longbooktitle = {Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brasil, December 9-12, 2009. Proceedings}, booktitle = {ICFEM}, publisher = {Springer}, series = {LNCS}, volume = {5885}, isbn = {}, keywords = {formal verification of hybrid systems, train control, theorem proving, parameter constraint identification, disturbances}, abstract = { Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. We verify that safety is preserved when a PI controlled speed supervision is used.} }

@TECHREPORT{DBLP:conf/icfem/PlatzerQ09:TR, author = {Andr{\'e} Platzer and Jan-David Quesel}, title = {{European Train Control System}: A Case Study in Formal Verification}, number = {54}, year = {2009}, month = {Sep}, editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm}, institution = {Reports of {SFB/TR~14 AVACS}}, OPTtype = {Reports of {SFB/TR~14 AVACS}}, series = {ATR}, note = {ISSN: 1860-9821, http://www.avacs.org.}, pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_054.pdf}, }

@INPROCEEDINGS{DBLP:conf/hybrid/ZulianiPC10, author = {Paolo Zuliani and Andr{\'e} Platzer and Edmund M. Clarke}, title = {Bayesian Statistical Model Checking with Application to {Simulink/Stateflow} Verification}, booktitle = {HSCC}, year = {2010}, pages = {243-252}, doi = {10.1145/1755952.1755987}, editor = {Karl Henrik Johansson and Wang Yi}, longbooktitle = {Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010}, booktitle = {HSCC}, publisher = {ACM}, year = {2010}, isbn = {978-1-60558-955-8}, abstract = { We address the problem of model checking stochastic systems, i.e. checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a novel Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic (discrete) systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and non-Bayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing or estimation. We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discrete-time hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than state-of-the-art statistical techniques, while retaining the same error bounds. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models: we have in fact successfully applied it to very large stochastic models from Systems Biology.} }

@TECHREPORT{DBLP:conf/hybrid/ZulianiPC10:TR, author = {Paolo Zuliani and Andr{\'e} Platzer and Edmund M. Clarke}, title = {Bayesian Statistical Model Checking with Application to {Simulink/Stateflow} Verification.}, number = {CMU-CS-10-100}, year = {2010}, month = {Jan}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2010/CMU-CS-10-100.pdf} }

@BOOK{Platzer10, author = {Andr{\'e} Platzer}, title = {Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics}, publisher = {Springer}, address = {Heidelberg}, year = {2010}, isbn = {978-3-642-14508-7}, doi = {10.1007/978-3-642-14509-4}, }

@INPROCEEDINGS{DBLP:conf/csl/Platzer10, author = {Andr{\'e} Platzer}, title = {Quantified Differential Dynamic Logic for Distributed Hybrid Systems}, booktitle = {CSL}, year = {2010}, pages = {469-483}, editor = {Anuj Dawar and Helmut Veith}, longbooktitle = {Computer Science Logic 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings}, booktitle = {CSL}, publisher = {Springer}, series = {LNCS}, volume = {6247}, year = {2010}, doi = {10.1007/978-3-642-15205-4_36}, isbn = {978-3-642-15204-7}, keywords = {Dynamic logic, Distributed hybrid systems, Axiomatization, Theorem proving, Quantified differential equations}, abstract = { We address a fundamental mismatch between the combinations of dynamics that occur in complex physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic networks, where neither structure nor dimension stay the same while the system follows mixed discrete and continuous dynamics. We provide the logical foundations for closing this analytic gap. We develop a system model for distributed hybrid systems that combines quantified differential equations with quantified assignments and dynamic dimensionality-changes. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for it. We prove that this calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when new cars may appear dynamically on the road.} }

@TECHREPORT{DBLP:conf/csl/Platzer10:TR, author = {Andr{\'e} Platzer}, title = {Quantified Differential Dynamic Logic for Distributed Hybrid Systems}, number = {CMU-CS-10-126}, year = {2010}, month = {May}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2010/CMU-CS-10-126.pdf} }

@INPROCEEDINGS{DBLP:conf/hybrid/Platzer11, author = {Andr{\'e} Platzer}, title = {Quantified Differential Invariants}, booktitle = {HSCC}, year = {2011}, pages = {63-72}, doi = {10.1145/1967701.1967713}, editor = {Emilio Frazzoli and Radu Grosu}, longbooktitle = {Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, 2011}, booktitle = {HSCC}, publisher = {ACM}, isbn = {}, keywords = {distributed hybrid systems, verification logic, quantified differential equations, quantified differential invariants}, abstract = { We address the verification problem for distributed hybrid systems with nontrivial dynamics. Consider air traffic collision avoidance maneuvers, for example. Verifying dynamic appearance of aircraft during an ongoing collision avoidance maneuver is a longstanding and essentially unsolved problem. The resulting systems are not hybrid systems and their state space is not of the form R^n. They are distributed hybrid systems with nontrivial continuous and discrete dynamics in distributed state spaces whose dimension and topology changes dynamically over time. We present the first formal verification technique that can handle the complicated nonlinear dynamics of these systems. We introduce quantified differential invariants, which are properties that can be checked for invariance along the dynamics of the distributed hybrid system based on differentiation, quantified substitution, and quantifier elimination in real-closed fields. This gives a computationally attractive technique, because it works without having to solve the infinite-dimensional differential equation systems underlying distributed hybrid systems. We formally verify a roundabout maneuver in which aircraft can appear dynamically.} }

@INPROCEEDINGS{DBLP:conf/aistats/ZawadzkiGP11, author = {Erik P. Zawadzki and Geoffrey J. Gordon and Andr{\'e} Platzer}, title = {An Instantiation-Based Theorem Prover for First-Order Programming}, shortbooktitle = {AISTATS}, year = {2011}, pages = {}, doi = {}, booktitle = {Proceedings of the 14th International Conference on Artifical Intelligence and Statistics (AISTATS) 2011, Fort Lauderdale, FL, USA}, year = {2011}, pages = {}, doi = {}, volume = {15}, series = {JMLR W\&CP}, }

@INPROCEEDINGS{DBLP:conf/fm/LoosPN11, author = {Sarah M. Loos and Andr{\'e} Platzer and Ligia Nistor}, title = {Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified}, booktitle = {FM}, year = {2011}, pages = {42-56}, doi = {10.1007/978-3-642-21437-0_6}, editor = {Michael Butler and Wolfram Schulte}, longbooktitle = {FM 2011: Formal Methods, 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Proceedings}, booktitle = {FM}, publisher = {Springer}, series = {LNCS}, volume = {6664}, year = {2011}, isbn = {}, keywords = {distributed car control, multi-agent systems, highway traffic safety, formal verification, distributed hybrid systems, adaptive cruise control}, }

@TECHREPORT{DBLP:conf/fm/LoosPN11:TR, author = {Sarah M. Loos and Andr{\'e} Platzer and Ligia Nistor}, title = {Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified}, number = {CMU-CS-11-107}, year = {2011}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2011/CMU-CS-11-107.pdf} }

@INPROCEEDINGS{DBLP:conf/cai/GaoPC11, author = {Sicun Gao and Andr{\'e} Platzer and Edmund M. Clarke}, title = {Quantifier Elimination over Finite Fields with {G}r{\"o}bner Bases}, booktitle = {CAI}, year = {2011}, pages = {140-157}, doi = {10.1007/978-3-642-21493-6_9}, editor = {Franz Winkler}, longbooktitle = {Algebraic Informatics, Fourth International Conference, CAI 2011, Linz, Austria, June 21-24, 2011, Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {6742}, }

@INPROCEEDINGS{DBLP:conf/cade/Platzer11, author = {Andr{\'e} Platzer}, title = {Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs}, booktitle = {CADE}, longbooktitle = {International Conference on Automated Deduction, CADE'11, Wroc{\l}aw, Poland, Proceedings}, year = {2011}, pages = {431-445}, doi = {10.1007/978-3-642-22438-6_34}, keywords = {dynamic logic, proof calculus, stochastic differential equations, stochastic hybrid systems, stochastic processes}, editor = {Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans}, publisher = {Springer}, series = {LNCS}, volume = {6803}, isbn = {}, abstract = { Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, real-time systems, hybrid systems, and distributed systems. Some applications also have a stochastic behavior, however, either because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Discrete probabilistic systems have been studied using logic. But logic has been chronically underdeveloped in the context of stochastic hybrid systems, i.e., systems with interacting discrete, continuous, and stochastic dynamics. We aim at overcoming this deficiency and introduce a dynamic logic for stochastic hybrid systems. Our results indicate that logic is a promising tool for understanding stochastic hybrid systems and can help taming some of their complexity. We introduce a compositional model for stochastic hybrid systems. We prove adaptivity, cadlag, and Markov time properties, and prove that the semantics of our logic is measurable. We present compositional proof rules, including rules for stochastic differential equations, and prove soundness. } }

@TECHREPORT{DBLP:conf/cade/Platzer11:TR, author = {Andr{\'e} Platzer}, title = {Stochastic Differential Dynamic Logic for Stochastic Hybrid Systems}, number = {CMU-CS-11-111}, year = {2011}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2011/CMU-CS-11-111.pdf} }

@TECHREPORT{Platzer11:diffcut, author = {Andr{\'e} Platzer}, title = {The Structure of Differential Invariants and Differential Cut Elimination}, number = {CMU-CS-11-112}, year = {2011}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2011/CMU-CS-11-112.pdf} }

@INPROCEEDINGS{DBLP:conf/cav/Platzer11, author = {Andr{\'e} Platzer}, title = {Logic and Compositional Verification of Hybrid Systems (Invited Tutorial)}, booktitle = {CAV}, longbooktitle = {Computer Aided Verification, 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings}, year = {2011}, pages = {28-43}, month = {}, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, publisher = {Springer}, series = {LNCS}, volume = {6806}, doi = {10.1007/978-3-642-22110-1_4}, abstract = { Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behavior. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerised controllers for physical systems which are guaranteed to meet their design goals. The continuous dynamics of hybrid systems can be modeled by differential equations, the discrete dynamics by a combination of discrete state-transitions and conditional execution. The discrete and continuous dynamics interact to form hybrid systems, which makes them quite challenging for verification. In this tutorial, we survey state-of-the-art verification techniques for hybrid systems. In particular, we focus on a coherent logical approach for systematic hybrid systems analysis. We survey theory, practice, and applications, and show how hybrid systems can be verified in the hybrid systems verification tool KeYmaera. KeYmaera has been used successfully to verify safety, reactivity, controllability, and liveness properties, including collision freedom in air traffic, car, and railway control systems. It has also been used to verify properties of electrical circuits. } }

@INPROCEEDINGS{DBLP:conf/icfem/RenshawLP11, author = {David W. Renshaw and Sarah M. Loos and Andr{\'e} Platzer}, title = {Distributed Theorem Proving for Distributed Hybrid Systems}, booktitle = {ICFEM}, year = {2011}, pages = {356-371}, doi = {10.1007/978-3-642-24559-6_25}, editor = {Shengchao Qin and Zongyan Qiu}, longbooktitle = {Formal Methods and Software Engineering, 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {6991}, isbn = {}, keywords = {Hybrid systems, theorem proving, formal verification, distributed systems}, }

@INPROCEEDINGS{DBLP:conf/icfem/MartinsPL11, author = {Jo{\~a}o Martins and Andr{\'e} Platzer and Jo{\~a}o Leite}, title = {Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications}, booktitle = {ICFEM}, year = {2011}, pages = {131-146}, doi = {10.1007/978-3-642-24559-6_11}, editor = {Shengchao Qin and Zongyan Qiu}, longbooktitle = {Formal Methods and Software Engineering, 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {6991}, isbn = {}, keywords = {Bayesian statistical model checking, distributed hybrid systems, probabilistic hybrid automata, verification of smart grid}, }

@INPROCEEDINGS{DBLP:conf/itsc/LoosP11, author = {Sarah M. Loos and Andr{\'e} Platzer}, title = {Safe Intersections: At the Crossing of Hybrid Systems and Verification}, booktitle = {ITSC}, longbooktitle = {Intelligent Transportation Systems (ITSC), 14th International IEEE Conference on, October 5-7, Washington, DC, USA, Proceedings}, year = {2011}, pages = {1181-1186}, doi = {10.1109/ITSC.2011.6083138}, keywords = {}, editor = {Kyongsu Yi}, }

@INPROCEEDINGS{DBLP:conf/cdc/RajhansBLKPG11, author = {Akshay Rajhans and Ajinkya Bhave and Sarah M. Loos and Bruce H. Krogh and Andr{\'e} Platzer and David Garlan}, title = {Using parameters in architectural views to support heterogeneous design and verification}, booktitle = {CDC}, longbooktitle = {50th IEEE Conference on Decision and Control and European Control Conference}, year = {2011}, pages = {2705-2710}, doi = {10.1109/CDC.2011.6161408}, isbn = {978-1-61284-800-6}, }

@TECHREPORT{RenshawP11, author = {David W. Renshaw and Andr{\'e} Platzer}, title = {Differential Invariants and Symbolic Integration for Distributed Hybrid Systems}, number = {CMU-CS-12-107}, year = {2011}, month = {May}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2012/CMU-CS-12-107.pdf} }

@INPROCEEDINGS{DBLP:conf/iccps/MitschLP12, author = {Stefan Mitsch and Sarah M. Loos and Andr{\'e} Platzer}, title = {Towards formal verification of freeway traffic control}, booktitle = {ICCPS}, longbooktitle = {ACM/IEEE Third International Conference on Cyber-Physical Systems, Beijing, China, April 17-19}, year = {2012}, pages = {171-180}, publisher = {IEEE}, isbn = {978-0-7695-4695-7}, doi = {10.1109/ICCPS.2012.25}, editor = {Chenyang Lu}, }

@TECHREPORT{DBLP:conf/lics/Platzer12b:TR, author = {Andr{\'e} Platzer}, title = {The Complete Proof Theory of Hybrid Systems}, number = {CMU-CS-11-144}, year = {2011}, month = {November}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2011/CMU-CS-11-144.pdf} }

@INPROCEEDINGS{DBLP:conf/acc/ArechigaLPK12, author = {Nikos Ar{\'e}chiga and Sarah M. Loos and Andr{\'e} Platzer and Bruce H. Krogh}, title = {Using Theorem Provers to Guarantee Closed-Loop System Properties}, booktitle = {ACC}, longbooktitle = {American Control Conference, Montr\'eal, Canada, June 27-29}, year = {2012}, editor = {Dawn Tilbury}, pages = {3573-3580}, doi = {10.1109/ACC.2012.6315388}, }

@ARTICLE{DBLP:journals/lmcs/Platzer12, author = {Andr{\'e} Platzer}, title = {The Structure of Differential Invariants and Differential Cut Elimination}, journal = {Logical Methods in Computer Science}, volume = {8}, number = {4}, year = {2012}, pages = {1-38}, doi = {10.2168/LMCS-8(4:16)2012}, keywords = {Proof theory, differential equations, differential invariants, differential cut elimination, differential dynamic logic hybrid systems, logics of programs, real differential semialgebraic geometry}, abstract = { The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze trade-offs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics. } }

@INPROCEEDINGS{DBLP:conf/lics/Platzer12a, author = {Andr{\'e} Platzer}, title = {Logics of Dynamical Systems}, booktitle = {LICS}, year = {2012}, pages = {13-24}, doi = {10.1109/LICS.2012.13}, longbooktitle = {Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25???28, 2012}, publisher = {IEEE}, isbn = {978-1-4673-2263-8}, keywords = {logic of dynamical systems, dynamic logic, differential dynamic logic, hybrid systems, axiomatization, deduction}, abstract = { We study the logic of dynamical systems, that is, logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the state of a system evolves over time. They are important in modeling and understanding many applications, including embedded systems and cyber-physical systems. In discrete dynamical systems, the state evolves in discrete steps, one step at a time, as described by a difference equation or discrete state transition relation. In continuous dynamical systems, the state evolves continuously along a function, typically described by a differential equation. Hybrid dynamical systems or hybrid systems combine both discrete and continuous dynamics. This is a brief survey of differential dynamic logic for specifying and verifying properties of hybrid systems. We explain hybrid system models, differential dynamic logic, its semantics, and its axiomatization for proving logical formulas about hybrid systems. We study differential invariants, i.e., induction principles for differential equations. We briefly survey theoretical results, including soundness and completeness and deductive power. Differential dynamic logic has been implemented in automatic and interactive theorem provers and has been used successfully to verify safety-critical applications in automotive, aviation, railway, robotics, and analogue electrical circuits.} }

@INPROCEEDINGS{DBLP:conf/lics/Platzer12b, author = {Andr{\'e} Platzer}, title = {The Complete Proof Theory of Hybrid Systems}, booktitle = {LICS}, year = {2012}, pages = {541-550}, doi = {10.1109/LICS.2012.64}, longbooktitle = {Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25???28, 2012}, publisher = {IEEE}, isbn = {978-1-4673-2263-8}, keywords = {proof theory, hybrid dynamical systems, differential dynamic logic, axiomatization, completeness}, abstract = { Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has often been claimed that hybrid systems are more challenging than continuous dynamical systems and than discrete systems. We now show that, proof-theoretically, this is not the case. We present a complete proof-theoretical alignment that interreduces the discrete dynamics and the continuous dynamics of hybrid systems. We give a sound and complete axiomatization of hybrid systems relative to continuous dynamical systems and a sound and complete axiomatization of hybrid systems relative to discrete dynamical systems. Thanks to our axiomatization, proving properties of hybrid systems is exactly the same as proving properties of continuous dynamical systems and again, exactly the same as proving properties of discrete dynamical systems. This fundamental cornerstone sheds light on the nature of hybridness and enables flexible and provably perfect combinations of discrete reasoning with continuous reasoning that lift to all aspects of hybrid systems and their fragments.} }

@TECHREPORT{Platzer12:dGL, author = {Andr{\'e} Platzer}, title = {Differential Game Logic for Hybrid Games}, number = {CMU-CS-12-105}, year = {2012}, month = {March}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2012/CMU-CS-12-105.pdf} }

@ARTICLE{DBLP:journals/lmcs/Platzer12b, author = {Andr{\'e} Platzer}, title = {A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems}, journal = {Logical Methods in Computer Science}, volume = {8}, number = {4}, year = {2012}, pages = {1-44}, doi = {10.2168/LMCS-8(4:17)2012}, note = {Special issue for selected papers from CSL'10} }

@ARTICLE{DBLP:journals/corr/abs-1205-4788, author = {Andr{\'e} Platzer}, title = {Dynamic Logics of Dynamical Systems}, journal = {CoRR}, volume = {abs/1205.4788}, year = {2012}, url = {http://arxiv.org/abs/1205.4788}, }

@INPROCEEDINGS{DBLP:conf/itp/Platzer12, author = {Andr{\'e} Platzer}, title = {A Differential Operator Approach to Equational Differential Invariants}, booktitle = {ITP}, longbooktitle = {Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA}, year = {2012}, pages = {28-48}, month = {}, editor = {Lennart Beringer and Amy Felty}, publisher = {Springer}, series = {LNCS}, volume = {7406}, doi = {}, keywords = {differential dynamic logic, differential invariants, differential equations, hybrid systems}, abstract = { Hybrid systems, i.e., dynamical systems combining discrete and continuous dynamics, have a complete axiomatization in differential dynamic logic relative to differential equations. Differential invariants are a natural induction principle for proving properties of the remaining differential equations. We study the equational case of differential invariants using a differential operator view. We relate differential invariants to Lie's seminal work and explain important structural properties resulting from this view. Finally, we study the connection of differential invariants with partial differential equations in the context of the inverse characteristic method for computing differential invariants. } }

@INPROCEEDINGS{DBLP:conf/cade/QueselP12, author = {Jan-David Quesel and Andr{\'e} Platzer}, title = {Playing Hybrid Games with KeYmaera}, booktitle = {IJCAR}, year = {2012}, pages = {439-453}, doi = {10.1007/978-3-642-31365-3_34}, editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler}, longbooktitle = {Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK. Proceedings}, series = {LNCS}, volume = {7364}, publisher = {Springer}, isbn = {978-3-642-31364-6}, }

@INPROCEEDINGS{DBLP:conf/dcfs/Platzer12, author = {Andr{\'e} Platzer}, title = {Logical Analysis of Hybrid Systems: A Complete Answer to a Complexity Challenge}, booktitle = {DCFS}, longbooktitle = {Descriptional Complexity of Formal Systems - 14th International Workshop, DCFS 2012, Braga, Portugal, July 23-25, 2012. Proceedings}, year = {2012}, pages = {43-49}, doi = {10.1007/978-3-642-31623-4_3}, editor = {Martin Kutrib and Nelma Moreira and Rog{\'e}rio Reis}, publisher = {Springer}, series = {LNCS}, volume = {7386}, isbn = {978-3-642-31622-7}, }

@INPROCEEDINGS{DBLP:conf/qest/HenriquesMZPC12, author = {David Henriques and Jo{\~a}o G. Martins and Paolo Zuliani and Andr{\'e} Platzer and Edmund M. Clarke}, title = {Statistical Model Checking for {Markov} Decision Processes}, booktitle = {QEST}, year = {2012}, pages = {84-93}, doi = {10.1109/QEST.2012.19}, longbooktitle = {Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012, London, UK, 17-20 September, 2012}, publisher = {IEEE Computer Society}, keywords = {statistical model checking, Markov decision processes, reinforcement learning}, abstract = { Statistical Model Checking (SMC) is a computationally very efficient verification technique based on selective system sampling. One well identified shortcoming of SMC is that, unlike probabilistic model checking, it cannot be applied to systems featuring nondeterminism, such as Markov Decision Processes (MDP). We address this limitation by developing an algorithm that resolves nondeterminism probabilistically, and then uses multiple rounds of sampling and Reinforcement Learning to provably improve resolutions of nondeterminism with respect to satisfying a Bounded Linear Temporal Logic (BLTL) property. Our algorithm thus reduces an MDP to a fully probabilistic Markov chain on which SMC may be applied to give an approximate solution to the problem of checking the probabilistic BLTL property. We integrate our algorithm in a parallelised modification of the PRISM simulation framework. Extensive validation with both new and PRISM benchmarks demonstrates that the approach scales very well in scenarios where symbolic algorithms fail to do so.} }

@TECHREPORT{DBLP:conf/hybrid/LoosRP13:TR, author = {David W. Renshaw and Sarah Loos and Andr{\'e} Platzer}, title = {Mechanized Safety Proofs for Disc-Constrained Aircraft}, number = {CMU-CS-12-132}, year = {2012}, month = {August}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2012/CMU-CS-12-132.pdf} }

@ARTICLE{DBLP:journals/jalc/Platzer12, author = {Andr{\'e} Platzer}, title = {Logical Analysis of Hybrid Systems: A Complete Answer to a Complexity Challenge}, journal = {Journal of Automata, Languages and Combinatorics}, volume = {17}, number = {2-4}, year = {2012}, pages = {265-275}, }

@INPROCEEDINGS{DBLP:conf/hybrid/KouskoulasRPK13, author = {Yanni Kouskoulas and David W. Renshaw and Andr{\'e} Platzer and Peter Kazanzides}, title = {Certifying the Safe Design of a Virtual Fixture Control Algorithm for a Surgical Robot}, year = {2013}, pages = {263-272}, doi = {10.1145/2461328.2461369}, publisher = {ACM}, editor = {Calin Belta and Franjo Ivancic}, booktitle = {Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013}, }

@INPROCEEDINGS{DBLP:conf/hybrid/LoosRP13, author = {Sarah M. Loos and David W. Renshaw and Andr{\'e} Platzer}, title = {Formal Verification of Distributed Aircraft Controllers}, year = {2013}, pages = {125-130}, doi = {10.1145/2461328.2461350}, publisher = {ACM}, editor = {Calin Belta and Franjo Ivancic}, booktitle = {Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013}, }

@TECHREPORT{Platzer13:dGL, author = {Andr{\'e} Platzer}, title = {A Complete Axiomatization for Differential Game Logic for Hybrid Games}, number = {CMU-CS-13-100R}, year = {2013}, month = {January}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, note = {Extended in revised version from July 2013}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2013/CMU-CS-13-100R.pdf} }

@INPROCEEDINGS{DBLP:conf/cpsed/Platzer13, author = {Andr{\'e} Platzer}, title = {Teaching {CPS} Foundations With Contracts}, year = {2013}, booktitle = {CPS-Ed}, longbooktitle = {First Workshop on Cyber-Physical Systems Education}, pages = {7-10}, }

@INPROCEEDINGS{DBLP:conf/ijcai/ZawadzkiPG13, author = {Erik P. Zawadzki and Andr{\'e} Platzer and Geoffrey J. Gordon}, title = {A Generalization of {SAT} and {\#SAT} for Policy Evaluation}, booktitle = {IJCAI}, year = {2013}, pages = {2583-2589}, editor = {Francesca Rossi}, longbooktitle = {IJCAI 2013, Proceedings of the 23nd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013}, publisher = {IJCAI/AAAI}, isbn = {}, }

@TECHREPORT{DBLP:conf/ijcai/ZawadzkiPG13:TR, author = {Erik P. Zawadzki and Andr{\'e} Platzer and Geoffrey J. Gordon}, title = {A Generalization of {SAT} and {\#SAT} for Policy Evaluation}, number = {CMU-CS-13-107}, year = {2013}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2013/CMU-CS-13-107.pdf} }

@INPROCEEDINGS{DBLP:conf/rss/MitschGP13, author = {Stefan Mitsch and Khalil Ghorbal and Andr{\'e} Platzer}, title = {On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles}, booktitle = {Robotics: Science and Systems}, year = {2013}, editor = {Paul Newman and Dieter Fox and David Hsu}, longbooktitle = {Robotics: Science and Systems IX, Technische Universit{\"a}t Berlin, Berlin, Germany, June 24 - June 28, 2013}, isbn = {978-981-07-3937-9} }

@ARTICLE{DBLP:journals/fmsd/ZulianiPC13, author = {Paolo Zuliani and Andr{\'e} Platzer and Edmund M. Clarke}, title = {Bayesian Statistical Model Checking with Application to {Simulink/Stateflow} Verification}, journal = {Formal Methods in System Design}, volume = {43}, number = {2}, year = {2013}, pages = {338-367}, doi = {10.1007/s10703-013-0195-3}, issn = {0925-9856}, keywords = {Probabilistic verification, Hybrid systems, Stochastic systems, Statistical model checking, Hypothesis testing, Estimation}, abstract = { We address the problem of model checking stochastic systems, i.e., checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for a certain class of hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic discrete systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and non-Bayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing (i.e., testing against a probability threshold) or estimation (i.e., computing with high probability a value close to the true probability). We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discrete-time hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than state-of-the-art statistical techniques. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models. It is in principle applicable to a variety of stochastic models from other domains, e.g., systems biology. } }

@INPROCEEDINGS{DBLP:conf/itsc/LoosWSP13, author = {Sarah M. Loos and David Witmer and Peter Steenkiste and Andr{\'e} Platzer}, title = {Efficiency Analysis of Formally Verified Adaptive Cruise Controllers}, booktitle = {ITSC}, longbooktitle = {Intelligent Transportation Systems (ITSC), 16th International IEEE Conference on, October 6-9, The Hague, Netherlands, Proceedings}, year = {2013}, pages = {1565-1570}, doi = {10.1109/ITSC.2013.6728453}, editor = {Andreas Hegyi and Bart De Schutter}, isbn = {978-1-4799-2914-613}, keywords = {Traffic theory for ITS, Network modeling, Driver assistance systems, V2V wireless communication, Hybrid systems, Formal verification}, abstract = { We consider an adaptive cruise control system in which control decisions are made based on position and velocity information received from other vehicles via V2V wireless communication. If the vehicles follow each other at a close distance, they have better wireless reception but collisions may occur when a follower car does not receive notice about the decelerations of the leader car fast enough to react before it is too late. If the vehicles are farther apart, they would have a bigger safety margin, but the wireless communication drops out more often, so that the follower car no longer receives what the leader car is doing. In order to guarantee safety, such a system must return control to the driver if it does not receive an update from a nearby vehicle within some timeout period. The value of this timeout parameter encodes a tradeoff between the likelihood that an update is received and the maximum safe acceleration. Combining formal verification techniques for hybrid systems with a wireless communication model, we analyze how the expected efficiency of a provably-safe adaptive cruise control syst em is affected by the value of this timeout. } }

@INPROCEEDINGS{DBLP:conf/tacas/GhorbalP14, author = {Khalil Ghorbal and Andr{\'e} Platzer}, title = {Characterizing Algebraic Invariants by Differential Radical Invariants}, booktitle = {TACAS}, year = {2014}, pages = {279-294}, editor = {Erika {\'A}brah{\'a}m and Klaus Havelund}, longbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings}, publisher = {Springer}, volume = {8413}, }

@TECHREPORT{DBLP:conf/tacas/GhorbalP14:TR, author = {Khalil Ghorbal and Andr{\'e} Platzer}, title = {Characterizing Algebraic Invariants by Differential Radical Invariants}, number = {CMU-CS-13-129}, year = {2013}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2012/CMU-CS-13-129.pdf} }

@INPROCEEDINGS{DBLP:conf/fm/MitschQP14, author = {Stefan Mitsch and Jan-David Quesel and Andr{\'e} Platzer}, title = {Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems}, booktitle = {FM}, year = {2014}, pages = {481-496}, doi = {10.1007/978-3-319-06410-9_33}, editor = {Cliff B. Jones and Pekka Pihlajasaari and Jun Sun}, longbooktitle = {FM 2014: Formal Methods, 19th International Symposium on Formal Methods, Singapore, May 12-16, 2014, Proceedings}, publisher = {Springer}, volume = {8442}, }

@ARTICLE{DBLP:journals/jhuapltechdigest/KouskoulasPK13, author = {Yanni Kouskoulas and Andr{\'e} Platzer and Peter Kazanzides}, title = {Formal Methods for Robotic System Control Software}, journal = {Johns Hopkins APL Technical Digest}, volume = {32}, number = {2}, year = {2013}, pages = {490-498}, eprint = {http://techdigest.jhuapl.edu/TD/td3202/32_02-Kouskoulas.pdf}, }

@MISC{FCPS13, author = {Andr\'e Platzer}, title = {Foundations of Cyber-Physical Systems}, year = {2013}, howpublished = {Lecture Notes 15-424/624, Carnegie Mellon University}, url = {http://www.cs.cmu.edu/~aplatzer/course/fcps13/fcps13.pdf} }

@INPROCEEDINGS{DBLP:conf/optml/ZawadzkiGP13, author = {Erik P. Zawadzki and Geoffrey J. Gordon and Andr{\'e} Platzer}, title = {A Projection Algorithm for Strictly Monotone Linear Complementarity Problems}, booktitle = {6th NIPS Workshop on Optimization for Machine Learning}, year = {2013}, }

@INPROCEEDINGS{DBLP:conf/tacas/GhorbalP14, author = {Khalil Ghorbal and Andr{\'e} Platzer}, title = {Characterizing Algebraic Invariants by Differential Radical Invariants}, booktitle = {TACAS}, year = {2014}, pages = {279-294}, doi = {10.1007/978-3-642-54862-8_19}, editor = {Erika {\'A}brah{\'a}m and Klaus Havelund}, longbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {8413}, isbn = {978-3-642-54861-1}, }

@ARTICLE{DBLP:journals/mics/MitschPP14, author = {Stefan Mitsch and Grant Olney Passmore and Andr{\'e} Platzer}, title = {Collaborative Verification-Driven Engineering of Hybrid Systems}, journal = {Mathematics in Computer Science}, volume = {8}, number = {1}, year = {2014}, pages = {71-97}, doi = {10.1007/s11786-014-0176-y}, }

@INPROCEEDINGS{DBLP:conf/cade/JeanninP14, author = {Jean{-}Baptiste Jeannin and Andr{\'e} Platzer}, title = {{dTL$^2$}: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems}, booktitle = {IJCAR}, year = {2014}, pages = {292-306}, doi = {10.1007/978-3-319-08587-6_22}, editor = {St{\'e}phane Demri and Deepak Kapur and Christoph Weidenbach}, longbooktitle = {Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings}, publisher = {Springer}, series = {LNCS}, subseries = {LNAI}, volume = {8562}, isbn = {978-3-319-08586-9}, }

@ARTICLE{DBLP:jourals/tac/RajhansBRKGPS14, author = {Akshay Rajhans and Ajinkya Bhave and Ivan Ruchkin and Bruce H. Krogh and David Garlan and Andr{\'e} Platzer and Bradley Schmerl}, title = {Supporting Heterogeneity in Cyber-Physical Systems Architectures}, journal = {IEEE Transactions on Automatic Control}, year = {2014}, volume = {59}, number = {12}, pages = {3178-3193}, doi = {10.1109/TAC.2014.2351672}, }

@INPROCEEDINGS{DBLP:conf/sas/GhorbalSP14, author = {Khalil Ghorbal and Andrew Sogokon and Andr{\'e} Platzer}, title = {Invariance of Conjunctions of Polynomial Equalities for Algebraic Differential Equations}, booktitle = {SAS}, year = {2014}, pages = {151-167}, editor = {Markus M{\"u}ller-Olm and Helmut Seidl}, longbooktitle = {Static Analysis - 21th International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {8723}, isbn = {978-3-319-10935-0}, doi = {10.1007/978-3-319-10936-7_10} }

@TECHREPORT{DBLP:conf/rv/MitschP14:TR, author = {Stefan Mitsch and Andr{\'e} Platzer}, title = {{ModelPlex}: Verified Runtime Validation of Verified Cyber-Physical System Models}, number = {CMU-CS-14-121}, year = {2014}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2014/CMU-CS-14-121.pdf} }

@INPROCEEDINGS{DBLP:conf/rv/MitschP14, author = {Stefan Mitsch and Andr{\'e} Platzer}, title = {{ModelPlex}: Verified Runtime Validation of Verified Cyber-Physical System Models}, booktitle = {RV}, year = {2014}, pages = {199-214}, doi = {10.1007/978-3-319-11164-3_17}, editor = {Borzoo Bonakdarpour and Scott A. Smolka}, longbooktitle = {Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22--25, 2014. Proceedings}, publisher = {Springer}, series = {LNCS}, volume = {8734}, }

@INPROCEEDINGS{DBLP:conf/fmra/MitschQP14, author = {Stefan Mitsch and Jan-David Quesel and Andr{\'e} Platzer}, title = {From Safety to Guilty \& from Liveness to Niceness}, editor = {Calin Belta and Hadas Kress-Gazit}, booktitle = {5th Workshop on Formal Methods for Robotics and Automation}, year = {2014}, }

@ARTICLE{DBLP:journals/jais/GhorbalJZPGC14, author = {Khalil Ghorbal and Jean{-}Baptiste Jeannin and Erik P. Zawadzki and Andr{\'e} Platzer and Geoffrey J. Gordon and Peter Capell}, title = {Hybrid Theorem Proving of Aerospace Systems: Applications and Challenges}, journal = {Journal of Aerospace Information Systems}, volume = {11}, pages = {702-713}, doi = {10.2514/1.I010178}, }

@ARTICLE{DBLP:journals/eatcs/Platzer14, author = {Andr{\'e} Platzer}, title = {Analog and Hybrid Computation: Dynamical Systems and Programming Languages}, journal = {Bulletin of the {EATCS}}, year = {2014}, volume = {114}, eprint = {http://bulletin.eatcs.org/index.php/beatcs/article/viewFile/292/274}, }

@INPROCEEDINGS{DBLP:conf/vmcai/GhorbalSP15, author = {Khalil Ghorbal and Andrew Sogokon and Andr{\'e} Platzer}, title = {A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets}, booktitle = {VMCAI}, year = {2015}, pages = {431-448}, doi = {10.1007/978-3-662-46081-8_24}, editor = {Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen}, longbooktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015, Proceedings}, series = {LNCS}, volume = {8931}, publisher = {Springer}, }

@UNPUBLISHED{LoosP14:TeachCPS, author = {Sarah M. Loos and Andr{\'e} Platzer}, title = {Teaching Cyber-Physical Systems with Logic}, year = {2014} }

@TECHREPORT{JeanninGKGSZP14:TR, author = {Jean{-}Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Ryan Garnder and Aurora Schmidt and Erik Zawadzki and Andr{\'e} Platzer}, title = {A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System}, number = {CMU-CS-14-138}, year = {2014}, month = {}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2014/CMU-CS-14-138.pdf} }

@MISC{FCPS14, author = {Andr\'e Platzer}, title = {Foundations of Cyber-Physical Systems}, year = {2014}, howpublished = {Lecture Notes 15-424/624, Carnegie Mellon University}, url = {http://symbolaris.com/course/fcps14/fcps14.pdf} }

@ARTICLE{@INPROCEEDINGS{DBLP:journals/sttt/QueselMLAP165, author = {Jan-David Quesel and Stefan Mitsch and Sarah Loos and Nikos Ar{\'e}chiga and Andr{\'e} Platzer}, title = {How to Model and Prove Hybrid Systems with {KeYmaera}: A Tutorial on Safety}, journal = {STTT}, year = {2016}, volume = {18}, number = {1}, pages = {67-91}, doi = {10.1007/s10009-015-0367-0}, }

@INPROCEEDINGS{DBLP:conf/tacas/JeanninGKGSZP15, author = {Jean{-}Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Ryan Gardner and Aurora Schmidt and Erik Zawadzki and Andr{\'e} Platzer}, title = {A Formally Verified Hybrid System for the Next-generation Airborne Collision Avoidance System}, booktitle = {TACAS}, year = {2015}, pages = {21-36}, doi = {10.1007/978-3-662-46680-3_2}, editor = {Christel Baier and Cesare Tinelli}, longbooktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, London, UK, April 11-18, 2015, Proceedings}, series = {LNCS}, volume = {9035}, publisher = {Springer}, }

@TECHREPORT{Platzer14:dGI, author = {Andr{\'e} Platzer}, title = {Differential Hybrid Games}, number = {CMU-CS-14-102}, year = {2014}, month = {December}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2014/CMU-CS-14-102.pdf} }

@INPROCEEDINGS{DBLP:conf/cade/Platzer15, author = {Andr{\'e} Platzer}, title = {A Uniform Substitution Calculus for Differential Dynamic Logic}, booktitle = {CADE}, longbooktitle = {International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings}, year = {2015}, pages = {467-481}, doi = {10.1007/978-3-319-21401-6_32}, editor = {Amy P. Felty and Aart Middeldorp}, publisher = {Springer}, series = {LNCS}, volume = {9195}, eprint = {1503.01981} }

@INPROCEEDINGS{DBLP:conf/cade/FultonMQVP15, author = {Nathan Fulton and Stefan Mitsch and Jan-David Quesel and Marcus V{\"o}lp and Andr{\'e} Platzer}, title = {{KeYmaera X}: An Axiomatic Tactical Theorem Prover for Hybrid Systems}, booktitle = {CADE}, longbooktitle = {International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings}, year = {2015}, pages = {527--538}, doi = {10.1007/978-3-319-21401-6_36}, editor = {Amy P. Felty and Aart Middeldorp}, publisher = {Springer}, series = {LNCS}, volume = {9195}, }

@MISC{Peterson15, author = {Annika Peterson}, title = {Formal Verification of a Controlled Flight Between Two Robots: A Case Study}, howpublished = {Senior thesis, Carnegie Mellon University, Computer Science Department}, month = {May}, year = {2015}, school = {Carnegie Mellon University, Computer Science Department}, }

@ARTICLE{DBLP:journals/csur/MitschPRS15, author = {Stefan Mitsch and Andr{\'e} Platzer and Werner Retschitzegger and Wieland Schwinger}, title = {Logic-based Modeling Approaches for Qualitative and Hybrid Reasoning in Dynamic Spatial Systems}, journal = {{ACM} Comput. Surv.}, volume = {}, number = {}, pages = {}, year = {2015}, }

@ARTICLE{DBLP:journals/tocl/Platzer15, author = {Andr{\'e} Platzer}, title = {Differential Game Logic}, journal = {{ACM} Trans. Comput. Log.}, volume = {17}, number = {1}, year = {2015}, pages = {1:1--1:51}, doi = {10.1145/2817824}, issn = {1529-3785}, optnote = {Preprint at arXiv 1408.1980} }

@INPROCEEDINGS{DBLP:conf/emsoft/JeanninGKGSZP15, author = {Jean{-}Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Ryan Gardner and Aurora Schmidt and Erik Zawadzki and Andr{\'e} Platzer}, title = {Formal Verification of {ACAS X}, an Industrial Airborne Collision Avoidance System}, booktitle = {EMSOFT}, year = {2015}, pages = {127-136}, doi = {10.1109/EMSOFT.2015.7318268}, editor = {Alain Girault and Nan Guan}, longbooktitle = {2015 International Conference on Embedded Software, {EMSOFT} 2015, Amsterdam, The Netherlands, October 4-9, 2015}, publisher = {IEEE Press}, }

@INPROCEEDINGS{DBLP:conf/emsoft/ArechigaKDPK15, author = {Nikos Arechiga and James Kapinski and Jyotirmoy V. Deshmukh and Andr{\'e} Platzer and Bruce H. Krogh}, title = {Forward invariant cuts to simplify proofs of safety}, booktitle = {EMSOFT}, pages = {227-236}, year = {2015}, doi = {10.1109/EMSOFT.2015.7318278}, editor = {Alain Girault and Nan Guan}, longbooktitle = {2015 International Conference on Embedded Software, {EMSOFT} 2015, Amsterdam, The Netherlands, October 4-9, 2015}, publisher = {IEEE}, isbn = {978-1-4673-8079-9} }

@INPROCEEDINGS{DBLP:conf/itsc/MullerMP15, author = {Andreas M{\"u}ller and Stefan Mitsch and Andr{\'e} Platzer}, title = {Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems}, booktitle = {ITSC}, longbooktitle={Intelligent Transportation Systems (ITSC), 2015 IEEE 18th International Conference on}, year = {2015}, pages = {757-764}, doi = {10.1109/ITSC.2015.128}, keywords = {Automobiles, Contracts, Load modeling, Mathematical model, Roads, Safety}, }

@ARTICLE{DBLP:journals/sttt/JeanninGKSGMP16, author = {Jean{-}Baptiste Jeannin and Khalil Ghorbal and Yanni Kouskoulas and Aurora Schmidt and Ryan Gardner and Stefan Mitsch and Andr{\'e} Platzer}, title = {A Formally Verified Hybrid System for Safe Advisories in the Next-generation Airborne Collision Avoidance System}, journal = {STTT}, longjournal = {International Journal on Software Tools for Technology Transfer}, year = {2016}, volume = {}, number = {}, pages = {}, doi = {10.1007/s10009-016-0434-1}, url = {http://www.cs.cmu.edu/~aplatzer/pub/acasx-zones-long.pdf} }

@INPROCEEDINGS{DBLP:conf/vmcai/SogokonGJP16, author = {Andrew Sogokon and Khalil Ghorbal and Paul B. Jackson and Andr{\'e} Platzer}, title = {A Method for Invariant Generation for Polynomial Continuous Systems}, booktitle = {VMCAI}, year = {2016}, pages = {268-288}, doi = {10.1007/978-3-662-49122-5_13}, editor = {Barbara Jobstmann and K. Rustan M. Leino}, longbooktitle = {Verification, Model Checking, and Abstract Interpretation - 17th International Conference, {VMCAI} 2016, St. Petersburg, FL, USA, January 17-19, 2016, Proceedings}, series = {LNCS}, volume = {9583}, publisher = {Springer}, }

@INPROCEEDINGS{DBLP:conf/cpp/FultonP16, author = {Nathan Fulton and Andr{\'e} Platzer}, title = {A Logic of Proofs for Differential Dynamic Logic: Toward Independently Checkable Proof Certificates for Dynamic Logics}, booktitle = {Proceedings of the 2016 Conference on Certified Programs and Proofs, {CPP} 2016, St. Petersburg, FL, USA, January 18-19, 2016}, pages = {110-121}, year = {2016}, doi = {10.1145/2854065.2854078}, editor = {Jeremy Avigad and Adam Chlipala}, publisher = {{ACM}}, }

@ARITCLE{DBLP:journals/cl/GhorbalSP16, author = {Khalil Ghorbal and Andrew Sogokon and Andr{\'e} Platzer}, title = {A Hierarchy of Proof Rules for Checking Positive Invariance of Algebraic and Semi-Algebraic Sets}, journal = {Computer Languages, Systems and Structures}, year = {2015}, doi = {10.1016/j.cl.2015.11.003}, }

@ARTICLE{DBLP:journals/fmsd/MitschP16, author = {Stefan Mitsch and Andr{\'e} Platzer}, title = {{ModelPlex}: Verified Runtime Validation of Verified Cyber-Physical System Models}, journal = {Form. Methods Syst. Des.}, longjournal = {Formal Methods in System Design}, year = {2016}, volume = {}, number = {}, pages = {}, doi = {10.1007/s10703-016-0241-z}, issn = {0925-9856}, note = {Special issue of selected papers from RV'14}, }

@ARTICLE{DBLP:journals/jar/Platzer16, author = {Andr{\'e} Platzer}, title = {A Complete Uniform Substitution Calculus for Differential Dynamic Logic}, journal = {J. Autom. Reas.}, longjournal = {Journal of Automated Reasoning}, year = {2016}, volume = {}, number = {}, pages = {}, doi = {10.1007/s10817-016-9385-1}, }

@INPROCEEDINGS{DBLP:conf/cade/Platzer16, author = {Andr{\'e} Platzer}, title = {Logic \& Proofs for Cyber-Physical Systems}, booktitle = {IJCAR}, longbooktitle = {Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings}, year = {2016}, pages = {15-21}, doi = {10.1007/978-3-319-40229-1_3}, volume = {9706}, editor = {Nicola Olivetti and Ashish Tiwari}, publisher = {Springer}, series = {LNCS}, keywords = {logic, cyber-physical systems, multi-dynamical systems, differential dynamic logic, KeYmaera X}, abstract = {\emph{Cyber-physical systems} (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safety-critical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one? This paper highlights some of the most fascinating aspects of cyber-physical systems and their dynamical systems models, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. Because of the impact that they can have on the real world, CPSs deserve proof as safety evidence. \emph{Multi-dynamical systems} understand complex systems as a combination of multiple elementary dynamical aspects, which makes them natural mathematical models for CPS, since they tame their complexity by compositionality. The family of \emph{differential dynamic logics} achieves this compositionality by providing compositional logics, programming languages, and reasoning principles for CPS. Differential dynamic logics, as implemented in the theorem prover KeYmaera X, have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robot system for skull-base surgery. This combination of strong theoretical foundations with practical theorem proving challenges and relevant applications makes \emph{Logic for CPS} an ideal area for compelling and rewarding research.} }

@INPROCEEDINGS{DBLP:conf/ifm/MullerMRSP16, author = {Andreas M{\"u}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and Andr{\'e} Platzer}, title = {A Component-based Approach to Hybrid Systems Safety Verification}, booktitle = {IFM}, longbooktitle={Integrated Formal Methods - 12th International Conference, {IFM} 2016, Reykjavik, Iceland, June 1-4, 2016, Proceedings}, year = {2016}, pages = {441-456}, doi = {10.1007/978-3-319-33693-0_28}, editor = {Erika Abraham and Marieke Huisman}, series = {LNCS}, volume = {9681}, publisher = {Springer}, year = {2016}, }

@TECHREPORT{DBLP:conf/ifm/MullerMRSP16:TR, author = {Andreas M{\"u}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and Andr{\'e} Platzer}, title = {A Component-based Approach to Hybrid Systems Safety Verification}, number = {CMU-CS-16-100}, year = {2016}, month = {June}, institution = {School of Computer Science, Carnegie Mellon University}, address = {Pittsburgh, PA}, pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2016/CMU-CS-16-100.pdf} }

@MISC{FCPS16:videos, author = {Andr\'e Platzer}, title = {Foundations of Cyber-Physical Systems}, year = {2016}, howpublished = {Lecture Videos 15-424/624/824, Carnegie Mellon University}, }

@MISC{FCPS16, author = {Andr\'e Platzer}, title = {Foundations of Cyber-Physical Systems}, year = {2016}, howpublished = {Lecture Notes 15-424/624/824, Carnegie Mellon University}, url = {http://symbolaris.com/course/fcps16/fcps16.pdf} }

@ARTICLE{DBLP:journals/corr/abs-1605-00604, author = {Stefan Mitsch and Khalil Ghorbal and David Vogelbacher and Andr{\'e} Platzer}, title = {Formal Verification of Obstacle Avoidance and Navigation of Ground Robots}, journal = {CoRR}, volume = {abs/1605.00604}, year = {2016}, url = {http://arxiv.org/abs/1605.00604}, }

@INPROCEEDINGS{DBLP:conf/lics/LoosP16, author = {Sarah M. Loos and Andr{\'e} Platzer}, title = {Differential Refinement Logic}, booktitle = {LICS}, year = {2016}, pages = {}, doi = {}, longbooktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, July 5--8, 2016}, publisher = {ACM}, }Copyright of publications is with the publisher or author as indicated. Author's versions of papers are posted with permission of the publisher for your personal use. Not for redistribution or commercial purpose. Slides are copyright © by the author.

*All information and materials on this site are provided solely for informational purposes on an AS-IS basis, and any and all implied warranties are expressly disclaimed.*