Recent Publications

 

1 Recent Publications (since 2007)

[OS13]

E.-R. Olderog and Mani Swaminathan. Structural transformations for data-enriched real-time systems. In Einar Broch Johnsen and Luigia Petre, editors, Integrated Formal Methods (iFM), volume 7940 of Lecture Notes in Computer Science, pages 378-393. Springer-Verlag, 2013. [ bib | http ]

[AdBOdG12]

K. R. Apt, F. S. de Boer, E.-R. Olderog, and S. de Gouw. Verification of object-oriented programs: A transformational approach. J Computer System Sciences, 78:823-852, 2012. [ bib ]

[Old12]

E.-R. Olderog. Automatic verification of real-time systems with rich data - an overview. In Manindra Agrawal, S. Barry Cooper, and Angsheng Li, editors, Theory and Applications of Models of Computation (TAMC), volume 7287 of LNCS, pages 84-93. Springer, 2012. [ bib ]

[OW12]

E.-R. Olderog and R. Wilhelm. Turing und die Verifikation. Informatik-Spektrum, 35(4):271-279, 2012. [ bib ]

[SKO12]

M. Swaminathan, J.-P. Katoen, and E.-R. Olderog. Layered reasoning for randomized distributed algorithms. Formal Asp. Comput., 24(4-6):477-496, 2012. [ bib | http ]

[SM12]

T. Strazny and R. Meyer. An algorithmic framework for coverability in well-structured systems. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), pages 173-182. IEEE Computer Society Conference Publishing Services, June 2012. Best Paper Award of ACSD. [ bib | Abstract ]

[Lin12]

S. Linker. Translating structural process properties to petri net markings. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12), pages 82-91. IEEE Computer Society Conference Publishing Services, June 2012. [ bib | Abstract ]

[QP12]

Jan-David Quesel and André Platzer. Playing hybrid games with KeYmaera. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, Automated Reasoning, Sixth International Joint Conference, IJCAR 2012, Manchester, UK, Proceedings, volume 7364 of LNCS, pages 439-453. Springer, June 2012. The original publication is available at www.springerlink.com. [ bib | DOI | slides | .pdf | Abstract ]

[Str11]

Tim Strazny. Accelerating backward reachability analysis. In Paul Pettersson and Cristina Seceleanu, editors, Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11), pages 2-4. Mälardalen University Sweden, October 2011. Technical report 254/2011. [ bib | Abstract ]

[HLOR11]

M. Hilscher, S. Linker, E.-R. Olderog, and A.P. Ravn. An abstract model for proving safety of multi-lane traffic manoeuvres. In Shengchao Qin and Zongyan Qiu, editors, Int'l Conf. on Formal Engineering Methods (ICFEM), volume 6991 of Lecture Notes in Computer Science. Springer-Verlag, Oct. 2011. The original publication is available at www.springerlink.com. [ bib | .pdf | Abstract ]

[QFD11]

J.-D. Quesel, M. Fränzle, and W. Damm. Crossing the bridge between similar games. In Stavros Tripakis and Uli Fahrenberg, editors, Formal Modeling and Analysis of Timed Systems - 9th International Conference (FORMATS), Aalborg, Denmark, 21-23 September, 2011. Proceedings, volume 6919 of LNCS, pages 160-176. Springer, Sep. 2011. The original publication is available at www.springerlink.com. [ bib | slides | .pdf | Abstract ]

[FLOQ11]

Johannes Faber, Sven Linker, Ernst-Rüdiger Olderog, and Jan-David Quesel. Syspect - modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics, 5(1-2):117-137, 2011. ISSN 1673-7288. [ bib | http | Abstract ]

[Lin10]

Sven Linker. Diagrammatic specification of mobile real-time systems. In Ashok Goel, Mateja Jamnik, and N. Narayanan, editors, Diagrammatic Representation and Inference, volume 6170 of Lecture Notes in Computer Science, pages 316-318. Springer Berlin / Heidelberg, 2010. 10.1007/978-3-642-14600-8_40. [ bib | http ]

[Kem10]

Stephanie Kemper. Compositional construction of real-time dataflow networks. In Dave Clarke and Gul A. Agha, editors, Coordination Models and Languages, 12th International Conference, COORDINATION 2010, Amsterdam, The Netherlands, June 7-9, 2010. Proceedings, volume 6116 of Lecture Notes in Computer Science, pages 92-106. Springer, 2010. [ bib | DOI | .pdf ]

