Publications

Theses

  • Steffen, M. (2006). Object-Connectivity and Observability for Class-Based, Object-Oriented Languages [Habilitation thesis]. Technische Faktultät der Christian-Albrechts-Universität zu Kiel.
  • Steffen, M. (1998). Polarized Higher-Order Subtyping [PhD thesis]. Dissertation, Universität Erlangen-Nürnberg.
  • Siegel, M., & Steffen, M. (1992). Vollständigkeit eines Beweissystems für Hennessy-Milner-Logik mit Rekursion [Diplomarbeit]. Friedrich-Alexander-Universität, Erlangen-Nürnberg.
  • Siegel, M., & Steffen, M. (1991). Ein Beweissystem für Hennessy-Milner-Logik mit Rekursion [Studienarbeit]. Friedrich-Alexander-Universität, Erlangen-Nürnberg.

Journal publications

  • Fava, D. S., & Steffen, M. (2020). Ready, Set, Go!: Data-Race Detection and the Go Language. Science of Computer Programming, 195, 102473. https://doi.org/10.1016/j.scico.2020.102473
  • Fava, D., Steffen, M., & Stolz, V. (2019). Operational Semantics of a Weak Memory Model with Channel Synchronization. Journal of Logical and Algebraic Methods in Programming, 103, 1–30. https://doi.org/10.1016/j.jlamp.2018.10.004
  • Gkolfi, A., Din, C. C., Johnsen, E. B., Kristensen, L. M., Steffen, M., & Yu, I. C. (2019). Translating Active Objects into Colored Petri Nets for Communication Analysis. Science of Computer Programming, 181, 1–26. https://doi.org/10.1016/j.scico.2019.04.002
  • Johnsen, E. B., Steffen, M., & Stumpf, J. B. (2018). Virtually Timed Ambients: A Calculus of Nested Virtualization. Journal of Logic and Algebraic Methods in Programming, 94, 109–127. https://doi.org/10.1016/j.jlamp.2017.10.001
  • Pun, K. I., Steffen, M., & Stolz, V. (2016). Effect-Polymorphic Behaviour Inference for Deadlock Checking. Journal of Logic and Algebraic Methods in Programming, 85(6). https://doi.org/10.1016/j.jlamp.2016.05.003
  • Ábrahám, E., Mai Thuong Tran, T., & Steffen, M. (2014). Observable interface behavior and inheritance. Mathematical Structures in Computer Science (Special Issue on Behavioral Types), 26, 561–605. https://doi.org/10.1017/S0960129514000255
  • Pun, K. I., Steffen, M., & Stolz, V. (2014). Deadlock Checking by Data Race Detection. Journal of Logic and Algebraic Methods in Programming. https://doi.org/10.1016/j.jlamp.2014.07.003
  • Hansen, H. A., Schneider, G., & Steffen, M. (2013). Reachability Analysis of Complex Planar Hybrid Systems. Science of Computer Programming, 78(12), 2511–2536. https://doi.org/10.1016/j.scico.2013.02.007
  • de Boer, F., Grabe, I., & Steffen, M. (2012). Termination Detection for Active Objects. Journal of Logic and Algebraic Programming, 81(4), 541–557. https://doi.org/10.1016/j.jlap.2012.03.009
  • Johnsen, E. B., Mai Thuong Tran, T., Owe, O., & Steffen, M. (2012). Safe Locking for Multi-Threaded Java with Exceptions. Journal of Logic and Algebraic Programming, Special Issue of Selected Contributions to NWPT’10. https://doi.org/10.1016/j.jlap.2011.11.002
  • Pun, K. I., Steffen, M., & Stolz, V. (2012). Deadlock Checking by a Behavioral Effect System for Lock Handling. Journal of Logic and Algebraic Programming, 81(3), 331–354. https://doi.org/10.1016/j.jlap.2011.11.001
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2011). Incremental Reasoning with Lazy Behavioral Subtyping for Multiple Inheritance. Science of Computer Programming, 76, 915–941. https://doi.org/10.1016/j.scico.2010.09.006
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2010). Lazy Behavioral Subtyping. Journal of Logic and Algebraic Programming, 79(7), 578–607. https://doi.org/10.1016/j.jlap.2010.07.008
  • Ábrahám, E., Grabe, I., Grüner, A., & Steffen, M. (2009). Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming, 78(7), 491–518 (28 pages). https://doi.org/10.1016/j.jlap.2009.01.001
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2008). A Deductive Proof System for Multithreaded Java with Exceptions. Fundamenta Informaticae, 82(4), 391–463 (73 pages). https://doi.org/10.5555/1366982.1366987
  • Ábrahám, E., Grüner, A., & Steffen, M. (0AD). Heap-Abstraction for an Object-Oriented Calculus with Thread Classes. Journal of Software and Systems Modelling (SoSyM), 7(2), 177–208 (32 pages). https://doi.org/10.1007/s10270-007-0065-9
  • Ábrahám, E., Grüner, A., & Steffen, M. (3AD). Abstract Interface Behavior of Object-Oriented Languages with Monitors. Theory of Computing Systems, 43(3-4), 322–361 (40 pages). https://doi.org/10.1007/s00224-007-9047-0
  • Ábrahám, E., Herbstritt, M., Becker, B., & Steffen, M. (2007). Bounded Model Checking with Parametric Data Structures. Electronic Notes in Theoretical Computer Science, 174(3), 3–16 (14 pages). https://doi.org/10.1016/j.entcs.2006.12.019
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2005). An Assertion-Based Proof System for Multithreaded Java. Theoretical Computer Science, 331, 251–290 (40 pages). https://doi.org/10.1016/tcs.2004.09.019
  • Dams, D., Lakhnech, Y., & Steffen, M. (2002). Iterating Transducers. Journal of Logic and Algebraic Programming, Special Issue on Model Checking, 52–53, 109–127 (19 pages). https://doi.org/10.1016/S1567-8326(02)00025-5
  • Hofmann, M., Naraschewski, W., Steffen, M., & Stroup, T. (1998). Inheritance of Proofs. Theory and Practice of Object Systems (Tapos), Special Issue on the Third Workshop on Foundations Of Object-Oriented Languages (FOOL 3, LICS and Federated Logic Conferences Workshop), July 1996, 4(1), 51–69 (19 pages). https://doi.org/10.1002/(SICI)1096-9942(1998)4:1<51::AID-TAPO4>3.0.CO;2-A
  • Pierce, B. C., & Steffen, M. (1997). Higher-Order Subtyping. Theoretical Computer Science, 176(1,2), 235–282 (48 pages). https://doi.org/10.1016/S0304-3975(96)00096-5

Submitted for publication

  • Luteberget, B., Claessen, K., Johansen, C., & Steffen, M. (2019, May). Capacity Analysis for Railway Construction using SAT modulo Discrete Event Simulation. Submitted.
  • Pun, K. I., Steffen, M., Stolz, V., Wickert, A.-K., Bodden, E., & Eichberg, M. (2017). Gotcha: Static Taint Analysis for Go. Journal of Logic and Algebraic Methods in Programming.

