[theses] [journal articles] [papers] [ongoing] [tech reports] [editor] [other] [software] [presentations] [BibTeX]

The page contains links to my publications, some presentations, etc., the corresponding bibliographic references can be found as BibTeX entries here. An HTML-translation of the bibfile can be found here.
Commercial use of the documents is illegitimate, especially if the copyright has been transferred elsewhere (but if you should manage to make money out of it, let me know the trick anyway...)

Theses

Object-Connectivity and Observability for Class-Based, Object-Oriented Languages
Habilitation thesis. My thesis can be found here (also containing some Readme and some technical slides plus the slides of the public presentation about XML)
thesis document: pdf (submitted 4.7.2006, defended 7.2.2007)

Polarized Higher-Order Subtyping
PhD thesis (``Dissertation zur Erlangung des Grades Doktor-Ingenieur'')
Technische Fakultät, Friedrich-Alexander-Universität Erlangen-Nürnberg
thesis document: dvi, ps, pdf (final version)
slides of my defense (in German): ps (12.11.1998)

Vollständigkeit eines Beweissystems für Hennessy-Milner Logik mit Rekursion
diploma thesis (``Diplomarbeit'', ``Completeness of a proof system for Hennessy-Milner logic with recursion'')
joint work with Michael Siegel, in German
Friedrich-Alexander-Universität Erlangen, IMMD VII
thesis document: ps (March 1992)

Ein Beweissystem für Hennessy-Milner Logik mit Rekursion
Studienarbeit, joint work with Michael Siegel, in German
Friedrich-Alexander-Universtät Erlangen, IMMD VII
document: ps (July 1991)

Journal articles

Observable interface behavior and inheritance
Erika Ábrahám, Thi Mai Thuong Tran, and Martin Steffen,
Special issue on Behavioral Types of the Journal for Mathematical Structures in Computer Science (MSCS)
Accepted for publication, to appear 2014.
© Cambridge University Press
The paper is a revised version of the earlier UiO-IFI technical report
paper pdf (final revision: 29. December 2013)

Reachability Analysis of Complex Planar Autonomous Systems
Hallstein A. Hansen, Gerardo Schneider, and Martin Steffen,
Science of Computer Programming. Volume 78, Issue 12, pages 2511-2536
paper: doi/pdf (1.12.2013)

Deadlock Checking by a Behavioral Effect System for Lock Handling
Ka I Pun, Martin Steffen, Volker Stolz
In a special issue of the Journal of Logic and Algebraic Programming with selected articles from NWPT'10. The paper is a revised version of the earlier technical report.
paper: doi perma link (6. March 2012)

Safe locking for Multi-Threaded Java with Exceptions
Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen.
In a special issue of the Journal of Logic and Algebraic Programming with selected articles from NWPT'10. The paper is an extended version of the FSEN'11 conference contribution and of the technical report.
paper: doi perma link (6. March 2012)

Incremental Reasoning with Lazy Behavioral Subtyping for Multiple Inheritance
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
Science of Computer Programming, Volume 76, pages 915-941
paper: doi perma link, (October 2010, paper version October 2011)

Behavioral interface description of an object-oriented language with futures and promises
Erika Ábrahám, Immo Grabe, Andreas Grüner, Martin Steffen.
In a special issue of the Journal of Logic and Algebraic Programming with selected articles from NWPT'07.
An earlier (and superseded) version is available as technical report
paper: pdf (24.02.2009)

Abstract Interface Behavior of Object-Oriented Languages with Monitors
Erika Ábrahám, Andreas Grüner, and Martin Steffen
Journal contribution to the ToCS special issue containing the post-proceedings of CiE'06 (Computability in Europe 2006). The article is an extended version of the Fmoods'06 contribution
paper: pdf (24.05.2007)

Dynamic Heap-Abstraction for Open Object-Oriented Systems with Thread Classes
Erika Ábrahám, Andreas Grüner, Martin Steffen
Journal of Software and System Modeling (SoSym). The article is an reworked version of the University Kiel technical report 0601 and a longer version of the CiE'06 proceedings version, both under the same title
paper: pdf (11.07.2007)
doi perma-link at springer link

Inductive Proof Outlines for Exceptions in Multithreaded Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
Fundamenta Informaticae vol. 82, 2008, pages 1-73. The article is an extendevd version of the contribution to FSEN'05, and as a shortened and reworked version of the corresponding technical report.
paper: pdf (29.05.2007)

An Assertion-based Proof System for Multithreaded Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
Special issue of TCS, vol. 331, pages 251-290, © Elsevier
paper: pdf (March 2004)

