Recent Publications

 

1 Recent Publications (since 2007)

[Pla08]

André Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 2008. Accepted for publication.
[ bib | .pdf | Abstract ]

[MFHR08]

R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, pages 1-25, 2008. ISSN: 0934-5043 (Print) 1433-299X (Online).
[ bib | .pdf | Abstract ]

[PQ08a]

André Platzer and Jan-David Quesel. KeYmaera: A hybrid theorem prover for hybrid systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[PC08]

André Platzer and Edmund M. Clarke. Computing differential invariants of hybrid systems as fixedpoints. In Aarti Gupta and Sharad Malik, editors, Computer-Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pages 179-189. Springer, 2008. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[Mey08]

R. Meyer. On boundedness in depth in the pi-calculus. In Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008, volume 273 of IFIP. Springer-Verlag, 2008. To appear.
[ bib | Abstract ]

[MKS08]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. In Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008, volume 5062 of LNCS. Springer-Verlag, 2008. To appear.
[ bib | Abstract ]

[PQ08b]

André Platzer and Jan-David Quesel. Logical verification and systematic parametric analysis in train control. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pages 646-649. Springer, 2008. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[Mey07]

R. Meyer. A Petri Net Semantics for pi-Calculus Verification. In Dagstuhl ''zehn plus eins'', pages 76-77. Verlagshaus Mainz GmbH Aachen, 2007.
[ bib ]

[FL07]

Sibylle Fröschle and Slawomir Lasota. Causality versus true-concurrency. Theoretical Computer Science, 386(3):169-187, 2007.
[ bib ]

[BPD⁺07]

B. Becker, A. Podelski, W. Damm, M. Fränzle, E.-R. Olderog, and R. Wilhelm. SFB/TR 14 AVACS - Automatic Verification and Analysis of Complex Systems. it - Information Technology, 49(2):118-126, 2007. See also http://www.avacs.org.
[ bib ]

[Sch07b]

A. Schäfer. PhD Abstract: Specification and Verification of Mobile Real-Time Systems. Bulletin of the EATCS, 92:193-195, 2007.
[ bib | .pdf ]

[Sch07c]

A. Schäfer. Spezifikation und Verifikation mobiler Realzeitsysteme. In D. Wagner, editor, Ausgezeichnete Informatikdissertationen 2007, GI-Edition-Lecture Notes in Informatics (LNI), pages 169-177. Gesellschaft für Informatik, 2007.
[ bib | .pdf ]

[MORW07]

M. Möller, E.-R. Olderog, H. Rasch, and H. Wehrheim. Integrating a formal method into a software engineering process with UML and Java. Formal Apsects of Computing, 2007. To appear.
[ bib | Abstract ]

[Pla07d]

André Platzer. Combining deduction and algebraic constraints for hybrid system analysis. In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, volume 259, pages 164-178. CEUR-WS.org, 2007. CEUR Workshop Proceedings.
[ bib | .pdf | Abstract ]

[DMO⁺07]

Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken, and Boris Wirtz. Automating verification of cooperation, control, and design in traffic applications. In Cliff Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169. Springer-Verlag, 2007. (c) Springer-Verlag.
[ bib | Abstract ]

[BOS07]

D. Basin, E.-R. Olderog, and P.E. Sevinç. Specifying and analyzing security automata using CSP-OZ. In Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007), pages 70-81. ACM Press, March 2007.
[ bib | Abstract ]

[Frö07]

Sibylle Fröschle. The insecurity problem: tackling unbounded data. In IEEE Computer Security Foundations Symposium 2007. IEEE Computer Society, 2007.
[ bib | Abstract ]

[Pla07e]

André Platzer. Differential dynamic logic for verifying parametric hybrid systems. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pages 216-232. Springer-Verlag, 2007. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[FJSS07]

Johannes Faber, Swen Jacobs, and Viorica Sofronie-Stokkermans. Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In J. Davies and J. Gibbons, editors, Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 233-252. Springer-Verlag, July 2007.
[ bib | .pdf | Abstract ]

[Brü07]

I. Brückner. Slicing Concurrent Real-Time System Specifications for Verification. In J. Davies and J. Gibbons, editors, Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 54-74. Springer-Verlag, July 2007.
[ bib | .pdf | Abstract ]

[BDFW07]

I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim. Slicing Abstractions. In F. Arbab and M. Sirjani, editors, FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering, volume 4767 of Lecture Notes in Computer Science, pages 17-32. Springer, April 2007.
[ bib | .pdf | Abstract ]

[Pla07b]

A. Platzer. A temporal dynamic logic for verifying hybrid system invariants. In S. Artemov and A. Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pages 457-471. Springer, 2007. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[Pla07a]

A. Platzer. Differential logic for reasoning about hybrid systems. In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 746-749. Springer-Verlag, 2007. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[PC07]

A. Platzer and E. M. Clarke. The image computation problem in hybrid systems model checking. In A. Bemporad, A. Bicchi, and G. Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pages 473-486. Springer-Verlag, 2007. (c) Springer-Verlag.
[ bib | .pdf | Abstract ]

[Sch07a]

A. Schäfer. Axiomatisation and decidability of multi-dimensional duration calculus. TIME'05 special issue of Information and Computation, 205(1), 2007. DOI 10.1016/j.ic.2006.08.005.
[ bib | Abstract ]

[KP07]

S. Kemper and A. Platzer. Sat-based abstraction refinement for real-time systems. In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, volume 182 of ENTCS, pages 107-122, 2007.
[ bib | .pdf | Abstract ]

[Pla07c]

A. Platzer. Towards a hybrid dynamic logic for hybrid dynamic systems. In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, and Jørgen Villadsen, editors, Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, volume 174 of ENTCS, pages 63-77, Jun 2007.
[ bib | .pdf | Abstract ]