[Pla10]

André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg, 2010. [ bib | DOI | http ]

[HMO10]

J. Hoenicke, R. Meyer, and E.-R. Olderog. Kleene, rabin, and scott are available. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory (CONCUR), volume 6269 of Lecture Notes in Computer Science, pages 462-477. Springer, 2010. [ bib | http ]

[FJLS10]

Sibylle Fröschle, Petr Jančar, Slawomir Lasota, and Zdeněk Sawa. Non-interleaving bisimulation equivalences on basic parallel processes. Inf. Comput., 208(1):42-62, 2010. [ bib ]

[Fab10]

J. Faber. Verification Architectures: Compositional reasoning for real-time systems. In D. Méry and S. Merz, editors, Integrated Formal Methods, volume 6396 of Lecture Notes in Computer Science, pages 136-151. Springer, Heidelberg, 2010. This publication is available at SpringerLink. [ bib | DOI | .pdf | Abstract ]

[FIJSS10]

J. Faber, C. Ihlemann, S. Jacobs, and V. Sofronie-Stokkermans. Automatic verification of parametric specifications with complex topologies. In D. Méry and S. Merz, editors, Integrated Formal Methods, volume 6396 of Lecture Notes in Computer Science, pages 152-167. Springer, Heidelberg, 2010. This publication is available at SpringerLink. [ bib | DOI | .pdf | Abstract ]

[OS10]

E.-R. Olderog and M. Swaminathan. Layered composition for timed automata. In K. Chatterjee and T. A Henzinger, editors, Formal Modeling and Analysis of Timed Systems (FORMATS), volume 6246 of Lecture Notes in Computer Science, pages 228-242. Springer-Verlag, 2010. [ bib | http ]

[MS10]

R. Meyer and T. Strazny. Petruchio: From dynamic networks to nets. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010, volume 6174 of LNCS, pages 175-179. Springer-Verlag, 2010. [ bib | Abstract ]

[HOP10]

J. Hoenicke, E.-R. Olderog, and A. Podelski. Fairness for dynamic control. In J. Esparza and R. Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6015 of Lecture Notes in Computer Science, pages 251-265. Springer-Verlag, 2010. [ bib ]

[OP10]

E.-R. Olderog and A. Podelski. Explicit fair scheduling for dynamic control. In D. Dams, U. Hannemann, and M. Steffen, editors, Concurrency, Compositionality, and Correctness, volume 5930 of Lecture Notes in Computer Science, pages 96-117. Springer-Verlag, 2010. [ bib ]

[Kem09]

Stephanie Kemper. SAT-based Verification for Timed Component Connectors. Electr. Notes Theor. Comput. Sci., 255:103-118, 2009. [ bib | DOI | .pdf ]

[FG09]

Sibylle B. Fröschle and Daniele Gorla. Proceedings 16th international workshop on expressiveness in concurrency. CoRR, abs/0911.3189, 2009. [ bib ]

[CFL09]

Wojciech Czerwiński, Sibylle Fröschle, and SLasota. Partially-commutative context-free processes. In CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory, pages 259-273. Springer-Verlag, 2009. [ bib ]

[FS09b]

Sibylle Fröschle and Graham Steel. Analysing pkcs#11 key management apis with unbounded fresh data. pages 92-106, 2009. [ bib ]

[Fab09]

J. Faber. Verification architectures for real-time systems. In M. Mousavi and E. Sekerinski, editors, Proceedings of Formal Methods 2009 Doctoral Symposium, number 09-15 in CS-Report, Eindhoven University of Technology, pages 14-19, 2009. [ bib | http | .pdf ]

[OM09]

E.-R. Olderog and R. Meyer. Automata-theoretic verification based on counterexample specification. In V. Diekert, K. Weicker, and N. Weicker, editors, Informatik als Dialog zwischen Theorie und Anwendung, pages 217-225. Vieweg-Teubner, 2009. [ bib ]

[FS09a]

M. Fränzle and M. Swaminathan. Revisiting decidability and optimum reachability for multi-priced timed automata. In J. Ouaknine and F. Vaandrager, editors, Formal Modeling and Analysis of Timed Systems (FORMATS), volume 5813 of Lecture Notes in Computer Science, pages 149-163. Springer-Verlag, 2009. [ bib | http ]

[PQR09]

André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[PQ09]