Iterating Transducers
Dennis Dams, Yassine Lakhnech, and Martin Steffen.
Special issue of the Journal of Logic and Algebraic Programming on model checking. volume 52-53, July 2002, pages 109-127. A preliminary version appeared in the proceedings of CAV'01.
paper: gzipped ps, pdf

Higher Order Subtyping
Benjamin C. Pierce and Martin Steffen
Theoretical Computer Science, volume 172, number 1,2, pages 235-282, July 1997

ongoing work/unpublished/submitted/yet to be rejected ...



Lock-Polymorphic Behavior Inference for Deadlock Checking
Ka I Pun, Martin Steffen, and Volker Stolz
Submitted for conference.
paper: pdf (18. September 2013)
slides: pdf (23. September 2013, BEAT II workshop)

ABS: A Core Language For Abstract Behavioral Specification
Einar Broch Johnsen, Reiner Haehnle, Jan Schaefer, Rudi Schlatte, and Martin Steffen
Submitted for proceedings inclusion.
paper: pdf (27. March 2011)

Safe locking for Multi-Threaded Java
Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen.
Accepted for publication for the LNCS proceedings of FSEN'11. A shorter version has been presented as extended abstract at the NWPT'10, and a longer version has been published as Technical Report
paper: pdf (October 2010)

Termination Detection for Active Objects
Immo Grabe, Frank S. de Boer, and Martin Steffen,
Journal of Logic and Algebraic Programming, Elsevier
paper: pdf (Available online 16 March 2012)

Static Deadlock Detection for Active Objects (extended abstract)
Frank S. de Boer, Immo Grabe, Martin Steffen.
Submitted for workshop presentation
extended abstract: pdf (10.09.2009)

Encapsulating Lazy Behavioral Subtyping)
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
Submitted
paper: pdf (17.12.2008)

Automated Test Driver Generation for Java Components
Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen
To appear in the proceedings at the 14th Netherland's Testing Day ``TestDag'08'', Delft, November 2008

Lazy Behavioral Subtyping (extended abstract)
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
Submitted for workshop presentation
extended abstractr: pdf (03.10.2008)

Automated Test Driver Generation for Java Components (abstract)
Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, Martin Steffen.
Submitted for presentation
abstract: pdf (9.9.2008)

Executable interface specifications for testing asynchronous Creol components
Immo Grabe, Marcel Kyas, Arild Torjusen, Martin Steffen.
To appear in the LNCS post-proceedings of the 3rd International Conference on Fundamentals of Software Engineering (FSEN09). An extended version appears as technical report
paper: pdf (15.01.2009),
presentation: pdf (16.04.2009),

Refereed papers

Compositional Resource Bound Analysis for Nested Transactions with Join Synchronization
Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong
Accepted for publication in SEFM'13. See also the technical report 414 for an extended version including additional material (proofs)
paper: pdf (24 June 2013)
presentation: pdf (September 2013)

Deadlock Checking by Data Race Detection
Violet Ka I Pun, Martin Steffen, and Volker Stolz
FSEN 2013
paper: pdf, (28 Januar 2013)
presentation: pdf, (6. May 2013)

A Petri Net based Analysis of Deadlock for Active Objects and Futures
Frank S. de Boer, Mario Bravetti, Immo Grabe, Matias Lee, Martin Steffen, and Gianluigi Zavattaro
To appear at FACS'12.
paper: pdf (June 2012)

A Type System for Finding Upper Resource Bounds of Multi-Threaded Programs with Nested Transactions
Tung Vu Xuan, Hoang Truong Anh, Thi Mai Thuong Tran, and Martin Steffen,
Accepted for publication in the ACM proceedings of the 3rd International Symposium on Information and Communication Technology SoICT2012
submission: pdf (June 2012)

Design issues in concurrent object-oriented languages and observability
Thi Mai Thuong Tran, and Martin Steffen,
IEEE proceedings of KSE'11
submission: pdf (29. June 2011)

Reachability Analysis of Planar Autonomous Systems
Hallstein A. Hansen, Gerardo Schneider, and Martin Steffen,
Accepted for publication as in the LNCS proceedings of FSEN'11
paper: pdf (25.04.2010)

Credo Methodology (Extended Version)
Immo Grabe, Mohammad Mahdi Jaghoori, Bernhard Aichernig, Tobias Blechmann, Frank de Boer,
Andreas Griesmayer, Einar Broch Johnsen, Joachim Klein, Sascha Küppelholz, Marcel Kyas, Wolfgang Leister,
Rudolf Schlatte, Andries Stam, Martin Steffen, Simon Tschirner, Lian Xuedong, Wang Yi
Proceedings of the 8th International Symposium on Formal Methods for Components and Objects (FMCO 2009), Selected Papers, 2010
© Springer-Verlag
paper: pdf (2010)