Papers

  • Johnsen, E. B., Steffen, M., & Stumpf, J. B. (2020). Assumption-Commitment Type System for Resource Management in Virtually Timed Ambients. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation (ISOLA’20). 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part I (Vol. 11476, pp. 103–121). Springer Verlag. https://doi.org/10.1007/978-3-030-61362-4_6
  • Fava, D., & Steffen, M. (2019). Ready, Set, Go! Data-Race Detection and the Go Language. Proceedings of the Brazilian Symposium on Formal Methods (SBMF). http://arxiv.org/abs/1910.12643
  • Johnsen, E. B., Steffen, M., Stumpf, J. B., & Tveito, L. (2019). Resource-aware virtually timed ambients. In C. A. Furia & K. Winter (Eds.), Proceedings of the International Conference on integrated Formal Methods (iFM 2018) (Vol. 11023). Springer Verlag. https://doi.org/10.1007/978-3-319-98938-9_12
  • Luteberget, B., Johansen, C., & Steffen, M. (2019). Optimization and Synthesis of Railway Signalling Layout from Local Capacity Specifications. In M. H. ter Beek, A. McIver, & J. N. Oliveira (Eds.), Accepted for publication in FM’19, Porto (Vol. 11800, pp. 121–137). Springer Verlag. https://doi.org/https://doi.org/10.1007/978-3-030-30942-8_9
  • Fava, D., Steffen, M., & Stolz, V. (2018). Operational Semantics of a Weak Memory Model with Channel Synchronization. In K. Havelund, J. Peleska, B. Roscoe, & E. de Vink (Eds.), International Symposium on Formal Methods (Vol. 10951, pp. 258–276). Springer International Publishing. https://doi.org/10.1007/978-3-319-95582-7_15
  • Johnsen, E. B., Steffen, M., Stumpf, J. B., & Tveito, L. (2018, September). An Analysis Tool for Models of Virtualized Systems. Proceedings of the Norsk Informatikk Konferanse (NIK’18).
  • Johnsen, E. B., Steffen, M., Stumpf, J. B., & Tveito, L. (2018). Checking Modal Contracts for Virtually Timed Ambients. In B. Fischer & T. Uustalu (Eds.), Proceedings of the 15th International Colloquium on Theoretical Aspects of Computing — ICTAC 2018, Stellenbosch, South Africa, October 16–19 (Vol. 11187, pp. 252–272). Springer Verlag. https://doi.org/10.1007/978-3-030-02508-3_14
  • Gkolfi, A., Din, C. C., Johnsen, E. B., and Lars Michael Kristensen, Steffen, M., & Yu, I. C. (2017). Translating Active Objects into Colored Petri Nets for Communication Analysis. In M. Dastani & M. Sirjani (Eds.), Proceedings of Fundamentals of Software Engineering (FSEN 2017) (Vol. 10522, pp. 84–99). Springer Verlag. https://doi.org/10.1007/978-3-319-68972-2_6
  • Johnsen, E. B., Steffen, M., & Stumpf, J. B. (2017). A Calculus of Virtually Timed Ambients. In P. James & M. Roggenbach (Eds.), Recent Trends in Algebraic Development Techniques. Proceedings of the 23rd International Workshop, WADT 2016, Gregynog, UK, September 21 - 24, 2016, Revised Selected Papers (Vol. 10644). Springer Verlag. https://doi.org/10.1007/978-3-319-72044-9_7
  • Bodden, E., Pun, K. I., Steffen, M., Stolz, V., & Wickert, A.-K. (2016). Information Flow Analysis for Go. In T. Margaria & B. Steffen (Eds.), 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA’16) (Vol. 9952, pp. 431–445). Springer Verlag. https://doi.org/10.1007/978-3-319-47166-2_30
  • Johnsen, E. B., Pun, K. I., Steffen, M., Lizeth, S., Steffen, M., & Yu, I. C. (2016). Meeting Deadlines, Elastically. In L. Petre & E. Sekerinski (Eds.), From Action Systems to Distributed System: The Refinement Approach (pp. 99–111). CRC press. https://doi.org/10.1201/b20053-18
  • Li, J., Qeriqi, A., & Yu, M. S. I. C. (2016). Automatic Translation of FBD-PLC-programs to NuSMV for Model Checking Safety-Critical Control Systems. Proceedings of the Norsk Informatikkonferanse NIK’16.
  • Luteberget, B., Johansen, C., Feyling, C., & Steffen, M. (2016). Rule-Based Incremental Verification Tools Applied to Railway Designs and Regulations. In J. Fitzgerald, C. H. C, S. Gnesi, A. Philippou, M. Butler, & W. Schulte (Eds.), Proceedings of the International Symposium on Formal Methods (FM 2016) (Vol. 9995, pp. 772–778). Springer Verlag. https://doi.org/10.1007/978-3-319-48989-6_49
  • Luteberget, B., Johansen, C., & Steffen, M. (2016). Rule-based Consistency Checking of Railway Infrastructure Designs. In E. Ábrahám & M. Huisman (Eds.), Proc. of the International Conference on integrated Formal Methods (iFM 2016) (Vol. 9681, pp. 491–507). Springer Verlag. https://doi.org/10.1007/978-3-319-33693-0_31
  • Rosenberg, C. M., Steffen, M., & Stolz, V. (2016). Leveraging DTrace for Runtime Verification. In C. Sánchez (Ed.), Proceedings of the 16th International Conference on Runtime Verification, RV 2016, Madrid, Spain, September 23-30, 2016 (Vol. 10012, pp. 318–332). Springer Verlag. https://doi.org/10.1007/978-3-319-46982-9_20
  • Steffen, M. (2016). A Small-Step Semantics of a Concurrent Calculus With Goroutines and Deferred Functions. In E. Ábrahám, M. Bonsangue, & E. B. Johnsen (Eds.), Theory and Practice of Formal Methods. Essays Dedicated to Frank de Boer on the Occasion of his 60th Birthday (Festschrift) (Vol. 9660, pp. 393–406). Springer Verlag. https://doi.org/10.1007/978-3-319-30734-3_26
  • Pun, K. I., Steffen, M., & Stolz, V. (2014). Behaviour Inference for Deadlock Checking. Proceeding of the 8th International Symposium On Theoretical Aspects of Software Engineering (TASE’14), 106–113. https://doi.org/10.1109/TASE.2014.23
  • Pun, K. I., Steffen, M., & Stolz, V. (2014). Effect-Polymorphic Behaviour Inference for Deadlock Checking. In D. Giannakopoulou & G. Salaün (Eds.), Proceedings of SEFM’14 (Vol. 8702, pp. 50–64). Springer Verlag. https://doi.org/10.1007/978-3-319-10431-7_5
  • de Boer, F. S., Bravetti, M., Grabe, I., Lee, M., Steffen, M., & Zavattaro, G. (2013). A Petri Net based Analysis of Deadlock for Active Objects and Futures. In C. S. Pasareanu & G. Salaün (Eds.), Revised Selected Papers of the 9th International Workshop on Formal Aspects of Component Software (FACS 2012) (Vol. 7684, pp. 110–127). Springer Verlag. https://doi.org/10.1007/978-3-642-35861-6_7
  • Pun, K. I., Steffen, M., & Stolz, V. (2013). Deadlock Checking by Data Race Detection. Proceedings of the 5th IPM International Conference On Fundamentals of Software Engineering (FSEN’13), 8161, 34–50. https://doi.org/10.1007/978-3-642-40213-5_3
  • Mai Thuong Tran, T., Steffen, M., & Truong, H. (2013). Compositional Static Analysis for Implicit Join Synchronization in a Transactional Setting. In G. Eleftherakis, M. Hinchey, & M. Holcombe (Eds.), Proceedings of SEFM’13 (Vol. 8137, pp. 212–228). Springer Verlag. https://doi.org/10.1007/978-3-642-40561-7_15
  • Hansen, H. A., Schneider, G., & Steffen, M. (2012). Reachability Analysis of Planar Autonomous Systems. Proceedings of the International Conference on Foundations of Software Engineering (Theory and Practice) (FSEN’11), 7141, 206–220. https://doi.org/10.1007/978-3-642-29320-7_14
  • Johnsen, E. B., Mai Thuong Tran, T., Owe, O., & Steffen, M. (2012). Safe Locking for Multi-Threaded Java. Proceedings of the International Conference on Foundations of Software Engineering (Theory and Practice) (FSEN’11), 7141, 158–173. https://doi.org/10.1007/978-3-642-29320-7_11
  • Xuan, T. V., Anh, H. T., Mai Thuong Tran, T., & Steffen, M. (2012). A Type System for Finding Upper Resource Bounds of Multi-Threaded Programs with Nested Transactions. ACM Proceedings of the 3rd ACM International Symposium On Information and Communication Technology SoICT, 20–31. https://doi.org/10.1145/2350716.2350722
  • Johnsen, E. B., Hähnle, R., Schäfer, J., Schlatte, R., & Steffen, M. (2011). ABS: A Core Language For Abstract Behavioral Specification. In B. K. Aichernig, F. S. de Boer, & M. M. Bonsangue (Eds.), Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010, Selected Papers (Vol. 6957, pp. 142–164). Springer Verlag. https://doi.org/10.1007/978-3-642-25271-6_8
  • Mai Thuong Tran, T., & Steffen, M. (2011). Design Issues in Concurrent Object-Oriented Languages and Observability. Proceedings of the Third International Conference On Knowledge and Systems Engineering (KSE 2011), Hanoi 14th-17th Oct, 2011, 135–142. https://doi.org/10.1109/KSE.2011.28
  • Grabe, I., Jaghoori, M. M., Aichernig, B., Blechmann, T., de Boer, F., Griesmayer, A., Johnsen, E. B., Klein, J., Küppelholz, S., Kyas, M., Leister, W., Schlatte, R., Stam, A., Steffen, M., Tschirner, S., Xuedong, L., & Yi, W. (2010). Credo Methodology. Modeling and Analyzing a Peer-to-Peer System in Credo. In V. Stolz & E. B. Johnsen (Eds.), Special Issue for the proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software, 2009, Malaysia. Elsevier Science Publishers. https://doi.org/10.1016/j.entcs.2010.08.047
  • Grabe, I., Kyas, M., Steffen, M., & B. Torjusen, A. (2010). Executable Interface Specifications for Testing Asynchronous Creol Components. In F. Arbab & M. Sirjani (Eds.), FSEN (Vol. 5961, pp. 324–339 (15 pages). Springer Verlag. https://doi.org/10.1007/978-3-642-11623-0_19
  • Mai Thuong Tran, T., Owe, O., & Steffen, M. (2010). Safe Typing for Transactional vs. Lock-Based Concurrency in Multi-Threaded Java. In S. B. Pham, T.-H. Hoang, B. McKay, & K. Hirota (Eds.), Proceedings of the Second International Conference on Knowledge and Systems Engineering, KSE 2010 (pp. 188–193). IEEE Computer Society. https://doi.org/10.1109/KSE.2010.9
  • Mai Thuong Tran, T., & Steffen, M. (2010). Safe Commits for Transactional Featherweight Java. In D. Méry & S. Merz (Eds.), Proceedings of the 8th International Conference on Integrated Formal Methods (iFM 2010) (Vol. 6396, pp. 290–304). Springer Verlag. https://doi.org/10.1007/978-3-642-16265-7_21
  • Owe, O., Steffen, M., & Torjusen, A. (2010). Model Testing Asynchronously Communicating Objects using Modulo AC Rewriting. Proceedings of the 6th Workshop on Model-Based Testing MBT’10 (ETAPS Satellite Workshop), 68–84. https://doi.org/10.1016/j.entcs.2010.12.015
  • de Boer, F. S., Bonsangue, M. M., Grüner, A., & Steffen, M. (2009). Java Test Driver Generation from Object-Oriented Interaction Traces. Electronic Notes in Theoretical Computer Science, 243, 33–47 (15 pages). https://doi.org/10.1016/j.entcs.2009.07.004
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2009). Encapsulating Lazy Behavioral Subtyping. Specification, Transformation, Navigation. Festschrift Dedicated to Bernd Krieg-Brückner on the Occasion Of His 60th Birthday, 52–67 (16 pages).
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2009). Incremental Reasoning for Multiple Inheritance. Proceedings of the 7th International Conference On Integrated Formal Methods (IFM’09), Düsseldorf, Germany, 16 – 19 February, 2009, 5423, 215–230. https://doi.org/10.1007/978-3-642-00255-7_15
  • Grabe, I., Jaghoori, M. M., Aichernig, B., Blechmann, T., de Boer, F., Griesmayer, A., Johnsen, E. B., Klein, J., Küppelholz, S., Kyas, M., Leister, W., Schlatte, R., Stam, A., Steffen, M., Tschirner, S., Xuedong, L., & Yi, W. (2009). Credo Methodology. In M. M. Bonsangue, F. S. de Boer, S. Hallerstede, & M. Leuschel (Eds.), Proceedings of the 8th International Symposium on Formal Methods for Components and Objects, FMCO 2009, Selected Papers (Vol. 6286, pp. 41–69). Springer Verlag. https://doi.org/10.1007/978-3-642-17071-3
  • de Boer, F. S., Bonsangue, M. M., Grüner, A., & Steffen, M. (2008, November). Automated Test Driver Generation for Java Components. Netherland’s Testing Day “TestDag’08”, Delft.
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2008). Lazy Behavioral Subtyping. In J. Cuellar, T. Maibaum, & K. Sere (Eds.), Proceedings of the 15th International Symposium on Formal Methods (FM’08) (Vol. 5014, pp. 52–67 (16 pages). Springer Verlag. https://doi.org/10.1007/978-3-540-68237-0_6
  • Owe, O., Schneider, G., & Steffen, M. (2007). Components, Objects, and Contracts. Sixth International Workshop on Specification And Verification of Component-Based Systems, Sept. 3–4, 2007, Cavtat, Croatia, 95–98. https://doi.org/10.1145/1292316.1292328
  • Ábrahám, E., Herbstritt, M., Becker, B., & Steffen, M. (2006, January). Memory-Aware Bounded Model Checking for Linear Hybrid Systems. Proceedings of the 9th. Workshop for “Methoden Und Beschreibungssprachen Zur Modellierung Und Verifikation Von Schaltungen Und Systemen” (MBMV06).
  • Ábrahám, E., Grüner, A., & Steffen, M. (2006). Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes (Extended Abstract). In A. Beckmann, U. Berger, B. Löwe, & J. V. Tucker (Eds.), Logical Approaches to Computational Barriers: CiE 2006 (Vol. 3988, pp. 1–10 (10 pages). Springer Verlag. https://doi.org/10.1007/11780342_1
  • Ábrahám, E., Grüner, A., & Steffen, M. (2006). Abstract Interface Behavior of Object-Oriented Languages with Monitors. In R. Gorrieri & H. Wehrheim (Eds.), FMOODS ’06 (Vol. 4037, pp. 218–232 (15 pages). Springer Verlag. https://doi.org/10.1007/s00224-007-9047-0
  • Ábrahám, E., de Boer, F. S., Bonsangue, M. M., Grüner, A., & Steffen, M. (2005). Observability, Connectivity, and Replay in a Sequential Calculus of Classes. In M. Bonsangue, F. S. de Boer, W.-P. de Roever, & S. Graf (Eds.), Proceedings of the Third International Symposium on Formal Methods for Components and Objects (FMCO 2004) (Vol. 3657, pp. 296–316 (21 pages). Springer Verlag. https://doi.org/10.1007/11561163_13
  • Ábrahám, E., Becker, B., Klaedke, F., & Steffen, M. (2005). Optimizing Bounded Model Checking for Linear Hybrid Systems. In R. Cousot (Ed.), Proceedings of the 6th International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI 2005) (Vol. 3385, pp. 396–412 (17 pages). Springer Verlag. https://doi.org/10.1007/978-3-540-30579-8_26
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2005). Inductive Proof Outlines for Exceptions in Multithreaded Java. In F. Arbab & M. Sirjani (Eds.), FSEN ’05: IPM International Conference on Foundations of Software Engineering (Theory and Practice). Oct. 1 – 3, 2005) (Vol. 159, pp. 281–297 (17 pages). Elsevier Science Publishers. https://doi.org/10.1016/j.entcs.2005.12.072
  • de Boer, F. S., Bonsangue, M. M., Steffen, M., & Ábrahám, E. (2005). A Fully Abstract Trace Semantics for UML Components. In M. Bonsangue, F. S. de Boer, W.-P. de Roever, & S. Graf (Eds.), Proceedings of the Third International Symposium on Formal Methods for Components and Objects (FMCO 2004) (Vol. 3657, pp. 49–69 (21 pages). Springer Verlag. https://doi.org/10.1007/11561163_3
  • Fecher, H., & Steffen, M. (2005). Characteristic μ-Calculus Formulas for Underspecified Transition Systems. Proceedings of the 11th International Workshop On Expressiveness in Concurrency (Express 04), 30 August, 2004, London, Great Britain. 13 Pages, 128(2). https://doi.org/10.1016/j.entcs.2004.11.031
  • Ábrahám, E., Bonsangue, M. M., de Boer, F. S., & Steffen, M. (2004). Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes. ICTAC’04, 3407, 37–51 (15 pages). https://doi.org/10.1007/978-3-540-31862-0_5
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2004). A Compositional Operational Semantics for Java_MT. In N. Derschowitz (Ed.), International Symposium on Verification (Theory and Practice), July 2003 (Vol. 2772, pp. 290–303 (14 pages). Springer Verlag. https://doi.org/10.1007/978-3-540-39910-0_13
  • Ioustinova, N., Sidorova, N., & Steffen, M. (2004). Synchronous Closing and Flow Analysis for Model Checking Timed Systems. In M. Bonsangue, F. S. de Boer, W.-P. de Roever, & S. Graf (Eds.), Proceedings of the Second International Symposium on Formal Methods for Components and Objects (FMCO 2003) (Vol. 3188, pp. 292–313 (22 pages). Springer Verlag. https://doi.org/10.1007/978-3-540-30101-1_14
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2003). Inductive Proof-Outlines for Monitors in Java. In E. Najm, U. Nestmann, & P. Stevens (Eds.), FMOODS ’03 (Vol. 2884, pp. 155–169 (15 pages). Springer Verlag. https://doi.org/10.1007/978-3-540-39958-2_11
  • Ábrahám-Mumm, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2003). A Tool-Supported Proof System for Monitors in Java. In M. M. Bonsangue, F. S. de Boer, W.-P. de Roever, & S. Graf (Eds.), FMCO 2002 (Vol. 2852, pp. 1–32 (33 pages). Springer Verlag. https://doi.org/10.1007/978-3-540-39656-7_1
  • Ábrahám-Mumm, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2002). Verification for Java’s Reentrant Multithreading Concept. In M. Nielsen & U. H. Engberg (Eds.), Proceedings of FoSSaCS 2002 (Vol. 2303, pp. 4–20 (17 pages). Springer Verlag. https://doi.org/10.1007/3-540-45931-6_2
  • Ioustinova, N., Sidorova, N., & Steffen, M. (2002). Abstraction and Flow Analysis for Model Checking Open Asynchronous Systems. Proceedings of the 9th Asia-Pacific Software Engineering Conference (APSEC 2002, 4.–6. December 2002, Gold Coast, Queensland, Australia, 227–235 (9 pages). https://doi.org/10.1109/APSEC.2002.1182992
  • Ioustinova, N., Sidorova, N., & Steffen, M. (2002). Closing Open SDL-Systems for Model Checking with DT Spin. In L.-H. Eriksson & P. A. Lindsay (Eds.), Proceedings of Formal Methods Europe: Formal Methods – Getting IT Right (FME’02) (Vol. 2391, pp. 531–548 (18 pages). Springer Verlag. https://doi.org/10.1007/3-540-45614-7_30
  • Sidorova, N., & Steffen, M. (2002). Synchronous Closing of Timed SDL Systems for Model Checking. In A. Cortesi (Ed.), Proceedings of the 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2002 (Vol. 2294, pp. 79–93 (15 pages). Springer Verlag. https://doi.org/10.1007/3-540-47813-2_6
  • Ábrahám-Mumm, E., Hannemann, U., & Steffen, M. (2001). Assertion-Based Analysis of Hybrid Systems with PVS. In R. Moreno-Díaz & B. Buchberger (Eds.), Computer Aided Systems Theory (EUROCAST 2001), Selected and revised papers (Vol. 2178, pp. 94–109 (16 pages). Springer Verlag. https://doi.org/10.1007/3-540-45654-6_8
  • Ábrahám-Mumm, E., Hannemann, U., & Steffen, M. (2001). Verification of Hybrid Systems: Formalization and Proof Rules in PVS. Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2001). https://doi.org/10.1109/ICECCS.2001.930163
  • Dams, D., Lakhnech, Y., & Steffen, M. (2001). Iterating Transducers. In G. Berry, H. Comon, & A. Finkel (Eds.), Proceedings of the 13th International Conference on Computer-Aided Verification, CAV ’01 (Vol. 2102, pp. 286–297 (12 pages). Springer Verlag. https://doi.org/10.1007/3-540-44585-4_27
  • Sidorova, N., & Steffen, M. (2001). Embedding Chaos. In P. Cousot (Ed.), Proceedings of the 8th International Static Analysis Symposium, SAS ’01 (Vol. 2126, pp. 319–334 (15 pages). Springer Verlag. https://doi.org/10.1007/3-540-47764-0_18
  • Sidorova, N., & Steffen, M. (2001). Verifying Large SDL-Specifications using Model Checking. In R. Reed & J. Reed (Eds.), Proceedings of the 10th International SDL Forum SDL 2001: Meeting UML (Vol. 2078, pp. 403–416 (14 pages). Springer Verlag. https://doi.org/10.1007/3-540-48213-X_25
  • Sidorova, N., & Steffen, M. (2000). Verification of a Wireless ATM Medium-Access Protocol. Proceedings of the 7th Asia-Pacific Software Engineering Conference (APSEC 2000), 5.–8. December 2000, Singapore, 84–91 (8 pages). https://doi.org/10.1109/APSEC.2000.896686
  • Stahl, K., Baukus, K., Lakhnech, Y., & Steffen, M. (1999). Divide, Abstract, and Model-Check. In D. Dams, R. Gerth, S. Leue, & M. Massink (Eds.), Theoretical and Practical Aspects of SPIN Model Checking, Proceedings of 5th and 6th International SPIN Workshops, Trento/Toulouse (Vol. 1680, pp. 57–76 (20 pages). Springer Verlag. https://doi.org/10.1007/3-540-48234-2_5
  • Nestmann, U., & Steffen, M. (1997). Typing Confluence. Second International ERCIM Workshop on Formal Methods In Industrial Critical Systems, 77–101.
  • Steffen, M. (1997). Polarized Higher-Order Subtyping (Extended Abstract). In Z. Luo & S. Soloviev (Eds.), Electronic Proceedings of the Types working group Workshop on Subtyping, inheritance and modular development of proofs.
  • Hofmann, M., Naraschewski, W., Steffen, M., & Stroup, T. (1996, July). Inheritance of Proofs. Electronic Proceedings of the Third Workshop On Foundations of Object-Oriented Languages (FOOL 3).
  • Nestmann, U., & Steffen, M. (1996). Correct Transformational Design of Concurrent Search Structures. In B. Freitag, C. Jones, C. Lengauer, & H.-J. Schek (Eds.), Object-Orientation with Parallelism and Persistence. Contributions from the Dagstuhl-Seminar 9514, April ’95 (pp. 23–42). Kluwer Academic Publishers.
  • Nestmann, U., Steffen, M., & Stroup, T. (1995). Formale Semantik für asynchronen Methodenaufruf. In R. Gotzhein & J. Bredereke (Eds.), Formale Beschreibungstechniken für verteilte Systeme (pp. 169–178 (10 pages). Universität Kaiserslautern, Fachbereich Informatik.
  • Steffen, M., & Pierce, B. C. (1994). Higher-Order Subtyping. In E.-R. Olderog (Ed.), Proceedings of PROCOMET ’94 (pp. 511–530 (20 pages). North-Holland.
  • Steffen, M., & Siegel, M. (1992). Validity in the Propositional μ-Calculus. In U. Goltz & W. Reisig (Eds.), Workshop: Logics for Distributed Systems, GMD-Studien Nr. 214. GMD, Gesellschaft für Mathematik und Datenverarbeitung.

Other papers (workshop contributions …)

  • Fava, D., & Steffen, M. (2019, November). Ready, set, Go! Data race detection and the Go language. Informal Proceedings of NWPT’19.
  • Fava, D., Steffen, M., & Stolz, V. (2018). Anything Goes Unless Forbidden. Notes on synchronization and the operational semantics of a relaxed memory model. 35th Annual Meeting of the GI Working Group “Programming Languages and Computing Concepts, 96–110.
  • Fava, D., Steffen, M., Stolz, V., & Valle, S. (2017). An Operational Semantics for a Weak Memory Model with Buffered Writes, Message Passing, and Goroutines. Informal Proceedings of the PhD Symposium at IFM’17 (Integrated Formal Methods). https://martinsteffen.github.io/download/17/oswmmwb-abstract-ifm.pdf
  • Fava, D., Steffen, M., Stolz, V., & Valle, S. (2017). An Operational Semantics for a Weak Memory Model with Buffered Writes, Message Passing, and Goroutines. Informal Proceedings of NPWT’17 (Nordic Workshop On Programming Theory).
  • Stumpf, J. B., Johnsen, E. B., & Steffen, M. (2017, June). Virtually Timed Ambients: Formalization and Analysis (extended abstract). Informal Proceedings of the PhD Symposium at IFM’17 (Integrated Formal Methods). https://martinsteffen.github.io/download/17/vta-abstract-ifmds.pdf
  • Johnsen, E. B., Steffen, M., & Stumpf, J. B. (2016, October). A Calculus of Virtually Timed Ambients (extended abstract). Proceedings of the 24nd Nordic Workshop on Programming Theory (NWPT’16). "steffenwwwc" # "16/calculusvta-abstract-nwpt.pdf"
  • Johnsen, E. B., Steffen, M., & Stumpf, J. B. (2016, September). A Calculus of Virtually Timed Ambients (extended abstract). Informal Proceedings of the 23rd International Workshop On Algebraic Development Techniques (WADT 2016).
  • Pun, K. I., Steffen, M., Stolz, V., Wickert, A.-K., Bodden, E., & Eichberg, M. (2016). Don’t let data Go astray: A Context-Sensitive Taint Analysis for Concurrent Programs in Go (extended abstract). Proceedings of the 24nd Nordic Workshop on Programming Theory (NWPT’16).
  • Pun, K. I., Steffen, M., & Stolz, V. (2013, November). Lock-Polymorphic Behaviour Inference for Deadlock Checking (extended abstract). Proceedings of NWPT’13. https://martinsteffen.github.io/download/13/lockpolymorphic-nwpt.pdf
  • Pun, K. I., Steffen, M., & Stolz, V. (2012, October). Deadlock Checking by Data Race Detection. Proceedings of the 24nd Nordic Workshop on Programming Theory (NWPT’12). https://martinsteffen.github.io/download/12/deadlockchecking-nwpt.pdf
  • Mai Thuong Tran, T., Steffen, M., & Truong, H. (2012, October). Compositional Analysis of Resource Bounds for Software Transactions. Proceedings of the 24nd Nordic Workshop on Programming Theory (NWPT’12). https://martinsteffen.github.io/download/12/compositional-nwpt.pdf
  • Ábrahám, E., Mai Thuong Tran, T., & Steffen, M. (2011). Inheritance and Observability (extended abstract) [Technical report]. Proceedings of the 23nd Nordic Workshop on Programming Theory (NWPT’11), 254/2011. https://martinsteffen.github.io/download/11/inheritance-nwpt.pdf
  • Mai Thuong Tran, T., & Steffen, M. (2011, January). Specification and Verification. Eternal Task Force 2: Time Awareness and Management. State-of-the-Art Report.
  • Pun, K. I., Steffen, M., & Stolz, V. (2011). Polymorphic behavioural lock effects for deadlock checking (extended abstract) [Technical report]. Proceedings of the 23nd Nordic Workshop on Programming Theory (NWPT’11), 254/2011, 48–50. https://martinsteffen.github.io/download/11/dlpoly-nwpt.pdf
  • Mai Thuong Tran, T., Steffen, M., & Truong, H. (2011). Estimating Resource Bounds for Software Transactions (extended abstract) [Technical report]. Proceedings of the 23nd Nordic Workshop on Programming Theory (NWPT’11), 254/2011, 77–79. https://martinsteffen.github.io/download/11/resources-nwpt.pdf
  • Pun, K. I., & Steffen, M. (2010). Deadlock checking by behavior inference for lock handling (extended abstract). Proceedings of the 22nd Nordic Workshop on Programming Theory (NWPT’10), 57, 8–9.
  • Johnsen, E. B., Mai Thuong Tran, T., Owe, O., & Steffen, M. (2010). Safe Locking for Multi-Threaded Java (extended abstract). Proceedings of the 22nd Nordic Workshop on Programming Theory (NWPT’10), 57, 5–7.
  • de Boer, F. S., Grabe, I., & Steffen, M. (2009, September). Static Deadlock Detection for Active Objects (Extended Abstract). ENTCS Proceedings of NWPT’09. 09/static-nwpt.pdf
  • Owe, O., Steffen, M., & Torjusen, A. (2009, September). Model Testing Asynchronously Communicating Objects using Modulo AC Rewriting (Extended Abstract). Proceedings of NWPT’09.
  • Steffen, M., & Tran, T. M. T. (2009, October). Safe Commits for Transactional Featherweight Java (extended abstract). Proceedings of the Nordic Workshop on Programming Theory, NWPT’09. 09/safecommits-nwpt09.pdf
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2008). Lazy Behavioral Subtyping (Extended Abstract). In T. Uustalu, J. Vain, & J. Ernits (Eds.), Proceedings of the Nordic Workshop of Programming Theory ’08 (Abstracts), Tallinn. https://martinsteffen.github.io/download/08/lazy-nwpt.pdf
  • Kyas, M., Stam, A., Steffen, M., & Torjusen, A. B. (2008). A Specification-Driven Interpreter for Testing Asynchronous Creol Components (extended abstract). In T. Uustalu, J. Vain, & J. Ernits (Eds.), Proceedings of the Nordic Workshop of Programming Theory ’08 (Abstracts), Tallinn. https://martinsteffen.github.io/download//08/specificationdriven-nwpt.pdf
  • Ábrahám, E., Grabe, I., Grüner, A., & Steffen, M. (2007). Abstract Interface Behavior of an Object-Oriented Language with Futures and Promises (extended abstract). In E. B. Johnsen, O. Owe, & G. Schneider (Eds.), Proceedings of the 19th Nordic Workshop on Programming Theory (NWPT’07). Extended Abstracts. University of Oslo, Dept. of Computer Science, Technical Report 366.
  • de Boer, F. S., Bonsangue, M. M., Grüner, A., & Steffen, M. (2007). Test Driver Generation from Object-Oriented Interaction Traces (extended abstract). In E. B. Johnsen, O. Owe, & G. Schneider (Eds.), Proceedings of the 19th Nordic Workshop on Programming Theory (NWPT’07). Extended Abstracts. University of Oslo, Dept. of Computer Science, Technical Report 366 (pp. 52–54). https://martinsteffen.github.io/download/07/testing-short.pdf
  • Ábrahám, E., Grüner, A., & Steffen, M. (2005). Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes. In R. Iosif & D. Distefano (Eds.), Proceedings of the First International Workshop on the Verification of COncurrent Systems with dynaMIC Allocated Heaps, Cosmicah’05, Queen Mary Technical Report RR-05-04 (pp. 47–61 (14 pages).
  • Traulsen, C., & Steffen, M. (2005, September). Using Constraints for Model Checking Buffered Systems (Extended Abstract). Informal Proceedings of the 17th Nordic Workshop On Programming Theory.
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2004, April). Inductive Proof Outlines for Multithreaded Java with Exceptions (Extended abstract). Electronic Proceedings of the “12. Kolloquium Programmiersprachen Und Grundlagen Der Programmierung.” http://nakalele.informatik.uni-freiburg.de/cgi/KPS2004.cgi
  • Ábrahám, E., Bonsangue, M. M., de Boer, F. S., & Steffen, M. (2004, April). Classes, Object Connectivity, and Observability (Extended abstract). Informal Electronic Proceedings of the “12. Kolloquium Programmiersprachen Und Grundlagen Der Programmierung.”
  • Ábrahám-Mumm, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2001). Deductive Verification for Multithreaded Java (Extended abstract). Proceedings of the “11. Kolloquium Programmiersprachen Und Grundlagen Der Programmierung”, 2001, Rurberg, 121–126.
  • Dams, D., Lakhnech, Y., & Steffen, M. (1999, April). Iterating Transducers. Informal Electronic Proceedings of the “Kolloquium Programmiersprachen Und Grundlagen Der Programmierung”, Heinsberg.
  • Mikk, E., & Steffen, M. (1999). Programming Environment for Statecharts. Included in the proceedings of the “7. Deutschen Anwenderforum für Statemate MAGNUM, 26.–27. April, 1999.

Technical reports

  • Fava, D., Steffen, M., & Stolz, V. (2018). Operational Semantics of a Weak Memory Model with Channel Synchronization: Proof of Sequential Consistency for Race-Free Programs (No.477; Number 477). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Gkolfi, A., Din, C. C., Einar Broch Johnsen, M. S., Lars Michael Kristensen, & Yu, I. C. (2018). Translating Active Objects into Colored Petri Nets for Communication Analysis (No.479; Number 479). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Fava, D., Steffen, M., Stolz, V., & Valle, S. (2017). An Operational Semantics for a Weak Memory Model with Buffered Writes, Message Passing, and Goroutines (No.466; Number 466). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Luteberget, B., Johansen, C., & Steffen, M. (2016). Rule-based Consistency Checking of Railway Infrastructure Designs (Technical Report No.450; Number 450). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Pun, K. I., Steffen, M., & Stolz, V. (2013). Lock-Polymorphic Behaviour Inference for Deadlock Checking (Technical Report No.436; Number 436). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics. http://www.ifi.uio.no/ msteffen/download/13/lockpolymorphic-rep.pdf
  • Mai Thuong Tran, T., Steffen, M., & Truong, H. (2013). Estimating Resource Bounds for Software Transactions (Revised version) (Technical Report No.414; Number 414). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Pun, K. I., Steffen, M., & Stolz, V. (2012). Behaviour Inference for Deadlock Checking (Technical Report No.416; Number 416). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Pun, K. I., Steffen, M., & Stolz, V. (2012). Deadlock Checking by Data Race Detection (Technical Report No.421; Number 421). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Ábrahám, E., Mai Thuong Tran, T., & Steffen, M. (2011). Observable interface behavior and inheritance (Technical Report No.409; Number 409, pp. 43 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Hansen, H. A., Schneider, G., & Steffen, M. (2011). Reachability Analysis of Complex Planar Autonomous Systems (Technical Report No.412; Number 412, pp. 44 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Johnsen, E. B., Mai Thuong Tran, T., Owe, O., & Steffen, M. (2011). Safe Locking for Multi-Threaded Java (Technical Report (Revised Version) No.402; Number 402, pp. 32 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Pun, K. I., Steffen, M., & Stolz, V. (2011). Deadlock Checking by a Behavioral Effect System for Lock Handling (Technical Report No.404; Number 404). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2009). Lazy Behavioral Subtyping: Single Inheritance and Interfaces (Research Report No.384; Number 384, pp. 38 pages). Department of Informatics.
  • Steffen, M., & Tran, T. M. T. (2009). The Stock Quoter Case Study. Internal Document.
  • Steffen, M., & Tran, T. M. T. (2009). Safe Commits for Transactional Featherweight Java (Technical Report No.392; Number 392, pp. 23 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2008). Lazy Behavioral Subtyping (revised version) (Technical Report No.368; Number 368, pp. 21 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Dovland, J., Johnsen, E. B., Owe, O., & Steffen, M. (2008). Incremental Reasoning for Multiple Inheritance (Research Report No.373; Number 373, pp. 21 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Grabe, I., Steffen, M., & Torjusen, A. B. (2008). Executable Interface Specifications for Testing Asynchronous Creol Components (Technical Report No.375; Number 375, pp. 26 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Ábrahám, E., Grabe, I., Grüner, A., & Steffen, M. (2007). Behavioral Interface Description of an Object-Oriented Language with Futures and Promises (Technical Report No.364; Number 364, pp. 38 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Owe, O., Schneider, G., & Steffen, M. (2007). Components, Objects, and Contracts (Research Report No.363; Number 363, pp. 18 pages). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Ábrahám, E., Grüner, A., & Steffen, M. (2006). Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes (Technical Report No.0601; Number 0601, pp. 40 pages). Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám, E., Grüner, A., & Steffen, M. (2005). An Open Structural Operational Semantics for an Object-Oriented calculus with Thread Classes (Technical Report No.0505; Number 0505). Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám, E., Becker, B., Klaedke, F., & Steffen, M. (2004). Optimizing Bounded Model Checking for Linear Hybrid Systems. Further experimental results (Technical Report No.TR214; Number TR214). Albert-Ludwigs-Universität Freiburg, Fakultät für Angewandte Wissenschaften, Institut für Informatik.
  • Ábrahám, E., Bonsangue, M. M., de Boer, F. S., & Steffen, M. (2004). Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes [Preliminary Technical Report and Project report]. Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel. http://www-omega.imag.fr/doc/d1000313_1/WP11-D115-313-V1-fa.pdf
  • Ábrahám, E., Bonsangue, M. M., de Boer, F. S., & Steffen, M. (2003). A Structural Operational Semantics for a Concurrent Class Calculus (Technical Report No.0307; Number 0307). Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2003). Inductive Proof Outlines for Multithreaded Java with Exceptions (Technical Report No.0313; Number 0313, pp. 105 pages). Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2003). A Hoare Logic for Monitors in Java (Techical Report TR-ST-03-1; Number TR-ST-03-1, pp. 80 pages). Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám-Mumm, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2002). A Compositional Operational Semantics for Java_MT (Technical Report TR-ST-02-2; Number TR-ST-02-2, pp. 15 pages). Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám-Mumm, E., de Boer, F. S., de Roever, W.-P., & Steffen, M. (2002). Verification for Java’s Reentrant Multithreading Concept: Soundness and Completeness (Technical Report TR-ST-02-1; Number TR-ST-02-1, pp. 95 pages). Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Ábrahám-Mumm, E., Hannemann, U., & Steffen, M. (2001). Verification of Hybrid Systems: Formalization and Proof Rules in PVS (TR-ST-01-1; Number TR-ST-01-1). Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Dams, D., Lakhnech, Y., & Steffen, M. (2000). Iterating Transducers for Safety of data-abstractions (Internal Report TR-ST-00-2; Number TR-ST-00-2, pp. 33 pages). Christian-Albrechts-Universität, Lehrstuhl Softwaretechnologie.
  • Sidorova, N., & Steffen, M. (2000). Verification of a Wireless ATM Medium-Access Protocol (Technical Report TR-ST-00-3; Number TR-ST-00-3, pp. 22 pages). Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel.
  • Sidorova, N., & Steffen, M. (2000). Verifying Mascara Control (Technical Report TR-ST-00-1; Number TR-ST-00-1, pp. 51 pages). Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel. Change that one http://www.informatik.uni-kiel.de/inf/deRoever/techreports/00/tr-st-00-1.ps.gz
  • Hofmann, M., Naraschewski, W., Steffen, M., & Stroup, T. (1996). Inheritance of Proofs (Interner Bericht 5/96; Number 5/96). Universität Erlangen-Nürnberg, Informatik, IMMDVII.
  • Egner, M., Nestmann, U., & Steffen, M. (1995). Confluent Processes for Transformation Correctness (preliminary version) (Interner Bericht IMMD7-1/95; Number IMMD7-1/95). Informatik VII, Universität Erlangen-Nürnberg.
  • Nestmann, U., Steffen, M., & Stroup, T. (1995). Formale Semantik für asynchronen Methodenaufruf (Interner Bericht TR-I7-95-11; Number TR-I7-95-11, pp. 11 pages). Universität Erlangen–Nürnberg, IMMD VII.
  • Steffen, M., & Nestmann, U. (1995). Typing Confluence (Interner Bericht IMMD7-xx/95; Number IMMD7-xx/95). Informatik VII, Universität Erlangen-Nürnberg.
  • Nestmann, U., & Steffen, M. (1994). Kalkübasierte OO-Sprachen (Technical Report IMMD7-02/94; Number IMMD7-02/94, pp. 9 pages). Universität Erlangen-Nürnberg, Informatik, IMMDVII.
  • Steffen, M., & Pierce, B. C. (1994). Higher-Order Subtyping (Interner Bericht IMMD7-01/94; Number IMMD7-01/94). Informatik VII, Universität Erlangen-Nürnberg.

Edited books and proceedings

  • Fava, D., Johnsen, E. B., Owe, O., & Steffen, M. (Eds.). (2019). Journal of Logic and Algebraic Methods in Programming: Special issue with selected publications of the “Nordic Workshop of Programming Theory”, NWPT ’18. In preparation. Elsevier.
  • Software Engineering and Formal Methods. SEFM 2019 Collocated Workshops: CoSim-CPS, ASYDE, CIFMA, and FOCLASA, Oslo, Norway, September 16–20, 2019, Revised Selected Papers. (2020). In J. Camara & M. Steffen (Eds.), Software Engineering and Formal Methods. SEFM 2019 Collocated Workshops: CoSim-CPS, ASYDE, CIFMA, and FOCLASA, Oslo, Norway, September 16–20, 2019, Revised Selected Papers. https://doi.org/10.1007/978-3-030-57506-9
  • Knoop, J., Steffen, M., & y Widemann, B. T. (Eds.). (2019). Tagungsband des 36ten Jahrestreffens der GI-Fachgruppe “Programmiersprachen und Rechenkonzepte” (Number 488). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Knoop, J., Steffen, M., & y Widemann, B. T. (Eds.). (2018). Tagungsband des 35ten Jahrestreffens der GI-Fachgruppe “Programmiersprachen und Rechenkonzepte” (Number 482). University of Oslo, Faculty of Mathematics and Natural Sciences, Dept. of Informatics.
  • Owe, O., Steffen, M., & Telle, J. A. (Eds.). (2013). Information and Computation: Special issue with selected publications of “Fundamentals of Computation Theory”, FCT ’11 (Vol. 231). Elsevier.
  • Proceedings of FCT ’11: Fundamentals of Computation Theory, 18th International Symposium (Oslo, Norway, August 25 – 28, 2011). (2011). In O. Owe, M. Steffen, & J. A. Telle (Eds.), Proceedings of FCT ’11: Fundamentals of Computation Theory, 18th International Symposium (Oslo, Norway, August 25 – 28, 2011) (Vol. 6914). Springer Verlag. https://doi.org/10.1007/978-3-642-22953-4
  • Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever. (2010). In D. Dams, U. Hannemann, & M. Steffen (Eds.), Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever (Number 5930). Springer Verlag. https://doi.org/10.1007/978-3-642-11512-7
  • Proceedings of the 7th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS ’05), Athens, Greece. (2005). In M. Steffen & G. Zavattaro (Eds.), FMOODS ’05 (Vol. 3535). Springer Verlag.

Slides of further presentations

  • Steffen, M. (2021). Presentation at the defense of Francisco Ramón (Kiko) Fernández Reyes (Abstractions to control the future).
  • Steffen, M. (2018). Operational Semantics of a Weak Memory Model with Channel Communication. Presentation at D-CON 18, Darmstadt.
  • Steffen, M. (2017). Weak Memory Models. Guest lecture, University College Bergen.
  • Steffen, M. (2017). Highlights of the Go Language. Guest lecture, University Oslo.
  • Steffen, M. (2017). Correctness, Concurrency, & Compositionality. Facets of Program Analysis. Sonderkolloquium Kassel.
  • Steffen, M. (2017). Einführung in die Rekursion. Sonderkolloquium Kassel.
  • Steffen, M. (2016). Highlights of the Go Language. Guest lecture, University Oslo.
  • Steffen, M. (2016). Highlights of the Go Language. Guest lecture, University College, Bergen.
  • Steffen, M. (2016). Model checking. Presentation at the logic seminar.
  • Steffen, M. (2015). Highlights of the Go Language. Guest lecture, University Oslo.
  • Steffen, M. (2014). A Proof System for Service Response Times. Presented at the Envisage WP2.2 meeting, Rome.
  • Steffen, M. (2014). Effect-Polymorphic Behaviour Inference for Deadlock Checking. Presented at SEFM’14, Grenoble.
  • Steffen, M. (2014). Deadlock Checking by Data Race Detection with OTT. Presented at the 31. Workshop of the GI-Fachgruppe, Programmiersprachen und Rechenkonzepte.
  • Steffen, M. (2014). PMA Group Presentation. Presented at the Conserns Meeting 2014, Geilo.
  • Steffen, M. (2013). Compositional Static Analysis for Implicit Join Synchronization in a Transactional Setting. Presented at the International Conference on Software Engineering and Formal Methods (SEFM’13).
  • Steffen, M. (2013). Compositional Static Analysis for Implicit Join Synchronization in a Transactional Setting. Presented at Second International Workshop on Behavioural Types (BEAT II) 2013.
  • Steffen, M. (2013). Curry-Howard Isomorphism. Presented at the Formal Methods Seminar.
  • Steffen, M. (2013). Deadlock Checking by Data Race Detection. Presented in 30. Workshop of the GI-Fachgruppe, Programmiersprachen und Rechenkonzepte.
  • Steffen, M. (2012). Compositional Analysis of Resource Bounds for Software Transactions. Presented at NWPT’12, Bergen.
  • Steffen, M. (2012). Estimating Resource Bounds for Nested Transactions with Join Synchronization. Presented in 29. Workshop of the GI-Fachgruppe, Programmiersprachen und Rechenkonzepte.
  • Steffen, M. (2012). What’s new about deadlocks. Presented at the Formal Methods seminar.
  • Steffen, M. (2011). PMA group: Master theses. Presentation for master students.
  • Steffen, M. (2011). Estimating Resource Bounds for Software Transactions. Presented at the Formal Methods seminar.
  • Steffen, M. (2010). PMA group: Master theses. Presentation for master students.
  • Steffen, M. (2010). The Abstract Behavioral Specification Language (ABS) and the HATS Tool Chain. Presentation at FCMO 2010.
  • Steffen, M. (2010). Observability and Full-Abstraction for Object-Oriented Languages. Presentation at the College of Technology, Vietnam National University, Hanoi.
  • Steffen, M. (2010). PMA group: Master theses. Presentation for master students.
  • Steffen, M. (2010). The Core ABS Language. Presentation at the HATS meeting, Amsterdam.
  • Steffen, M. (2010). Inheritance and Observability. Presentation at the Formal Methods seminar, Oslo.
  • Steffen, M. (2010). Model Testing Asynchronously Communicating Objects using Rewriting Modulo AC? Presented at the University Graz.
  • Steffen, M. (2010). Model Testing Asynchronously Communicating Objects using Rewriting Modulo AC. Presented at MBT’10 (Model Based Testing), ETAPS Satellite.
  • Steffen, M. (2010). PMA group: Research & Topics. Presentation for master students.
  • Steffen, M. (2009). Design of an Abstract Behavioral Specification Language. Presentation at FCMO’09, Eindhoven. 4.11.2009.
  • Steffen, M. (2009). Core ABS language. Presentation at the HATS meeting.
  • Steffen, M. (2009). Executable interface specifications for testing asynchronous Creol components. Talk at the 3rd International Conference on Fundamentals of Software Engineering, FSEN 2009.
  • Steffen, M. (2009). Incremental Reasoning for Multiple Inheritance. Talk at iFM 2009.
  • Steffen, M. (2009). Software Transactional Memory and Automatic Mutual Exclusion (1). Talk at the Formal Methods Seminar.
  • Steffen, M. (2009). Software Transactional Memory and Automatic Mutual Exclusion (2). Talk at the Formal Methods Seminar.
  • Steffen, M. (2008). Creol as Formal Model for Distributed, Concurrent Systems. Talk at FLACOS’2008, Malta.
  • Steffen, M. (2008). (Multiple) Inheritance, Behavioral Subtyping and Separation Logic. Talk at the Advanced Seminar.
  • Steffen, M. (2008). Research Topics within the Credo, Hats, and Avabi projects. Short presentation for prospective Master’s students at the University of Oslo.
  • Steffen, M. (2008). Object-Oriented Components (Workpackage 2). Talk at the Credo progress review meeting.
  • Steffen, M. (2008). Workpackage 2 Progress and Developments. Talk at the Credo plenary meeting.
  • Steffen, M. (2007). Futures and Promises in Creol. Talk at the Sintef Research Company, Oslo.
  • Steffen, M. (2007). Futures and Promises in OO. Credo Review Meeting in Brussels.
  • Steffen, M. (2007). Behavioral interface description of an object-oriented language with futures and promises. Nordic Workshop on Programming Theory.
  • Steffen, M. (2007). Behavioral interface behavior for concurrent OO languages with futures and promises. Credo Project Meeting, Amsterdam.
  • Steffen, M. (2007). Components, Objects, and Contracts. Specification and Verification of Component-Based Systems (SAVCBS’07).
  • Steffen, M. (2007). Game semantics. Tuesday’s Lunch Club.
  • Steffen, M. (2007). Interface Automata. Tuesday’s Lunch Club.
  • Steffen, M. (2007). XML Query Languages. Public presentation for the habilitation defense (Habilitationsvortrag).
  • Steffen, M. (2006). Interfaces, Components, and Types. Talk at the Credo meeting in Prague.
  • Steffen, M. (2006). Abstract Interface Behavior of Object-Oriented Languages with Monitors. Talk at the Mobij/Credo meeting in Oslo.
  • Steffen, M. (2006). Observability and Classes: Bits and Pieces. Talk at the Mobij/Credo meeting in Oslo.
  • Steffen, M. (2005). Inductive Proof Outlines for Exceptions in Multithreaded Java. Talk at the IPM International Workshop on Foundations of Software Engineering: Theory and Practice (FSEN’05), Tehran.
  • Steffen, M. (2005). Determinism, Replay, and Observability in Class-Based OO Languages. Talk at the IFIP WG 2.2 meeting, Skagen.
  • Steffen, M. (2005). Switching, Swapping, and Replay. Issues for an open semantics for a Java-like calculus. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel”, 8. 6. 2005.
  • Steffen, M. (2005). Observability issues in class-based languages (Inheritance, concurreny, cloning, and all that). Gjesteforelesning (guest lecture) at the University of Olso.
  • Steffen, M. (2004). Observability, Classes, and Object Connectivity. Invited talk at the 3rd FMCO’03, Leiden, The Netherlands.
  • Steffen, M. (2004). Observability, Classes, and Object Connectivity. Talk at the IFIP WG 2.2 meeting, Bertonino.
  • Steffen, M. (2004). Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes. Talk at ICTAC’04, Guiyang, China.
  • Steffen, M. (2004). An assertional proof-system for multithreaded Java. Invited talk at the Summer Research Institute 2004, EPFL, Lausanne.
  • Steffen, M. (2004). Observability, Classes, and Object-Connectivity. Invited talk at the Summer Research Institute 2004, EPFL, Lausanne.
  • Steffen, M. (2004). Object connectivity for class-based, multithreaded OO. Invited talk at the University Bamberg, July 13, 2004.
  • Steffen, M. (2004). Object Connectivity. Talk at the “Kolloquium Programmiersprachen und Grundlagen der Programmierung”, 17.–19. March 2004, Freiburg-Munzingen.
  • Steffen, M. (2003). Inductive Proof Outlines for Monitors in Java. Talk at Fmoods’03, Paris, 21. November 2003.
  • Steffen, M. (2003). Object Connectivity and Full Abstraction for Class-Based OO. Talk at the MobiJ workshop, FMCO’03, Leiden, 3. November 2003.
  • Steffen, M. (2003). Towards Full Abstraction for Class-Based OO. Invited talk at the University of Kent, Canterbury.
  • Steffen, M. (2003). Towards Full Abstraction for Class-Based OO. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel”, 18. 6 2003.
  • Steffen, M. (2003). A Hoare logic for Monitors in Java. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel”, 12. 2. 2003.
  • Steffen, M. (2003). Towards Full Abstraction for Class-Based OO. Presented at the MobiJ-meeting Kiel, 9. 6 2003.
  • Steffen, M. (2003). Programmierung eingebetteter System mit Lego Mindstorms. Talk at the “Day of the open door” of the Technische Fakultät, University Kiel, May 17th.
  • Steffen, M. (2003). Towards Full Abstraction for Multithreaded, Class-Based OO. Presented at the MobiJ workshop, TU München, 6. February 2003.
  • Steffen, M. (2003). Programmierung eingebetteter System mit Lego Mindstorms. Presentation at the “Day of the open door” of the Christian-Albrechts Universität, 4th May 2003.
  • Steffen, M. (2002). Towards Full Abstraction for Multithreaded, Class-Based OO. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel”, 4. December 2002.
  • Steffen, M. (2002). A Proof System for Multithreaded Java. Talk at the Omega Meeting, University Oldenburg, 9. September 2002.
  • Steffen, M. (2001). Embedding Chaos. Presented at 8th International Static Analysis Symposium (SAS’01), Paris, 15th. July 2001.
  • Steffen, M. (2001). Embedding Chaos. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel.”
  • Steffen, M. (2001). Iterating Transducers. Presented at the 13th Conference on Computer Aided Verification CAV’01, Paris, July 2001.
  • Steffen, M. (2001). Assertion-Based Analysis of Hybrid Systems with PVS. Presented at the Eighth International Conference on Computer Aided Systems Theory, Formal Methods and Tools for Computer Science (Eurocast ’01), Las Palmas de Gran Canaria, February 2001.
  • Steffen, M. (2001). Accelerating Transducers. Presented at the University of Chicago, 30. March 2001.
  • Steffen, M. (2000). Accelerating Transducers. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel”, January 2000.
  • Steffen, M. (2000). On the Verification of Mascara. Talk at the Vires-meeting.
  • Steffen, M. (2000). Accelerating Transducers. Talk at the Vires-meeting.
  • Steffen, M. (2000). Verification of Mascara Control. Talk at the Vires-review, 16. June 2000.
  • Steffen, M. (2000). Accelerating Transducers. Talk at the Vires-review, 16. June 2000.
  • Steffen, M. (2000). Fehlerfreie Software? Vortrag zum Tag der offenen Tür der Christian-Albrechts-Universtiät, 7th May, 2000.
  • Steffen, M. (1999). Accelerating Transducers. Talk at the Kolloquium “Programmiersprachen und Grundlagen der Programmierung”, Kirchhunden–Heinsberg.
  • Steffen, M. (1999). Polarized Higher-Order Subtyping. Invited talk presented at BRICS, Aalborg. April 1999.
  • Steffen, M. (1999). OO: Ein Streifzug. Presented at a local seminar, University Kiel.
  • Steffen, M. (1998). Dynamic Control. Vires-project talk about parts of the Mascara protocol, November 1998, Plasmolen.
  • Steffen, M. (1998). Polarized Higher-Order Subtyping. Vortrag an der TU Eindhoven.
  • Steffen, M. (1998). Verifikation objektorientierter Programme. Presented at the “AG”, the working-group “Computer Science, Logics, and Mathematics, Kiel.”
  • Steffen, M. (1997). Polarized Higher-Order Subtyping. Vortrag im Types working group Workshop on Subtyping, inheritance and modular development of proofs, Durham.
  • Steffen, M. (1997). Polarized Higher-Order Subtyping. Talk at the “Kolloquium Programmiersprachen und Grundlagen der Programmierung, Fehmarn.
  • Steffen, M. (1997). Polarized Higher-Order Subtyping. Vortrag beim Doktoranden-Workshop an der Universität Passau.
  • Steffen, M. (1996). Objektorientierung und Typentheorie. Vortrag an der Universität Kiel.
  • Steffen, M. (1996). Polarisiertes F_≤^\,ω. Vortrag bei der Herbsttagung des SFB 182 in Pommersfelden, 24. – 25. Oktober 1996.
  • Steffen, M. (1996). Polarized F_≤^\,ω. Talk at the LFCS, Edinburgh.
  • Steffen, M. (1995). Confluent Processes for Transformation Correctness. Vortrag im Dagstuhl-Seminar Objekt-Orientierung mit Parallelität und Persistenz.
  • Steffen, M. (1995). Konfluente Prozesse. Vortrag beim Workshop ‘Formale Methoden in Parallelität und Objektorientierung’ an der Universität Passau.
  • Steffen, M. (1995). Konfluenz im \pi-Kalkül. Vortrag bei der Herbsttagung des SFB 182, Pommersfelden.
  • Steffen, M. (1995). Korrektheit paralleler Datenstrukturen durch Programmtransformation. Vortrag bei der Herbsttagung des SFB 182, Pommersfelden, 12. – 13. Oktober 1995.
  • Steffen, M. (1994). Objektorientierte Verifikation. Vortrag auf der IMMD7-Jahresbesprechung.
  • Steffen, M. (1994). Semantik und Verifikation von Objekten. Vortrag auf der Frühjahrstagung des SFB 182, Pommersfelden.
  • Steffen, M. (1994). Higher Order Subtyping. Talk at the Working Conference on Programming Concepts, Methods and Calculi (Procomet), San Miniato, Italy.
  • Steffen, M. (1993). Higher Order Subtyping. Talk at the Universität Erlangen-Nürnberg/Universität Passau workshop, Erlangen.
  • Steffen, M. (1993). Higher Order Subtyping. Vortrag am LFCS, Edinburgh.
  • Steffen, M. (1993). Higher Order Subtyping. Vortrag an der Universität of Sussex, Brighton.
  • Steffen, M. (1992). A Proof System for Hennessy-Milner Logic with Recursion. Talk at the LFCS, Edinburgh.
  • Steffen, M. (1992). A Proof System for Hennessy-Milner Logic with Recursion. Vortrag beim Workshop “Logics for Distributed Systems”, GMD, Bonn.
  • Steffen, M. (1990). Nebenläufige Basisalgorithmen. Talk at the Diplomseminar, Sarntal.