André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. In Ana Cavalcanti and Karin Breitman, editors, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 9-12, 2009, Proceedings, volume 5885 of LNCS, pages 246-265, Heidelberg, 2009. Springer. (c) Springer-Verlag. [ bib | DOI | slides | .pdf | Abstract ]

[SJ09]

A. Schäfer and M. John. Conceptional modeling and analysis of spatio-temporal processes in biomolecular systems. In Markus Kirchberg and Sebastian Link, editors, Sixth Asia-Pacific Conference on Conceptual Modelling (APCCM 2009), Wellington, New Zealand, January 2009, volume 96 of CRPIT, pages 39-48. Australian Computer Society, 2009. [ bib ]

[Fr9]

Sibylle Fröschle. Adding branching to the strand space model. Electron. Notes Theor. Comput. Sci., 242(1):139-159, 2009. [ bib ]

[SFK08]

M. Swaminathan, M. Fränzle, and J-.P. Katoen. The surprising robustness of (closed) timed automata against clock-drift. In Giorgio Ausiello and Juhani Karhumäki, editors, IFIP International Conference on Theoretical Computer Science (IFIP TCS), volume 273 of International Federation for Information Processing, pages 537-553. Springer, 2008. [ bib | http ]

[AdBO09]

K. R. Apt, F. S. de Boer, and E.-R. Olderog. Verification of Sequential and Concurrent Programs, 3rd Edition. Texts in Computer Science. Springer-Verlag, 2009. 502 pp, ISBN 978-1-84882-744-8. [ bib ]

[OD08]

E.-R. Olderog and H. Dierks. Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press, 2008. ISBN 978-0-521-88333-7. For more information see: http://csd.informatik.uni-oldenburg.de/rt-book/. [ bib ]

[Old08]

E.-R. Olderog. Automatic verification of combined specifications. In G. Pu and V. Stolz, editors, Proc. of the 1st Internat. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2007), Macau, volume 207 of ENTCS, pages 3-16, April 2008. [ bib | www: | Abstract ]

[MORW08]

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, 20:161-204, 2008. [ bib | Abstract ]

[Sch08]

A. Schäfer. Beschreibung und Verifikation räumlicher und zeitlicher Eigenschaften mobiler Systeme. it - Information Technology, 50(5):324-326, 2008. http://it-Information-Technology.de. [ bib | DOI | .pdf | Abstract ]

[Pla08a]

André Platzer. Differential-algebraic dynamic logic for differential-algebraic programs. Journal of Logic and Computation, 2008. Accepted for publication. [ bib | DOI | .pdf | Abstract ]

[Pla08b]

André Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2):143-189, 2008. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[MFHR08]

R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. ISSN 0934-5043 (Print) 1433-299X (Online). [ bib | DOI | .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, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. (c) Springer-Verlag. [ bib | DOI | slides | .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 176-189. Springer, 2008. (c) Springer-Verlag. [ bib | DOI | .pdf | Abstract ]

[Mey08]

R. Meyer. On boundedness in depth in the π-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 ]

[MKS09]

R. Meyer, V. Khomenko, and T. Strazny. A practical approach to verification of mobile systems using net unfoldings. Fundamenta Informaticae, 94(3-4):439-471, 2009. Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper. [ 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, pages 327-347. Springer-Verlag, 2008. [ 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 | DOI | .pdf | Abstract ]

[JEP08]

Martin Johns, Björn Engelmann, and Joachim Posegga. Xssds: Server-side detection of cross-site scripting attacks. In ACSAC, pages 335-344, 2008. [ bib | DOI | http | Abstract ]

[Mey07]

R. Meyer. A Petri Net Semantics for π-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 ]

[Pla07a]

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 | DOI | 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 ]

[Pla07b]

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 | DOI | .pdf | Abstract ]

[FJSS07]

J. Faber, S. Jacobs, and V. 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 ]

[Pla07d]

André 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 | DOI | .pdf | Abstract ]

[Pla07c]

André 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 | DOI | .pdf | Abstract ]

[PC07]

André Platzer and Edmund 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 | DOI | .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]

Stephanie Kemper and André 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 | DOI | .pdf | Abstract ]

[FL09]

Sibylle Fröschle and SLasota. Normed processes, unique decomposition, and complexity of bisimulation equivalences. Electron. Notes Theor. Comput. Sci., 239:17-42, 2009. [ bib ]

[Pla07e]

André 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 | DOI | .pdf | Abstract ]