Safe Typing for Transactional vs. Lock-Based Concurrency in Multi-Threaded Java
Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen.
Proceedings of the Second International Conference on Knowledge and Systems Engineering (KSE 2010), October 2010
© IEEE
paper: pdf (23.05.2010)

Safe Commits for Transactional Featherweight Java
Martin Steffen and Thi Mai Thuong Tran
Accepted for publication at the 8th International Conference on Integrated Formal Method (iFM10), pages 290-304 © Springer Verlag, 2010
paper: pdf (15.07.2010),

Model Testing Asynchronously Communicating Objects using Modulo AC Rewriting
Olaf Owe, Arild Torjusen, Martin Steffen.
Sixth Workshop on Model-Based Testing MBT'10, Paphos, Cyprus, March 2010
paper: pdf (15.02.2010)
slides: pdf (21.03.2010)

Credo Methodology. Modeling and Analyzing a Peer-to-Peer System in Credo
Immo Grabe, Mohammad Mahdi Jaghoori, Bernhard Aichernig, Tobias Blechmann, Frank de Boer, Andreas Griesmayer, Einar Broch Johnsen, Joachim Klein, and Sascha Küppelholz, Marcel Kyas, Wolfgang Leister, Rudolf Schlatte, Andries Stam, Martin Steffen, Simon Tschirner, Lian Xuedong, and Wang Yi
TTSS'09, Kuala Lumpur, Malaysia
paper: pdf (June 2009)

Incremental reasoning for multiple inheritance
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
7th International Conference on integrated Formal Methods, iFM'09, Düsseldorf, Germany
paper: pdf (22.09.2008)
slides: pdf (19.02.2009)

Java Test Driver Generation from Object-Oriented Interaction Traces
Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen
International Workshop on Harnessing Theories for Tool Support in Software TTSS'08, ICTAC 2008 satellite workshop, 30.-31. August. Istanbul, Turkey
paper: pdf locally or as doi perma link (28.7.2008)

Lazy Behavioral Subtyping
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
To appear in the LNCS Proceedings of 5th International Symposium on Formal Methods (FM 08), Turku, Finland
A longer version is available as technical report
paper: pdf (16.11.2007)

Components, Objects, and Contracts
Olaf Owe, Gerardo Schneider, and Martin Steffen
Workshop of Specification and Verification of Component-Based Systems (SAVCBS'07), pages 95-98 September 3-4, 2007
paper: pdf (23.07.2007)
slides: pdf (3.09.2007)

Dynamic Heap-Abstraction for Open Object-Oriented Systems with Thread Classes (Extended Abstract)
Erika Ábrahám, Andreas Grüner, and Martin Steffen
In the proceedings of CiE'06 (Computability in Europe 2006, Logical Approaches to Computational Barriers). pages 1-10, LNCS 3988, © Springer-Verlag
A longer version appeared under the same title as CAU technical report 0601, January 2006
(A preliminary version has been presented also at the ICALP satellite workshop Cosmicah'05)
paper: pdf (30.03.2006)
doi perma-link at springer link

Abstract Interface Behavior of Object-Oriented Languages with Monitors
Erika Ábrahám, Andreas Grüner, and Martin Steffen
Proceedings of the 7th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (Fmoods'06), LNCS 4036, pages 218-232, © IFIP/Springer-Verlag.
paper: pdf (1.4.2006) (an extended version (forthcoming report) can be found here)
slides: pdf (20.02.2006, Mobij meeting, Oslo)

Bounded Model Checking for Parametric Data Structures
Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen
Special issue for the Proceedings of the Fourth International Workhop on Bounded Model Checking (BMC'06), ENTC, vol 174, nr. 3. © Elsevier Science
paper: pdf (17. March 2006)
doi perma link

Inductive Proof Outlines for Exceptions in Multithreaded Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
ENTCS special issue with selected contributions to the IPM International Workshop in Foundations of Software Engineering (FSEN'05), Tehran, Iran. Oct. 1-3, 2005
A journal version, hich is a shortened version of the corresponding technical report, can be found here
paper: pdf (18.11.2005)
slides: pdf (02.10.2005)

Observability, Connectivity, and Replay in a Sequential Calculus of Classes
Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, Andreas Grüner, and Martin Steffen
Proceedings of the Third International Symposium on Formal Methods for Components and Objects (FMCO'04) Leiden, November 2004, pages 296--316, LNCS 3657, © Springer-Verlag
paper: pdf (1. July 2005).

A Fully Abstract Trace Semantics for UML Components
Frank S. de Boer, Marcello M. Bonsangue, Martin Steffen, and Erika Ábrahám,
Proceedings of FMCO'04, Leiden, November 2004, LNCS 3657, © Springer-Verlag
paper: pdf (July 2005).

Optimizing Bounded Model Checking for Linear Hybrid Systems
Erika Ábrahám, Felix Klaedke, Bernd Becker, and Martin Steffen
Proceedings of the 6th International Workshop on ``Verification, Model Checking, and Abstraction'' (VMCAI'05), January 17-19, 2005, Paris
pages 396-412, LNCS 3885, © Springer-Verlag
paper: pdf (November 04). some more experiments: ps., see also the technical report section

Synchronous Closing and Flow Analysis for Model Checking Timed Systems
Natalia Ioustinova, Natalia Sidorova, and Martin Steffen
Proceedings of FMCO'03, Leiden, November 2003, LNCS 3188, © Springer-Verlag
paper: pdf (15.03.2004)

Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes
Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen
Proceedings of the First International Colloquium on Theoretical Aspects of Computing ICTAC 2004 (handed in also as WP.1.1. D.1.1.5 Omega deliverable)
pages 38-52, LNCS 3704, © Springer-Verlag
paper: pdf (12.6.04). A longer version: pdf.

Characteristic mu-Calculus Formulas for Underspecified Transition Systems
Harald Fecher, Martin Steffen
In the Proceedings of the 11th International Workshop on Expressiveness in Concurrency (Express 04)
paper: pdf (revised version 2005)
also via Science direct, © Elsevier

A Compositional Operational Sematics for JavaMT
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
Proceedings of the International Symposium on Verification (Theory and Practice), Celebrating Zohar Manna's 64th Birthday, LNCS 2003, © Springer-Verlag
paper: gzipped ps, pdf (11.08.03)

Inductive Proof-Outlines for Montitors in Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
LNCS proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (Fmoods'03), LNCS, © Springer-Verlag. The technical report TR-ST-03-1 with the title ``A Hoare Logic for Monitors in Java'' contains a longer version.
paper: gzipped ps, pdf) (1. 9. 2003)
slides: slides (Paris, 20.11.03)

A Tool-supported Proof System for Multithreaded Java
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
Proceedings of FMCO'02, Leiden. LNCS, © Springer-Verlag
paper: gzipped ps, pdf, (23.07.03)
slides about the topic: Oldenburg, September 9, 2002: pdf, or a bit longer presented at FMCO'02 (Leiden) and the synchronous languages workshop: pdf/gzipped ps

Abstraction and Flow Analysis for Model Checking Open Asynchronous Systems
Natalia Ioustinova, Natalia Sidorova, and Martin Steffen
Proceedings of the 9th Asia-Pacific Software Engineering Conference (APSEC 2002), pages 227-235
paper: gzipped ps, pdf (1. 7. 2002)

Closing open SDL-systems for model checking with DTSpin
Natalia Ioustinova, Natalia Sidorova, and Martin Steffen
Proceedings of Formal Methods Europe FME'02, pages 531-548 LNCS, © Springer-Verlag
cf. also here
paper: gzipped ps, pdf (8. 5. 2002)

Synchronous Closing of Timed SDL Systems for Model Checking
Natalia Sidorova and Martin Steffen,
In the Proceedings of the Third International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI'02), pages 79-93 Venice
LNCS 2294, ©Springer-Verlag
paper: gzipped ps, pdf
slides: pdf

Verification for Java's Reentrant Multithreading Concept
Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
In the proceedings of FoSSACS 2002, LNCS 2303, © Springer-Verlag
paper: (gzipped ps, pdf)
For a longer version including the proofs, see the technical report TR-ST-02-1 below

Embedding Chaos
Natalia Sidorova and Martin Steffen
In the Proceedings of the 8th International Static Analysis Symposium (SAS'01), Paris, 2001, © Springer-Verlag
paper: gzipped ps pdf
slides: pdf

Verifying Large SDL-Specifications using Model Checking
Natalia Sidorova and Martin Steffen,
In the proceedings of the 10th SDL-Forum 2001, © Springer-Verlag
paper: pdf, gzipped ps

Verification of Hybrid Systems: Formalization and Proof Rules in PVS
Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen
In the proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2001), June 2001, © IEEE
A longer version appeared as technical report TR-ST-01-1
paper: pdf, gzipped ps

Iterating Transducers
Dennis Dams, Yassine Lakhnech, and Martin Steffen.
In the proceedings of 13th Conference on Computer Aided Verification CAV'01, © Springer-Verlag
paper: gzipped ps, pdf
slides: pdf

Assertion-Based Analysis of Hybrid Systems with PVS
Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen.
In the Proceedings of the Eighth International Conference on Computer Aided Systems Theory, Formal Methods and Tools for Computer Science (Eurocast '01), LNCS 2178, © Springer-Verlag
paper: gzipped ps, pdf, extended abstract: gzipped ps, pdf, slides: (19.02. 2001)

Verification of a Wireless ATM Medium-Access Protocol
Natalia Sidorova and Martin Steffen,
Proceedings of the 7th Asia-Pacific Software Engineering Conference (APSEC 2000),
p. 84-91. IEEE Computer Society
a preliminary and longer version appeared as technical report TR-ST-00-3

Divide, Abstract, and Model-Check
Karsten Stahl, Kai Baukus, Yassine Lakhnech, and Martin Steffen.
Combined Proceedings of the 5th and 6th International SPIN Workshop, Trento/Toulouse, 1999 LNCS-Series ,
paper: pdf, gzipped ps
code of the verification

Inheritance of proofs
Wolfgang Naraschewski and Martin Hofmann And Martin Steffen and Terry Stroup.
Theory and Practice of Object Systems (TAPOS), volume 4, number 1, 1998; Special Issue on the Third Workshop on Foundations of Object-Oriented Languages (FOOL 3), pp 51-69
paper: pdf, ps, dvi

Typing Confluence
Uwe Nestmann and Martin Steffen.
In the proceedings of FMICS'97, July 1997.
paper: pdf, ps (14.3.97)

Correct Transformational Design of Concurrent Search Structures
Uwe Nestmann and Martin Steffen.
In: B. Freitag, C. Jones, C. Lengauer, H.-J. Schek, editors, Object-Orientation with Parallelism and Persistence (contributions generated from Dagstuhl-Seminar 9514, April '95)
Copyright to Kluwer Academic Publishers

Edited books/proceedings

Proceedings of FCT'2011
Olaf Owe, Martin Steffen, and Jan Arne Telle (Eds.)
LNCS 6914, 2011, doi perma link,

Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever
Dennis Dams, Ulrich Hannemann, and Martin Steffen (Eds.)
LNCS 5930, 2010

Proceedings of the 7th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '05, co-located with DAIS'05),
15-17 June, 2005, Athens, Greece
Martin Steffen and Gianluigi Zavattaro (Eds.)
LNCS 3535

Technical reports
Most reports are preliminary and/or longer versions of the refereed/submitted/yet-to-be-rejected papers listed above, or also project contributions.

Lock-Polymorphic Behavior Inference for Deadlock Checking
Ka I Pun, Martin Steffen, and Volker Stolz
University of Oslo, Department of Informatics Research Report 436
paper: pdf (19. September 2013)

Deadlock Checking by Data Race Detection
Violet Ka I Pun, Martin Steffen, and Volker Stolz
University of Oslo, Department of Informatics Research Report 423
paper: pdf, (March 2011)

Behaviour Inference for Deadlock Checking
Ka I Pun, Martin Steffen, and Volker Stolz
University of Oslo, Department of Informatics Research Report 416
paper: pdf (9. July 2012)

Estimating Resource Bounds for Software Transactions
Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong
University of Oslo, Department of Informatics Research Report 414
paper: pdf or at the library (18 Feb 2013, revised version)

Reachability Analysis of Complex Planar Autonomous Systems
Hallstein A. Hansen, Gerardo Schneider, and Martin Steffen,
University of Oslo, Department of Informatics Research Report 412
report: pdf (14.11.2011)

Observable interface behavior and inheritance
Erika Ábrahám, Thi Mai Thuong Tran, and Martin Steffen,
University of Oslo, Department of Informatics Research Report 409
report: pdf (April 2011)

Deadlock Checking by a Behavioral Effect System for Lock Handling
Ka I Pun, Martin Steffen, Volker Stolz
University of Oslo, Department of Informatics Research Report 404
A shorter version has been presented as extended abstract at the NWPT'10
report: pdf (March 2011)

Safe locking for Multi-Threaded Java
Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen.
University of Oslo, Dept. of Informatics Research Report 402
A shorter version has been presented as extended abstract at the NWPT'10
report: pdf (Revised version January 2011)

Safe commits for Transactional Featherweight Java
Thi Mai Thuong Tran and Martin Steffen.
University of Oslo, Dept. of Informatics Research Report 392
A shorter version has been presented as extended abstract at the NWPT'09.
report: pdf (October 2009)

Lazy Behavioral Subtyping: Single Inheritance and Interfaces
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
University of Oslo, Dept. of Informatics Research Report 384
A shorter version has been submitted for conference proceedings.
report: pdf (May 2009)

Executable interface specifications for testing asynchronous Creol components
Immo Grabe, Arild Torjusen, Martin Steffen.
University of Oslo, Dept. of Informatics Research Report 375
A shorter version has been submitted for conference proceedings.
report: pdf (14.07.2008)

Incremental reasoning for multiple inheritance
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
University of Oslo, Dept. of Informatics Research Report 373
A shorter version has been submitted for conference proceedings.
paper: pdf (April 2008)

Lazy Behavioral Subtyping
Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen.
University of Oslo, Dept. of Informatics Research Report 368
The report is an extended version of conference version (FM'08) with the same title.
report: pdf (March 2008, revised version)


Behavioral interface description of an object-oriented language with futures and promises
Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen
University of Oslo, Dept. of Informatics Research Report 364.
The report is an extended version of the submitted conference version with the same title.
report: pdf (12. October 2007)

Components, Objects, and Contracts
Olaf Owe, Gerardo Schneider, and Martin Steffen
University of Oslo, Dept. of Informatics Research Report 363. A longer version of the contribution to SAVCBS'07
report: pdf (Aug 2007)

Abstract Interface Behavior of Object-Oriented Languages with Monitors
Erika Ábrahám, Andreas Grüner, and Martin Steffen
Institute of Computer Science and Applied Mathematics technical report TR-0612
paper: pdf (24.05.2007)

Dynamic Heap-Abstraction for Open Object-Oriented Systems with Thread Classes
Erika Ábrahám, Andreas Grüner, Martin Steffen
University Kiel, Institute of Computer Science and Applied Mathematics technical report TR-0601, February 1, 2006.
report: pdf (1.2.2006)

An Open Structural Operational Semantics for an Object-Oriented Calculus with Thread Classes
Erika Ábrahám, Andreas Grüner, Martin Steffen
University Kiel, Institute of Computer Science and Applied Mathematics technical report TR-0505,
report: pdf (13.05.2005)

Optimizing Bounded Model Checking for Linear Hybrid Systems: Theory and experimental results
Erika Ábrahám, Felix Klaedke, Bernd Becker, and Martin Steffen
Universtät Freiburg, Report Nr 214
report: pdf (November 2004)

A Deductive Proof System for Multithreaded Java with Exceptions
Erika Ábrahám, Andreas Grüner, Martin Steffen
University Kiel, Institute of Computer Science and Applied Mathematics technical report TR-0313
report: pdf (23.12.2003)

A Structural Operational Semantics for a Concurrent Class Calculus
Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen
University Kiel, Institute of Computer Science and Applied Mathematics technical report TR-0307
report: pdf (17.07.2003)

A Hoare Logic for Monitors in Java,
Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
University Kiel, Software Technology technical report TR-ST-03-1
report: pdf (15.08.2003)

Compositional operational semantics for JavaMT
Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
University Kiel, Software Technology technical report TR-ST-02-2
report: gzipped ps (15.05.2005)

Verification for Java's Reentrant Multithreading Concept: Soundness and Completeness
Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
University Kiel, Software Technology technical report TR-ST-02-1,
report: gzipped ps (March 2002)

Verification of Hybrid Systems: Formalization and Proof Rules in PVS
Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen
University Kiel, Software Technology technical report TR-ST-01-1
report: gzipped ps (January 2001)

Verification of a Wireless ATM Medium-Access Protocol
Natalia Sidorova and Martin Steffen
Universtity Kiel, Software Technology technical report TR-ST-00-3, May 2000
report: pdf,ps (May 2000)

Verifying Mascara Control
Natalia Sidorova and Martin Steffen
University Kiel, Software Technology technical report TR-ST-00-1,
report: gzipped ps (May 2000)

Polarized Higher-Order Subtyping (Extended Abstract)
Presented at the Types working group Workshop on Subtyping, inheritance and modular development of proofs , August 1997.
paper: pdf,ps (August 1997)

Formale Semantik für asynchronen Methodenaufruf (in German)
Uwe Nestmann , Martin Steffen, and Terry Stroup
In: R. Gotzhein and J. Bredereke, editors, Proceedings of the 5th `GI/ITG-Fachgespräch über Formale Beschreibungstechniken für verteilte Systeme' (Kaiserslautern, 22.-23. Juni 1995), pages 169-178, 1995
Also as University Erlangen IMMD technical report TR-17-95-11
report: pdf,ps (May 1995)

Confluent Processes for Transformation Correctness
Michael Egner and Uwe Nestmann and Martin Steffen.
University of Erlangen, Interner Bericht IMMD VII-01/95, January 1995

Higher Order Subtyping
Martin Steffen and Benjamin C. Pierce
University of Erlangen, Interner Bericht IMMD VII-01/94, January 1994. Also as LFCS technical report ECS-LFCS-94-280
report: pdf, ps (January 1994)

Kalülbasierte OO-Sprachen
Uwe Nestmann and Martin Steffen
University of Erlangen, Interner Bericht IMMD VII-02/94
report: pdf (January 1994)

Other (workshop contributions, extended abstracts, etc)

Lock-Polymorphic Behavior Inference for Deadlock Checking (extended abstract)
Ka I Pun, Martin Steffen, and Volker Stolz
Nordic Workshop of Programming Theory (NWPT'13).
paper: pdf (8. Nov. 2013)

Deadlock Checking by Data Race Detection (extended abstract)
Violet Ka I Pun, Martin Steffen, and Volker Stolz
Nordic Workshop of Programming Theory (NWPT'12).
paper: pdf, slides: pdf (31. October 2012)

Compositional Analysis of Resource Bounds for Software Transactions (extended abstract)
Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong
Nordic Workshop of Programming Theory (NWPT'12).
paper: pdf, slides: pdf, (2. Nov. 2012)

Observability and inheritance (extended abstract)
Erika Ábrahám, Thi Mai Thuong Tran, and Martin Steffen,
Nordic Workshop of Programming Theory (NWPT'11).
A longer version is available as University of Oslo, Department of Informatics Research Report 409
paper: pdf, slides: pdf (October 2011)

Estimating Resource Bounds for Software Transactions (extended abstract)
Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong
Nordic Workshop of Programming Theory (NWPT'11).
paper: pdf, slides: pdf, (October 2011)

Polymorphic behavioural lock effects for deadlock checking (extended abstract)
Ka I Pun, Martin Steffen, Volker Stolz
Nordic Workshop of Programming Theory (NWPT'11).
paper: pdf, slides: pdf (October. 2011)

Safe Locking for Multi-Threaded Java (extended abstract)
Einar Broch Johnsenn, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen.
Presented at NWPT'10
extended abstract: pdf (27. September 2010), slides

Deadlock checking by behavior inference for lock handling (extended abstract)
Ka I Pun and Martin Steffen.
Presented at NWPT'10
extended abstract: pdf (27. September 2010), slides

Model Testing Asynchronously Communicating Objects using Modulo AC Rewriting (extended abstract)
Martin Steffen, Arild Torjusen,
Proceedings of NWPT'09.
extended abstract: pdf (10.09.2009)

Safe Commits for Transactional Featherweight Java (extended abstract)
Martin Steffen, Thi Mai Thuong Tran
Presented at NWPT'09
extended abstract: pdf (10.09.2009),

A Specification-Driven Interpreter for Testing Asynchronous Creol Components (extended abstract)
Marcel Kyas, Andries Stam, Arild Torjusen, Martin Steffen.
Nordic Workshop of Programming Theory (NWPT'08), Talinn, November 2008.
extended abstractr: pdf (03.10.2008),

Test Driver Generation from Object-Oriented Interaction Traces (extended abstract)
Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, Martin Steffen
Nordic Workshop of Programming Theory (NWPT'07), October 2007
extended abstract: pdf (5.9.2007)

Abstract interface behavior of an object-oriented language with futures and promises (extended abstract)
Erika Ábrahám, Immo Grabe, Andreas Grüner, Martin Steffen
Nordic Workshop of Programming Theory (NWPT'07), October 2007
extended abstract: pdf (3.9.2007)
slides: pdf (10.10.2007)

Memory-aware Bounded Model Checking for Linear Hybrid Systems
Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen
Refereed workshop contribution for the 9th. workshop for Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV06), 20.-22.2. 2006, Dresden
paper: pdf (Jan. 2006)

Using Constraints for Model Checking Buffered Systems (Extended Abstract)
Claus Traulsen and Martin Steffen
Presented at the Nordic Workshop of Computing (NWPT'05)
extended abstract: pdf (13.9.2005)
slides: pdf

Classes, Object Connectivity, and Observability (extended abstract)
presented at Kolloquium Programmiersprachen und Grundlagen der Programmierung 17.-19. März 2004 Schloss Reinach, Freiburg-Munzingen
paper: pdf (30.04.2004)

Multithreaded Java with Exceptions (extended abstract)
presented at Kolloquium Programmiersprachen und Grundlagen der Programmierung 17.-19. März 2004 Schloss Reinach, Freiburg-Munzingen
paper: pdf (30.04.2004)

A Tool-supported Assertional Proof System for Multithreaded Java (extended abstract)
presented at the Ecoop-workshop about Formal Techniques for Java-like Programs (FTfJP), Darmstadt, 21.7.2003

Deductive Verification for Multithreaded Java (extended abstract)
Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen
Proceedings of the Kolloquium Programmiersprachen und Grundlagen der Programmierung, Rurberg 2001, pages 121-126
paper: gzipped ps, pdf

Bits and Pieces of Mascara Control Dragan Bosnacki, Dennis Dams, and Martin Steffen
Report of the Vires-project, 1 April 1998

Software

Accelerating Transducers
ocaml prototype implementation of for the theory of accelerating transducer-paper, status: research prototype implementation, not really usable externally, ask me for the code

Slides of (further) presentations

The Abstract Behavioral Specification (ABS) Language
Presentation (together with Jan Schaefer) at FMCO'10, Graz
slides: pdf (28.11.2010)

Observability & full abstraction for object-oriented languages
Talk at the College of Technology, Vietnam National University, Hanoi
slides: pdf (05.10.2010)

Inheritance & Observability
Talk at the Formal Methods seminar, Oslo
slides: pdf (03.05.2010)

Software transactional memory, automatic mutual exclusion etc.
Talk at the Formal Methods seminar, Oslo
slides: pdf (10.02. + 03.03.09)

Design of an abstract behavioral specification language
Presentation at FMCO'09, Eindhoven
slides: pdf (04.11.2009)

Creol as a formal model for concurrent, distributed objects
Invited presentation at Flacos'08, Malta
slides: pdf (27.11.08)

OO and Separation logic
Talk at the internal Formal Methods seminar, Olso
slides: pdf (30.09.08)

XML Query Languages
Habilitationsvortrag, i.e., the public presentation at my habilitation defense
slides: pdf (7.2.07)

Switching, Swapping, and Replay. Issues for an open semantics for a Java-like calculus
presented at the working-group ``Computer Science, Logics, and Mathematics''
slides: pdf (8.6.05)

Observability, Classes, and Object Connectivity
presented at the Summer Research Institute SRI 2004, EPFL, Lausanne and at the Universität Bamberg. (preliminary version have been presented at the MobiJ-workshop @ FMCO03, 3.11.03 and at Canterbury, 29.9.03)
slides: pdf (19.7. and 13.7.2004)

An Assertional Proof System for Multithreaded Java
presented at the Summer Research Institute SRI 2004, EPFL, Lausanne
slides: pdf (16.7.2004)

Programmierung eingebetter System mit Lego Mindstorms
Vortrag zum Tag der offenen Tür der Technischen Fakultät (faculty's day of the open door), 17th May, 2003
slides: pdf, infos: pdf (17.05.2003)

Towards full abstraction for multithreaded, class-based OO
Presented at the MobiJ workshop München, 6. February 2003 and at the working-group `` Computer Science, Logics, and Mathematics'', 4. December 2002.
slides: gzipped ps, pdf

Programmierung eingebetter System mit Lego Mindstorms
Vortrag zum Tag der offenen Tür (faculty's day of the open door), 4th May, 2002
slides: pdf gzipped ps (4.5.2002)

Embedding Chaos
working-group ``Computer Science, Logics, and Mathematics''
slides: gzipped ps, pdf (June 2001)

Iterating transducers
Joint work with Dennis Dams and Yassine Lakhnech
University of Chicago, Friday Seminar
slides: pdf (30.03.2001)

Verification of Mascara control
joint work with Natalia Sidorova
presented at the Vires review, 16th June 2000
slides: pdf, ps (16.06.2000)

Accelerating transducers
Joint work with Dennis Dams and Yassine Lakhnech
Vires review, 16th June 2000
slides: pdf, ps (16.06.2000)

Fehlerfreie Software?
Vortrag zum Tag der offenen Tür (University's day of the open door), 7th May, 2000
slides: pdf, ps (7.5.2000)

Polarized higher-order subtyping
Brics, Aalborg
slides: pdf, ps (15. April 1999)

OO: issues and problems
Seminar talk (in German)
slides: pdf, ps (January 1999)

Dynamic control
Vires-project talk about parts of the Mascara protocol, November 1998, Plasmolen

Verifikation objektorientierter Programme
presented in the working-group ``Computer Science, Logics, and Mathematics''
slides: pdf, ps (June 1998)


[theses] [papers] [ongoing] [tech reports] [editor] [other] [software] [presentations] [BibTeX]

($Id: papers.html 9958 2007-06-25 16:47:16Z msteffen $)