steffen.bib

@inproceedings{abraham*:fa-sequential,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Marcello M.
		  Bonsangue and Andreas Gr{\"u}ner and Martin Steffen},
  title = {Observability, Connectivity, and Replay in a Sequential
		  Calculus of Classes},
  crossref = {lncs3657},
  pages = {296--316 (21 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/fa-fmco.pdf},
  date = {1.7.2005},
  abstract = {Object calculi have been investigated as semantical
		  foundation for object-oriented languages. Often, they are
		  object-based, whereas the mainstream of object-oriented
		  languages is \emph{class-based.}
		  
		  Considering classes as part of a component makes
		  instantiation a possible interaction between component and
		  environment. As a consequence, one needs to take
		  \emph{connectivity} information into account.
		  
		  We formulate an operational semantics that incorporates the
		  connectivity information into the scoping mechanism of the
		  calculus. Furthermore, we formalize a notion of equivalence
		  on traces which captures the uncertainty of observation
		  cause by the fact that the observer may fall into separate
		  groups of objects. We use a corresponding trace semantics
		  for full abstraction wrt. a simple notion of observability.
		  This requires to capture the notion of \emph{determinism}
		  for traces where classes may be instantiated into more than
		  one instance during a run and showing thus twice an
		  equivalent behavior (doing a ``replay''), a problem absent
		  in an object-based setting.},
  keywords = {class-based object-oriented languages, formal semantics,
		  determinism, full abstraction}
}
@article{abraham*:futures,
  author = {Erika {\'A}brah{\'a}m and Immo Grabe and Andreas
		  Gr{\"u}ner and Martin Steffen},
  title = {Behavioral interface description of an object-oriented
		  language with futures and promises},
  year = 2009,
  journal = {Journal of Logic and Algebraic Programming},
  publisher = {Elsevier Science Publishers},
  volume = 78,
  number = 7,
  pages = {491-518 (28 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/09/futures.pdf},
  note = {Special issue with selected contributions of NWPT'07. The
		  paper is a reworked version of an earlier UiO Technical
		  Report TR-364, Oct.\ 2007},
  annote = {Revised submission 07.01.2009},
  doi = {http://dx.doi.org/10.1016/j.jlap.2009.01.001}
}
@inproceedings{abraham*:futures-nwpt,
  author = {Erika {\'A}brah{\'a}m and Immo Grabe and Andreas
		  Gr{\"u}ner and Martin Steffen},
  title = {Abstract Interface Behavior of an Object-Oriented Language
		  with Futures and Promises (extended abstract)},
  crossref = {nwpt07},
  url = {http://www.ifi.uio.no/~msteffen/download/07/futures-short.pdf},
  annote = {31.08.07 (submission)}
}
@techreport{abraham*:futures-rep,
  author = {Erika {\'A}brah{\'a}m and Immo Grabe and Andreas
		  Gr{\"u}ner and Martin Steffen},
  title = {Behavioral Interface Description of an Object-Oriented
		  Language with Futures and Promises},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2007,
  type = {Technical Report},
  number = 364,
  note = {38 pages},
  pages = {38 pages},
  isbn = {82-7368-322-2},
  issn = {0806-3036},
  month = oct,
  url = {http://www.ifi.uio.no/~msteffen/download/07/futures-rep.pdf}
}
@inproceedings{abraham*:memoryaware,
  author = {Erika {\'A}brah{\'a}m and Marc Herbstritt and Bernd Becker
		  and Martin Steffen},
  title = {Memory-Aware Bounded Model Checking for Linear Hybrid
		  Systems},
  booktitle = {Proceedings of the 9th. Workshop for ``Methoden und
		  Beschreibungssprachen zur Modellierung und Verifikation von
		  Schaltungen und Systemen'' (MBMV06)},
  year = 2006,
  month = jan,
  note = {10 pages},
  abstract = {Bounded Model Checking (BMC) is a successful method for
		  refuting properties of erroneous systems. Initially applied
		  to discrete systems only, BMC could be extended to more
		  complex domains like linear hybrid automata. the increasong
		  complexity coming along with these complex models, but also
		  recent optomizations of SAT-based BMC, like excessive
		  conflict learning, reveal a memory explosion problem
		  especially for deep counterexamples. In this paper we
		  introduce parametric data types for internal solver
		  structure that, taking advantage of the symmetry of BMC
		  problems, remarkably reduce the memory requirements of the
		  solver.},
  url = {http://www.ifi.uio.no/~msteffen/download/06/memoryaware.pdf}
}
@inproceedings{abraham*:optimizingbmc,
  author = {Erika {\'A}brah{\'a}m and Bernd Becker and Felix Klaedke
		  and Martin Steffen},
  title = {Optimizing Bounded Model Checking for Linear Hybrid
		  Systems},
  crossref = {lncs3385},
  pages = {396-412 (17 pages)},
  abstract = { Bounded model checking (BMC) is an automatic verification
		  method that is based on finitely unfolding the system's
		  transition relation. BMC has been successfully applied, in
		  particular, for discovering bugs in digital system design.
		  Its success is based on the effectiveness of satisfiability
		  solvers that are used to check for a finite unfolding
		  whether a violating state is reachable.
		  
		  In this paper we improve the BMC approach for linear hybrid
		  systems. Our improvements are tailored to lazy
		  satisfiability solving and follow two complementary
		  directions. First, we optimize the formula representation
		  of the finite unfoldings of the transition relations of
		  linear hybrid systems, and second, we accelerate the
		  satisfiability checks by accumulating and generalizing data
		  that is generated during earlier satisfiability checks.
		  
		  Experimental results show that the presented techniques
		  accelerate the satisfiability checks significantly.},
  url = {http://www.ifi.uio.no/~msteffen/download/05/optimizingbmc.pdf}
}
@techreport{abraham*:optimizingbmc-rep,
  author = {Erika {\'A}brah{\'a}m and Bernd Becker and Felix Klaedke
		  and Martin Steffen},
  title = {Optimizing Bounded Model Checking for Linear Hybrid
		  Systems},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg, Fakult{\"a}t
		  f{\"u}r Angewandte Wissenschaften, Institut f{\"u}r
		  Informatik},
  year = {2004},
  number = {TR214},
  month = nov,
  url = {http://www.informatik.uni-freiburg.de/tr/},
  abstract = {Bounded model checking (BMC) is an automatic verification
		  method that is based on finitely unfolding the system's
		  transition relation. BMC has been successfully applied, in
		  particular, for discovering bugs in digital system design.
		  Its success is based on the effectiveness of satisfiability
		  solvers that are used to check for a finite unfolding
		  whether a violating state is reachable.
		  
		  In this report we improve the BMC approach for linear
		  hybrid systems. Our improvements are tailored to lazy
		  satisfiability solving and follow two complementary
		  directions. First, we optimize the formula representation
		  of the finite unfoldings of the transition relations of
		  linear hybrid systems, and second, we accelerate the
		  satisfiability checks by accumulating and generalizing data
		  that is generated during earlier satisfiability checks.
		  
		  Experimental results show that the presented techniques
		  accelerate the satisfiability checks significantly.},
  type = {Technical report}
}
@article{abraham*:parametric,
  author = {Erika {\'A}brah{\'a}m and Marc Herbstritt and Bernd Becker
		  and Martin Steffen},
  title = {Bounded Model Checking with Parametric Data Structures},
  year = 2007,
  note = {Special Issue for the Proceedings of the Fourth
		  International Workshop on Bounded Model Checking (BMC06)},
  url = {http://portal.acm.org/citation.cfm?id=1244814#},
  publisher = {Elsevier Science},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = 174,
  number = 3,
  month = may,
  pages = {3--16 (14 pages)},
  doi = {10.1016/j.entcs.2006.12.019},
  abstract = {Bounded Model Checking (BMC) is a successful refutation
		  method for detecting errors in not only circuits and other
		  binary systemsm but also in systems with more complex
		  domains like timed automata or linear hybrid automata.
		  Counterexamples of a fixed length are described by formulas
		  in a decidable logic, and checked for statisfiability by a
		  suitable solver.
		  
		  In an earlier paper we analyzed how BMC of linear hybrid
		  automata can be accelerated alread by appropriate encodung
		  of counterexamples as formulas and by selective conflict
		  learning. In this paper we introduce parametric datatypes
		  for the internal solver structure that, taking advantage of
		  the symmetry of BMC problems, remarkably reduce the memory
		  requirements of the solver.}
}
@inproceedings{abraham.deboer.deroever.steffen:deductiveverification,
  author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  title = {Deductive Verification for Multithreaded {Java} (Extended
		  abstract)},
  booktitle = {Proceedings of the ``11. Kolloquium Programmiersprachen
		  und Grundlagen der Programmierung'', 2001, Rurberg},
  pages = {121--126},
  year = {2001}
}
@techreport{abraham.bonsangue.deboer.steffen:classcalc-rep,
  author = {Erika {\'A}brah{\'a}m and Marcello M. Bonsangue and Frank
		  S. de Boer and Martin Steffen},
  title = {A Structural Operational Semantics for a Concurrent Class
		  Calculus},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2003,
  type = {Technical Report},
  number = 0307,
  month = aug,
  url = {http://www.informatik.uni-kiel.de/reports/2003/0307.html},
  abstract = {The concurrent $\nu$-calculus has been investigated as a
		  core calculus for imperative, object-oriented languages
		  with multithreading and heap-allocated objects. From an
		  abstract point of view, the combination of this form of
		  concurrency with objects corresponds to features known from
		  the popular language Java. One distinctive feature,
		  however, of the concurrent object calculus is that it is
		  object-based, where as the mainstream of object-oriented
		  languages is class-based. This technical report extends the
		  concurrent $\nu$-calculus by introducing classes and
		  explores some of the semantical consequences. The semantics
		  will serve as the basis for a proof of full abstraction
		  wrt. to a may-testing based notion of observability.}
}
@inproceedings{abraham.bonsangue.deboer.steffen:connectivity-freiburgmunzingen,
  author = {Erika {\'A}brah{\'a}m and Marcello M. Bonsangue and Frank
		  S. de Boer and Martin Steffen},
  title = {Classes, Object Connectivity, and Observability (Extended
		  abstract)},
  booktitle = {Informal Electronic Proceedings of the ``12. Kolloquium
		  Programmiersprachen und Grundlagen der Programmierung''},
  year = 2004,
  month = apr,
  publisher = {University Freiburg},
  url = {http://nakalele.informatik.uni-freiburg.de/cgi/KPS2004.cgi}
}
@inproceedings{abraham.bonsangue.deboer.steffen:fa,
  author = {Erika {\'A}brah{\'a}m and Marcello M. Bonsangue and Frank
		  S. de Boer and Martin Steffen},
  title = {Object Connectivity and Full Abstraction for a Concurrent
		  Calculus of Classes},
  year = 2004,
  month = jul,
  crossref = {lncs3407},
  doi = {DOI: 10.1007/978-3-540-31862-0_5},
  pages = {37--51 (15 pages)},
  url = {http://www-omega.imag.fr/doc/d1000313_1/WP11-D115-313-V1-fa.pdf},
  abstract = {The concurrent object calculus has been investigated as a
		  core calculus for imperative, object-oriented languages
		  with multithreading and heap-allocated objects. The
		  combination of this form of concurrency with objects
		  corresponds to features known from the popular language
		  \textsl{Java.} One distinctive feature, however, of the
		  concurrent object calculus is that it is
		  \emph{object-based}, whereas the mainstream of
		  object-oriented languages is \emph{class-based.}
		  
		  This work explores the semantical consequences of
		  introducing classes to the calculus. Considering classes as
		  part of a component makes instantiation a possible
		  interaction between component and environment. A striking
		  consequence is that to characterize the observable behavior
		  we must take \emph{connectivity} information into account,
		  i.e., the way objects may have knowledge of each other. In
		  particular, unconnected environment objects can neither
		  determine the absolute order of interaction and furthermore
		  cannot exchange information to compare object identities.
		  
		  We formulate an operational semantics that incorporates the
		  connectivity information into the scoping mechanism of the
		  calculus. As instantiation itself is unobservable, objects
		  are instantiated only when accessed for the first time
		  (``\emph{lazy instantiation}'').
		  
		  Furthermore we use a corresponding trace semantics for full
		  abstraction wrt. a may-testing based notion of
		  observability.},
  keywords = {multithreading, class-based object-oriented languages,
		  formal semantics, full abstraction}
}
@techreport{abraham.bonsangue.deboer.steffen:fa-rep,
  author = {Erika {\'A}brah{\'a}m and Marcello M. Bonsangue and Frank
		  S. de Boer and Martin Steffen},
  title = {Object Connectivity and Full Abstraction for a Concurrent
		  Calculus of Classes},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2005,
  month = jan,
  type = {Preliminary Technical Report},
  annote = {Available at \url{http://www.informatik.uni-kiel.de/~ms}},
  url = {http://www.informatik.uni-kiel.de/~ms}
}
@article{abraham.deboer.deroever.steffen:assertionbased,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {An Assertion-Based Proof System for Multithreaded {J}ava},
  journal = {Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  year = 2005,
  volume = 331,
  doi = {10.1016/tcs.2004.09.019},
  pages = {251-290 (40 pages)}
}
@article{abraham.deboer.deroever.steffen:exceptions,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {A Deductive Proof System for Multithreaded {J}ava with
		  Exceptions},
  journal = {Fundamenta Informaticae},
  year = 2008,
  volume = 82,
  number = 4,
  pages = {391-463 (73 pages)},
  note = {An extended version of the 2005 conference contribution to
		  FSEN'05 and a reworked and shortened version of the
		  University of Kiel, Dept. of Computer Science technical
		  report 0303},
  urllocal = {http://www.ifi.uio.no/~msteffen/download/07/exceptions-journal.pdf},
  url = {http://iospress.metapress.com/content/g082364hgk01l773/},
  annote = {Submitted 18.07 2006. Resubmitted as final version
		  29.05.2007}
}
@inproceedings{abraham.deboer.deroever.steffen:exceptions-fsen,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {Inductive Proof Outlines for Exceptions in Multithreaded
		  {J}ava},
  crossref = {entcs-fsen05},
  abstract = {In this paper we give an operational semantics and
		  introduce an assertional proof system for exceptions in a
		  multithreaded Java sublanguage.},
  url = {http://www.ifi.uio.no/~msteffen/download/05/fsen05.pdf},
  finaldate = {18.11.2005},
  date = {18.5.2006},
  pages = {281-297 (17 pages)},
  note = {An extended version appeared in Fundamentae Informaticae},
  keywords = {Java, multi-threading, exceptions, proof systems}
}
@techreport{abraham.deboer.deroever.steffen:exceptions-rep,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {Inductive Proof Outlines for Multithreaded {J}ava with
		  Exceptions},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2003,
  month = dec,
  type = {Technical Report},
  annnote = {Available at
		  \url{http://www.informatik.uni-kiel.de/reports/2003/0313.html
		  }},
  number = {0313},
  url = {http://www.informatik.uni-kiel.de/reports/2003/0313.html},
  abstract = {Besides the features of a class-based object-oriented
		  language, Java integrates concurrency via its
		  thread-classes, allowing for a multithreaded flow of
		  control. Besides that, the language offers a flexible
		  exception mechanism for handling errors or exceptional
		  program conditions.
		  
		  To reason about safety-properties Java-programs and
		  extending previous work on the proof theory for monitor
		  synchronization, we introduce in this report an
		  \emph{assertional proof method} for JavaMT{}
		  (``\emph{Multi-Threaded Java}''), a small concurrent
		  sublanguage of Java, covering concurrency and especially
		  \emph{exception handling.} We show soundness and relative
		  completeness of the proof method.}
}
@techreport{abraham.deboer.deroever.steffen:hoarelogic-rep,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {A {H}oare Logic for Monitors in {J}ava},
  institution = {Lehrstuhl f{{\"u}r} Software-Technologie, Institut f{\"u}r
		  Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2003,
  type = {Techical report},
  number = {TR-ST-03-1},
  month = apr,
  pages = {80 pages},
  note = {80 pages},
  annote = {Available at
		  \url{http://www.informatik.uni-kiel.de/inf/deRoever/techreports/03/tr-st-03-1.pdf
		  }},
  url = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/03/tr-st-03-1.pdf},
  abstract = {Besides the features of a class-based object-oriented
		  language, \textsl{Java} integrates concurrency via its
		  thread-classes, allowing for a \emph{multithreaded} flow of
		  control. The concurrency model includes
		  \emph{shared-variable} concurrency via instance variables,
		  \emph{coordination} via reentrant synchronization monitors,
		  \emph{synchronous message passing,} and dynamic
		  \emph{thread creation.} To reason about safety-properties
		  of multithreaded programs, we introduce in this paper a
		  tool-supported \emph{assertional proof method} for
		  \textsl{Java}$_\mathit{MT}$ (``\emph{Multi-Threaded
		  Java}''), a small concurrent sublanguage of \textsl{Java},
		  covering the mentioned concurrency issues as well as the
		  object-based core of \textsl{Java}, i.e., object creation,
		  side effects, and aliasing, but leaving aside inheritance
		  and subtyping. We show soundness and relative completeness
		  of the proof method.}
}
@inproceedings{abraham.deboer.deroever.steffen:inductive,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {Inductive Proof-Outlines for Monitors in {J}ava},
  crossref = {lncs2884},
  pages = {155--169 (15 pages)},
  note = {A longer version appeared as technical report TR-ST-03-1,
		  April 2003},
  url = {XXXXhttp://www.informatik.uni-kiel.de/inf/deRoever/techreports/03/tr-st-03-1.pdf},
  abstract = {The research concerning Java's semantics and proof theory
		  has mainly focussed on various aspects of sequential
		  sub-languages. Java, however, integrates features of a
		  class-based object-oriented language with the notion of
		  multi-threading, where multiple threads can concurrently
		  execute and exchange information via shared instance
		  variables. Furthermore, each object can act as a monitor to
		  assure mutual exclusion or to coordinate between threads.
		  
		  In this paper we present a sound and relatively complete
		  assertional proof system for Java's monitor concept, which
		  generates verification conditions for a concurrent
		  sublanguage JavaMT of Java. This work extends previous
		  results by incorporating Java's monitor methods.},
  keywords = {OO, Java, multithreading, monitors, deductive
		  verification, proof-outlines}
}
@article{abraham.gruener.steffen:heapabstraction,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Heap-Abstraction for an Object-Oriented Calculus with
		  Thread Classes},
  journal = {Journal of Software and Systems Modelling (SoSyM)},
  publisher = {Springer Verlag},
  pages = {177-208 (32 pages)},
  volume = 7,
  number = 2,
  month = may,
  year = 2008,
  date = {published online 21.08.2007},
  doi = {10.1007/s10270-007-0065-9},
  url = {http://springerlink.metapress.com/content/dqxhn70707442838/fulltext.pdf},
  annote = {(Re)-submitted 23.08.2006. This is a reworked version of
		  the Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel technical report nr. 0601 and an extended version of the
		  CiE'06 extended abstract}
}
@inproceedings{abraham.gruener.steffen:heapabstraction-cie,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Dynamic Heap-Abstraction for Open, Object-Oriented Systems
		  with Thread Classes (Extended Abstract)},
  crossref = {lncs3988},
  pages = {1--10 (10 pages)},
  note = {A preliminary version has been included in the informal
		  workshop proceedings of Cosmicah'05, as Queen Mary
		  Technical Report RR-05-04, a longer version has been
		  published as Technical Report 0601 of the Institute of
		  Computer Science of the University Kiel, January 2006},
  url = {http://www.ifi.uio.no/~msteffen/download/06/heapabstraction.pdf},
  doi = {http://dx.doi.org/10.1007/11780342_1},
  annote = {Rejected for ICTAC 2005, Also submitted as workshop
		  contribution for Cosmicah 2005 under the title
		  ``Heap-Abstraction for an Object-Oriented Calculus with
		  Thread Classes''.},
  abstract = {This paper formalizes an open semantics for a calculus
		  featuring thread classes, where the environment, consisting
		  in particular of an overapproximation of the heap topology,
		  is abstractly represented.
		  
		  From an observational point of view, considering classes as
		  part of a component makes instantiation a possible
		  interaction between component and environment or observer.
		  For \emph{thread classes} it means that a component may
		  create external activity, which influences what can be
		  observed. The fact that cross-border instantiation is
		  possible requires that the \emph{connectivity} of the
		  objects needs to be incorporated into the semantics.
		  
		  We extend our prior work not only by adding thread classes,
		  but also in that thread names may be \emph{communicated,}
		  which means that the semantics needs to account explicitly
		  for the possible acquaintance of objects with threads. We
		  show soundness of the abstraction.},
  keywords = {class-based oo languages, thread-based concurrency, open
		  systems, formal semantics, heap abstraction, observable
		  behavior}
}
@inproceedings{abraham.gruener.steffen:heapabstraction-cosmicah05,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Dynamic Heap-Abstraction for Open, Object-Oriented Systems
		  with Thread Classes},
  booktitle = {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},
  editor = {Radu Iosif and Dino Distefano},
  month = jul,
  year = 2005,
  pages = {47--61 (14 pages)}
}
@techreport{abraham.gruener.steffen:heapabstraction-rep,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Dynamic Heap-Abstraction for Open, Object-Oriented Systems
		  with Thread Classes},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2006,
  pages = {40 pages},
  month = jan,
  url = {http://www.informatik.uni-kiel.de/reports/2006/0601.html},
  type = {Technical Report},
  number = 0601,
  date = {1.2.2006},
  note = {40 pages. A slightly shorter version is accepted for
		  inclusion into the Journal of Software and Systems Modeling
		  (SoSym)},
  abstract = {This paper formalizes an open semantics for a calculus
		  featuring thread classes, where the environment, consisting
		  in particular of an overapproximation of the heap topology,
		  is abstractly represented.
		  
		  From an observational point of view, considering classes as
		  part of a component makes instantiation a possible
		  interaction between component and environment or observer.
		  For \emph{thread classes} it means that a component may
		  create external activity, which influences what can be
		  observed. The fact that cross-border instantiation is
		  possible requires that the \emph{connectivity} of the
		  objects needs to be incorporated into the semantics.
		  
		  We extend our prior work not only by adding thread classes,
		  but also in that thread names may be \emph{communicated,}
		  which means that the semantics needs to account explicitly
		  for the possible acquaintance of objects with threads. We
		  show soundness of the abstraction.},
  keywords = {class-based oo languages, thread-based concurrency, open
		  systems, formal semantics, heap abstraction, observable
		  behavior}
}
@inproceedings{abraham.gruener.steffen:monitors,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Abstract Interface Behavior of Object-Oriented Languages
		  with Monitors},
  crossref = {lncs4037},
  abstract = {We characterize the observable behavior of multi-threaded,
		  object-oriented programs with \emph{re-entrant monitors.}
		  The observable uncertainty at the interface is captured by
		  may- and must-approximations for potential resp. necessary
		  lock ownership. The concepts are formalized in an object
		  calculus. We show the soundness of the abstractions.},
  keywords = {oo languages, formal semantics, thread-based concurrency,
		  monitors, open systems, observable behavior},
  date = {20.1.2006},
  pages = {218--232 (15 pages)},
  doi = {10.1007/s00224-007-9047-0},
  url = {http://www.springerlink.com/content/3365g26781740807},
  urlx = {http://www.ifi.uio.no/~msteffen/download/06/monitors.pdf}
}
@techreport{abraham.gruener.steffen:monitors-rep,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Abstract Interface Behavior of Object-Oriented Languages
		  with Monitors},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2006,
  type = {Technical Report},
  number = 0612,
  month = oct,
  pages = {43 pages},
  note = {43 pages},
  annote = {31.10.06}
}
@article{abraham.gruener.steffen:monitors-tocs,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {Abstract Interface Behavior of Object-Oriented Languages
		  with Monitors},
  keywords = {oo languages, formal semantics, thread-based concurrency,
		  monitors, open systems, observable behavior},
  journal = {Theory of Computing Systems},
  publisher = {Springer Verlag},
  volume = 43,
  number = {3-4},
  date = {03.10.2007},
  doi = {10.1007/s00224-007-9047-0},
  year = 2008,
  month = dec,
  pages = {322-361 (40 pages)},
  annote = {Published online 3. Oct. 2007},
  url = {http://www.ifi.uio.no/~msteffen/download/07/monitors-tocs.pdf}
}
@article{abraham.tran.steffen:inheritance,
  author = {Erika {\'A}brah{\'a}m and Thi {Mai Thuong Tran} and Martin
		  Steffen},
  title = {Observable interface behavior and inheritance},
  journal = {Mathematical Structures in Computer Science (Special Issue on Behavioral Types)},
  note = {Published online 13 November 2014. The paper is a reworked
		  version of the earlier UiO IFI technical report 409},
  month = nov,
  volume = 26,
  pages = {561-605},
  xpages = {1--45},
  year = 2014,
  publisher = {Cambridge University Press},
  issn = {1469-8072},
  xnumpages = 45,
  annote = {original submission 2011? final submission 20.12.2013. See
		  also at {\tt 13/inheritance.pdf}},
  doi = {10.1017/S0960129514000255},
  url = {http://journals.cambridge.org/article_S0960129514000255}
}
@inproceedings{abraham.tran.steffen:inheritance-nwpt,
  author = {Erika {\'A}brah{\'a}m and Thi {Mai Thuong Tran} and Martin
		  Steffen},
  title = {Observable interface behavior and inheritance (extended
		  abstract)},
  crossref = {nwpt11},
  url = {http://www.ifi.uio.no/~msteffen/download/11/inheritance-nwpt.pdf},
  annote = {112--114}
}
@techreport{abraham.tran.steffen:inheritance-rep,
  author = {Erika {\'A}brah{\'a}m and Thi {Mai Thuong Tran} and Martin
		  Steffen},
  title = {Observable interface behavior and inheritance},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2011,
  month = apr,
  type = {Technical Report},
  number = 409,
  pages = {43 pages},
  isbn = {82-7368-368-0},
  issn = {806-3036},
  note = {\url{www.ifi.uio.no/~msteffen/publications.html#techreports}},
  annote = {submitted for MSCS special issue}
}
@inproceedings{abrahammumm.deboer.deroever.steffen:compositionalsemantics,
  author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul
		  de Roever and Martin Steffen},
  title = {A Compositional Operational Semantics for
		  {Java$_{\mathit{MT}}$}},
  crossref = {lncs2772},
  pages = {290--303 (14 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/XXXX},
  note = {A preliminary version appeared as Technical Report
		  TR-ST-02-2, May 2002},
  abstract = {Besides the features of a class-based object-oriented
		  language, \textsl{Java} integrates concurrency via its
		  thread-classes, allowing for a \emph{multithreaded} flow of
		  control. The concurrency model includes
		  \emph{shared-variable} concurrency via instance variables,
		  \emph{coordination} via reentrant synchronization monitors,
		  \emph{synchronous message passing,} and dynamic
		  \emph{thread creation.} This report contains a
		  compositional version of the operational semantics of
		  {\textsl{Java}$_{\mathit{MT}$}}.},
  xurl = {http://www.informatik.uni-kiel.de/~ms}
}
@techreport{abrahammumm.deboer.deroever.steffen:compositionalsemantics-rep,
  author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  title = {A Compositional Operational Semantics for
		  {Java$_{\mathit{MT}}$}},
  institution = {Lehrstuhl f{{\"u}r} Software-Technologie, Institut f{\"u}r
		  Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2002,
  type = {Technical Report},
  number = {TR-ST-02-2},
  pages = {15 pages},
  note = {15 pages},
  month = may,
  url = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/02/tr-st-02-2.ps.gz},
  abstract = {Besides the features of a class-based object-oriented
		  language, \textsl{Java} integrates concurrency via its
		  thread-classes, allowing for a \emph{multithreaded} flow of
		  control. The concurrency model includes
		  \emph{shared-variable} concurrency via instance variables,
		  \emph{coordination} via reentrant synchronization monitors,
		  \emph{synchronous message passing,} and dynamic
		  \emph{thread creation.} This report contains a
		  compositional version of the operational semantics of
		  {\textsl{Java}$_{\mathit{MT}$}}.\mbox{}}
}
@inproceedings{abrahammumm.deboer.deroever.steffen:multithreading,
  author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  title = {Verification for {J}ava's Reentrant Multithreading
		  Concept},
  crossref = {lncs2303},
  pages = {4--20 (17 pages)},
  note = {A longer version, including the proofs for soundness and
		  completeness, appeared as Technical Report TR-ST-02-1,
		  March 2002},
  url = {http://www.ifi.uio.no/~msteffen/download/XXXX},
  abstract = {Besides the features of a class-based object-oriented
		  language, Java{} integrates concurrency via its
		  thread-classes, allowing for a \emph{multithreaded} flow of
		  control. The concurrency model offers \emph{coordination}
		  via lock-synchronization, and \emph{communication} by
		  synchronous message passing, including re-entrant method
		  calls, and by instance variables shared among threads.
		  
		  To reason about multithreaded programs, we introduce in
		  this paper an \emph{assertional proof method} for JavaMT{}
		  (``\emph{Multi-Threaded Java}''), a small concurrent
		  sublanguage of Java, covering the mentioned concurrency
		  issues as well as the object-based core of Java, i.e.,
		  object creation, side effects, and aliasing, but leaving
		  aside inheritance and subtyping.}
}
@techreport{abrahammumm.deboer.deroever.steffen:multithreading-rep,
  author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  title = {Verification for {J}ava's Reentrant Multithreading
		  Concept: {S}oundness and Completeness},
  institution = {Lehrstuhl f{{\"u}r} Software-Technologie, Institut f{\"u}r
		  Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2002,
  type = {Technical Report},
  number = {TR-ST-02-1},
  pages = {95 pages},
  note = {95 pages},
  abstract = {Besides the features of a class-based object-oriented
		  language, Jav integrates concurrency via its
		  thread-classes, allowing for a \emph{multithreaded} flow of
		  control. The concurrency model includes
		  \emph{shared-variable} concurrency via instance variables,
		  \emph{coordination} via reentrant synchronization monitors,
		  \emph{synchronous message passing,} and dynamic
		  \emph{thread creation.}
		  
		  To reason about multithreaded programs, we introduce in
		  this paper an \emph{assertional proof method} for safety
		  properties for JavaMT{} (``\emph{Multi-Threaded Java}''), a
		  small concurrent sublanguage of Java, covering the
		  mentioned concurrency issues as well as the object-based
		  core of Java, i.e., object creation, side effects, and
		  aliasing, but leaving aside inheritance and subtyping. We
		  show soundness and relative completeness of the proof
		  method.},
  url = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports}
}
@inproceedings{abrahammumm.deboer.deroever.steffen:toolsupported,
  author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and
		  Willem-Paul de Roever and Martin Steffen},
  title = {A Tool-Supported Proof System for Monitors in {J}ava},
  crossref = {lncs2852},
  pages = {1--32 (33 pages)},
  year = 2002,
  url = {http://www.ifi.uio.no/~msteffen/download/XXXX},
  abstract = {To reason about safety properties of multithreaded Java
		  programs, we introduce a tool-supported \emph{assertional
		  proof method} for JavaMT{} (``\emph{Multi-Threaded
		  Java}''), a sublanguage of Java, covering the mentioned
		  concurrency issues as well as the object-based core of
		  Java. The verification method is formulated in terms of
		  proof-outlines, where the assertions are layered into local
		  ones specifying the behavior of a single instance, and
		  global ones taking care of the connections between objects.
		  From the annotated program, a number of verification
		  conditions are generated and handed over to the interactive
		  theorem prover PVS. We illustrate the use of the proof
		  system on an example.}
}
@inproceedings{abrahammumm.hannemann.steffen:assertionbased-eurocast,
  author = {Erika {\'A}brah{\'a}m-Mumm and Ulrich Hannemann and Martin
		  Steffen},
  title = {Assertion-Based Analysis of Hybrid Systems with {PVS}},
  year = 2001,
  pages = {94-109 (16 pages)},
  crossref = {lncs2178},
  url = {http://www.ifi.uio.no/~msteffen/download/01/assertionbased.pdf}
}
@inproceedings{abrahammumm.hannemann.steffen:verification,
  author = {Erika {\'A}brah{\'a}m-Mumm and Ulrich Hannemann and Martin
		  Steffen},
  title = {Verification of Hybrid Systems: Formalization and Proof
		  Rules in {PVS}},
  year = 2001,
  booktitle = {Proceedings of the Seventh IEEE International Conference
		  on Engineering of Complex Computer Systems (ICECCS 2001)},
  note = {10 pages. A preliminary and longer version appeared as
		  technical report TR-ST-01-1}
}
@techreport{abrahammumm.hannemann.steffen:verification-rep,
  author = {Erika {\'A}brah{\'a}m-Mumm and Ulrich Hannemann and Martin
		  Steffen},
  title = {Verification of Hybrid Systems: Formalization and Proof
		  Rules in {PVS}},
  year = 2001,
  institution = {Lehrstuhl f{{\"u}r} Software-Technologie, Institut f{\"u}r
		  Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  number = {TR-ST-01-1},
  month = jan,
  abstract = {Combining discrete state-machines with continuous
		  behavior, hybrid systems are a well-established
		  mathematical model for discrete systems acting in a
		  continuous environment. As a priori \emph{infinite} state
		  systems, their computational properties are undecidable in
		  the general model and the main line of research
		  concentrates on model checking of finite abstractions of
		  restricted subclasses of the general model. In our work, we
		  use \emph{deductive methods}, falling back upon the
		  general-purpose theorem prover PVS.
		  
		  To do so we extend the classical approach for the
		  verification of state-based programs by developing an
		  inductive proof method to deal with the parallel
		  composition of hybrid systems. The methods cover shared
		  variable communication, label-synchronization, and
		  especially the common continuous activities in the parallel
		  composition of hybrid automata. Besides hybrid systems and
		  their parallel composition, we formalized their operational
		  step semantics and a number of proof-rules within PVS, for
		  one of which we give also a rigorous completeness proof.
		  Moreover, the theory is applied to the verification of a
		  number of examples.}
}
@inproceedings{bodden*:informationflowgo,
  author = {Eric Bodden and Ka I Pun and Martin Steffen and Volker
		  Stolz and Anna-Katharina Wickert},
  title = {Information Flow Analysis for {Go}},
  crossref = {lncs9952},
  pages = {431-445}
}
@article{dams.lakhnech.steffen:iterating,
  author = {Dennis Dams and Yassine Lakhnech and Martin Steffen},
  title = {Iterating Transducers},
  journal = {Journal of Logic and Algebraic Programming, special issue
		  on Model Checking},
  publisher = {Elsevier Science Publishers},
  year = 2002,
  volume = {52--53},
  month = jul,
  pages = {109--127 (19 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/02/iterating-jlap.pdf},
  note = {This is an extended version of the conference version
		  under the same title, Computer Aided Verification (CAV'01),
		  LNCS 2102}
}
@inproceedings{dams.lakhnech.steffen:iterating-cav,
  author = {Dennis Dams and Yassine Lakhnech and Martin Steffen},
  title = {Iterating Transducers},
  crossref = {lncs2102},
  pages = {286--297 (12 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/01/iterating.pdf}
}
@techreport{dams.lakhnech.steffen:iterating-rep,
  author = {Dennis Dams and Yassine Lakhnech and Martin Steffen},
  title = {Iterating Transducers for Safety of Abstraction},
  institution = {Christian-Albrechts-Universit{\"a}t, Lehrstuhl
		  Softwaretechnologie},
  year = 2000,
  type = {Internal Report},
  number = {TR-ST-00-2},
  month = may,
  annote = {This one is online available.}
}
@inproceedings{deboer*:automatedtestdriver-nltestday,
  author = {Frank S. de Boer and Marcello M. Bonsangue and Andreas
		  Gr{\"u}ner and Martin Steffen},
  title = {Automated Test Driver Generation for {J}ava Components},
  booktitle = {Netherland's Testing Day ``TestDag'08'', Delft},
  year = 2008,
  month = nov,
  xxxpages = {2 pages},
  note = {White Paper},
  url = {http://www.ifi.uio.no/~msteffen/download/08/testdag08-abstract.pdf}
}
@inproceedings{deboer*:fa-uml,
  author = {Frank S. de Boer and Marcello M. Bonsangue and Martin
		  Steffen and Erika {\'A}brah{\'a}m},
  title = {A Fully Abstract Trace Semantics for {UML} Components},
  crossref = {lncs3657},
  pages = {49--69 (21 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/05/fauml-fmco.pdf},
  abstract = {We present a fully abstract semantics for components. This
		  semantics is formalized in terms of a notion of trace for
		  components, providing a description of the component
		  externally observable behavior inspired by UML sequence
		  diagrams. Such a description abstracts from the actual
		  implementation given by UML state-machines. Our full
		  abstraction result is based on a may testing semantics
		  which involves a composition of components in terms of
		  cross-border dynamic class instantiation through component
		  interfaces.}
}
@article{deboer*:javatestdriver,
  author = {Frank S. de Boer and Marcello M. Bonsangue and Andreas
		  Gr{\"u}ner and Martin Steffen},
  title = {Java Test Driver Generation from Object-Oriented
		  Interaction Traces},
  note = {Special issue for the Proceedings of the 2nd International
		  Workshop on Harnessing Theories for Tool Support in
		  Software TTSS'08, ICTAC 2008 satellite workshop, 30.\
		  August 2008, Istambul, Turkey },
  journal = {Electronic Notes in Theoretical Computer Science},
  year = 2009,
  volume = 243,
  publisher = {Elsevier},
  pages = {33-47 (15 pages)},
  month = jul,
  url = {http://www.ifi.uio.no/~msteffen/download/08/javatestdriver.pdf},
  url2 = {http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4WW234B-4&_user=525211&_rdoc=1&_fmt=&_orig=search&_sort=d&_docanchor=&view=c&_acct=C000026378&_version=1&_urlVersion=0&_userid=525211&md5=e0ce5aec8d4c73be0b5c6a34c8381225},
  doi = {10.1016/j.entcs.2009.07.004},
  annote = {submitted 29.07.2008. An earlier version had been rejected
		  (under a different title) twice},
  abstract = {In the context of test-driven development for
		  object-oriented programs, mock objects are increasingly
		  used for unit testing. Several Java mock object frameworks
		  exist, which all have in common that mock objects,
		  realizing the test environment, are directly specified at
		  the Java program level. Though using directly the
		  programming language may facilitate acceptance by software
		  developers at first sight, the entailed syntax noise
		  sometimes distracts from the actual test specification,
		  speaking about interaction traces.
		  
		  We propose a Java-like test specification language, which
		  allows to describe the behavior of the test harness in
		  terms of the expected interaction \emph{traces} between the
		  program and its environment. The language is tailor-made
		  for Java, e.g., in that it reflects the nested calls and
		  return structure of thread-based interaction at the
		  interface. From a given trace specification, a testing
		  environment, i.e., a set of classes for mock objects, is
		  \emph{synthesized}.
		  
		  The design of the specification language is a careful
		  balance between two goals: using programming constructs in
		  Java-like notation helps the programmer to specify the
		  interaction without having to learn a completely new
		  specification notation. On the other hand,
		  \emph{additional} expressions in the specification language
		  allow to specify the desired trace behavior in a concise,
		  abstract way, hiding the intricacies of the required
		  synchronization code at the lower-level programming
		  language. }
}
@inproceedings{deboer*:petrinetbased,
  author = {Frank S. de Boer and Mario Bravetti and Immo Grabe and
		  Matias Lee and Martin Steffen and Gianluigi Zavattaro},
  title = {A {P}etri Net based Analysis of Deadlock for Active
		  Objects and Futures},
  year = 2013,
  crossref = {lncs7684},
  pages = {110--127},
  url = {http://www.ifi.uio.no/~msteffen/download/12/petrinetbased.pdf}
}
@inproceedings{deboer*:testdriver-nwpt,
  author = {Frank S. de Boer and Marcello M. Bonsangue and Andreas
		  Gr{\"u}ner and Martin Steffen},
  title = {Test Driver Generation from Object-Oriented Interaction
		  Traces (extended abstract)},
  crossref = {nwpt07},
  url = {http://www.ifi.uio.no/~msteffen/download/07/testing-short.pdf},
  pages = {52-54}
}
@inproceedings{deboer.grabe.steffen:static-nwpt,
  author = {Frank S. de Boer and Immo Grabe and Martin Steffen},
  title = {Static Deadlock Detection for Active Objects (Extended
		  Abstract)},
  booktitle = {ENTCS Proceedings of NWPT'09},
  url = {09/static-nwpt09.pdf},
  year = 2009,
  month = sep,
  annote = {submitted 10.09.2009}
}
@article{deboer.grabe.steffen:terminationdetection,
  author = {Frank de Boer and Immo Grabe and Martin Steffen},
  title = {Termination Detection for Active Objects},
  journal = {Journal of Logic and Algebraic Programming},
  year = 2012,
  volume = {81},
  number = {4},
  pages = {541-557},
  month = may,
  doi = {10.1016/j.jlap.2012.03.009},
  url = {http://dx.doi.org/10.1016/j.jlap.2012.03.009},
  annote = {Available online 16 March 2012}
}
@inproceedings{dovland*:encapsulating,
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  title = {Encapsulating Lazy Behavioral Subtyping},
  year = 2009,
  pages = {52--67 (16 pages)},
  booktitle = {Specification, Transformation, Navigation. Festschrift
		  dedicated to {Bernd Krieg-Br\"uckner} on the Occasion of
		  his 60th Birthday},
  annote = {An LNCS special proceedings is in preparation},
  publisher = {University Bremen},
  url = {http://www.ifi.uio.no/~msteffen/download/08/encapsulated.pdf}
}
@article{dovland*:incremental-multiple,
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  title = {Incremental Reasoning with Lazy Behavioral Subtyping for
		  Multiple Inheritance},
  year = 2011,
  journal = {Science of Computer Programming},
  publisher = {Elsevier},
  volume = 76,
  pages = {915-941},
  annote = {Science of Computing. resubmitted spring 2010, submitted:
		  22.06.09},
  url = {http://www.ifi.uio.no/~msteffen/download/10/incremental-multiple.pdf},
  doi = {http://dx.doi.org/10.1016/j.scico.2010.09.006}
}
@inproceedings{dovland*:lazy,
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  title = {Lazy Behavioral Subtyping},
  crossref = {lncs5014},
  pages = {52--67 (16 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/08/lazy.pdf}
}
@article{dovland*:lazy-jlap,
  title = {Lazy Behavioral Subtyping},
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  year = 2010,
  journal = {Journal of Logic and Algebraic Programming},
  publisher = {Elsevier Science Publishers},
  month = apr,
  volume = 79,
  number = 7,
  pages = {578-607},
  note = {30 pages. Article in Press, Preprint available at
		  {\texttt{ doi:10.1016/j.jlap.2010.07.008}}. Presented at
		  the 20th Nordic Workshop on Programming Theory, NWPT '08,
		  Tallinn. A shorter conference version appeared in the
		  Proceedings of the 15th International Symposium on Formal
		  Methods (FM'08), LNCS 5014},
  doi = {10.1016/j.jlap.2010.07.008},
  url = {http://www.ifi.uio.no/~msteffen/download/09/lazy-jlap.pdf},
  xxpages = {30 pages},
  annote = {resubmitted Sept. 2009, submitted 15.04.2009}
}
@inproceedings{dovland*:lazy-nwpt,
  title = {Lazy Behavioral Subtyping (Extended Abstract)},
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  year = 2008,
  month = nov,
  crossref = {nwpt08},
  note = {Presented at the 20th Nordic Workshop on Programming
		  Theory, NWPT '08, Tallinn},
  url = {http://www.ifi.uio.no/~msteffen/download/08/lazy-nwpt.pdf},
  annote = {submitted 03.10.2008}
}
@techreport{dovland*:lazy-rep,
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  title = {Lazy Behavioral Subtyping (revised version)},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2008,
  type = {Technical Report},
  number = 368,
  pages = {21 pages},
  note = {21 pages},
  xisbn = {82-7368-322-2},
  issn = {0806-3036},
  month = mar,
  url = {http://www.ifi.uio.no/~msteffen/download/08/lazy-rep.pdf}
}
@techreport{dovland*:lazy-single-interface-rep,
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  title = {Lazy Behavioral Subtyping: Single Inheritance and
		  Interfaces},
  institution = {Department of Informatics},
  month = may,
  year = 2009,
  isbn = {82-7368-343-5},
  type = {Research Report},
  number = 384,
  pages = {38 pages},
  address = {University of Oslo},
  xxxurl = {http://www.ifi.uio.no/~msteffen/download/09/lazy-single-inheritance.pdf},
  note = {38 pages. Submitted for journal publication. Available at
		  \url{http://einarj.at.ifi.uio.no/rr384.pdf}.}
}
@inproceedings{dovland*:multiple,
  title = {Incremental Reasoning for Multiple Inheritance},
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  crossref = {lncs5423},
  annote = {submitted 22.09.2008},
  pages = {215-230},
  url = {http://www.ifi.uio.no/~msteffen/download/09/multiple.pdf}
}
@techreport{dovland*:multiple-rep,
  title = {Incremental Reasoning for Multiple Inheritance},
  author = {Johan Dovland and Einar Broch Johnsen and Olaf Owe and
		  Martin Steffen},
  institution = {Department of Informatics},
  month = apr,
  year = 2008,
  type = {Research Report},
  number = 373,
  pages = {21 pages},
  note = {21 pages},
  isbn = {82-7368-333-8},
  address = {University of Oslo},
  url = {http://www.ifi.uio.no/~msteffen/download/08/multiple-rep.pdf}
}
@techreport{egner.nestmann.steffen:confluence,
  author = {Michael Egner and Uwe Nestmann and Martin Steffen},
  title = {{Confluent Processes for Transformation Correctness
		  (preliminary version)}},
  institution = {Informatik VII, Universit{\"a}t Erlangen-N{\"u}rnberg},
  year = 1995,
  type = {Interner Bericht},
  number = {IMMD7-1/95},
  month = jan,
  abstract = {Program transformations are central for the correct
		  development of parallel object-based programs in the
		  language $\pi o\beta\lambda$. A $\pi$-calculus translation
		  provides a formal semantics for the $\pi
		  o\beta\lambda$-language. In order to prove the correctness
		  of program transformations for the example program of a
		  symbol table, a theory of confluent mobile processes is
		  established.}
}
@inproceedings{fava*:oswmmwb-abstract-ifm,
  author = {Daniel Fava and Martin Steffen and Volker Stolz and Stian
		  Valle},
  title = {An Operational Semantics for a Weak Memory Model with
		  Buffered Writes, Message Passing, and Goroutines},
  booktitle = {Informal proceedings of the PhD Symposium at iFM'17
		  (integrated Formal Methods)},
  year = 2017,
  note = {Submitted for publication},
  url = {http://www.ifi.uio.no/~msteffen/download/17/oswmmwb-abstract-ifm.pdf}
}
@techreport{fava*:oswmmwb-rep,
  author = {Daniel Fava and Martin Steffen and Volker Stolz and Stian
		  Valle},
  title = {An Operational Semantics for a Weak Memory Model with
		  Buffered Writes, Message Passing, and Goroutines},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2017,
  number = 466,
  month = apr
}
@inproceedings{fecher.steffen:characteristic,
  author = {Harald Fecher and Martin Steffen},
  title = {Characteristic $\mu$-Calculus Formulas for Underspecified
		  Transition Systems},
  note = {Proceedings of the 11th International Workshop on
		  Expressiveness in Concurrency (Express 04), 30 August,
		  2004, London, Great Britain. 13 pages},
  journal = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  volume = 128,
  number = 2,
  year = 2005,
  month = apr,
  abstract = {Underspecification, which is essential for specification
		  formalisms, is usually expressed by equivalences,
		  simulations, or logic approaches.
		  
		  We introduce underspecified transition systems (UTSs) as
		  general model general model for underspecification, where,
		  e.g., transitions point to sets of states. We argue for the
		  generality of the UTSs by showing that the class of all
		  UTSs is strictly more expressive than the standard
		  equivalences and simulation approaches, in the sense that
		  more sets of transition systems can be expressed.
		  Additionally, a characteristic formula in terms of the
		  $\mu$-calculus is presented for every finite state UTS.
		  Furthermore, we show that UTSs can finitely describe sets
		  of transition systems, whenever they can be described
		  finitely by the other standard approaches except for
		  trace-set extension or $\mu$-calculus descriptions.},
  keywords = {underspecification, transition systems, bisimulation,
		  simulation, $\mu$-calculus},
  date = {2.8.2004},
  url = {http://www.ifi.uio.no/~msteffen/download/05/characteristic.pdf},
  officialurl = {http://dx.doi.org/10.1016/j.entcs.2004.11.031}
}
@inproceedings{gkolfi*:translatingtocpn,
  author = {Anastasia Gkolfi and Crystal Chang Din and Einar Broch
		  Johnsen and Martin Steffen and Ingrid Chieh Yu},
  title = {Translating Active Objects into Colored {P}etri Nets for
		  Communication Analysis},
  booktitle = {Accepted for publication in the LNCS post-proceedings of
		  ``Fundamentals of Software Engineering'', FSEN'2017},
  year = 2017
}
@inproceedings{grabe*:credomethodology,
  author = {Immo Grabe and Mohammad Mahdi Jaghoori and Bernhard
		  Aichernig and Tobias Blechmann and Frank de Boer and
		  Andreas Griesmayer and Einar Broch Johnsen and Joachim
		  Klein and Sascha K{\"u}ppelholz and Marcel Kyas and
		  Wolfgang Leister and Rudolf Schlatte and Andries Stam and
		  Martin Steffen and Simon Tschirner and Lian Xuedong and
		  Wang Yi},
  title = {Credo Methodology. {M}odeling and Analyzing a Peer-to-Peer
		  System in {C}redo},
  booktitle = {Special Issue for the proceedings of the 3rd International
		  Workshop on Harnessing Theories for Tool Support in
		  Software, 2009, Malaysia},
  editor = {Volker Stolz and Einar Broch Johnsen},
  year = 2010,
  note = {ENTCS Volume 266. 15 pages},
  publisher = {Elsevier Science Publishers}
}
@inproceedings{grabe*:credomethodology-extended,
  author = {Immo Grabe and Mohammad Mahdi Jaghoori and Bernhard
		  Aichernig and Tobias Blechmann and Frank de Boer and
		  Andreas Griesmayer and Einar Broch Johnsen and Joachim
		  Klein and Sascha K{\"u}ppelholz and Marcel Kyas and
		  Wolfgang Leister and Rudolf Schlatte and Andries Stam and
		  Martin Steffen and Simon Tschirner and Lian Xuedong and
		  Wang Yi},
  title = {Credo Methodology (Extended Version)},
  crossref = {lncs6286},
  pages = {41-69},
  note = {29 pages},
  doi = {10.1007/978-3-642-17071-3}
}
@inproceedings{grabe*:executable,
  author = {Immo Grabe and Marcel Kyas and Martin Steffen and Arild
		  B.\ Torjusen},
  title = {Executable Interface Specifications for Testing
		  Asynchronous {C}reol Components},
  crossref = {lncs5961},
  url = {http://www.ifi.uio.no/~msteffen/download//09/executable.pdf},
  year = {2010},
  pages = {324--339 (15 pages)}
}
@techreport{grabe*:executable-rep,
  author = {Immo Grabe and Martin Steffen and Arild Braathen Torjusen},
  title = {Executable Interface Specifications for Testing
		  Asynchronous {C}reol Components},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2008,
  month = jul,
  type = {Technical Report},
  number = 375,
  pages = {26 pages},
  isbn = {82-7368-335-4},
  url = {http://www.ifi.uio.no/~msteffen/download//08/executable-rep.pdf},
  xissn = {0806-3036},
  annote = {14.July 2008, revised May 2010},
  note = {26 pages}
}
@inproceedings{hansen.schneider.steffen:reachabilityanalysis,
  author = {Hallstein A. Hansen and Gerardo Schneider and Martin
		  Steffen},
  title = {Reachability Analysis of Planar Autonomous Systems},
  crossref = {lncs7141},
  pages = {206--220},
  annote = {Submitted: 10.02.2010}
}
@article{hansen.schneider.steffen:reachabilitycomplex,
  author = {Hallstein A. Hansen and Gerardo Schneider and Martin
		  Steffen},
  title = {Reachability Analysis of Complex Planar Hybrid Systems},
  journal = {Science of Computer Programming},
  year = 2013,
  month = dec,
  volume = 78,
  number = 12,
  pages = {2511-2536},
  note = {The work has been published as University of Oslo, Dept.\
		   of Computer Science Technical report 412, November 2011.
		  It is also an extended version of a paper published in the
		  LNCS proceedigs of FSEN 2011},
  annote = {Submitted 14. 11. 2011, see also {\tt
		  11/reachabilitycomplex.pdf}},
  doi = {http://dx.doi.org/10.1016/j.scico.2013.02.007}
}
@techreport{hansen.schneider.steffen:reachabilitycomplex-rep,
  author = {Hallstein A. Hansen and Gerardo Schneider and Martin
		  Steffen},
  title = {Reachability Analysis of Complex Planar Autonomous
		  Systems},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2011,
  number = 412,
  type = {Technical report},
  isbn = {82-7368-374-5},
  issn = {0806-3036},
  month = nov,
  url = {http://www.duo.uio.no/sok/work.html?WORKID=142076},
  pages = {44 pages}
}
@article{hofmann.naraschewski.steffen.stroup:inheritance,
  author = {Martin Hofmann and Wolfgang Naraschewski and Martin
		  Steffen and Terry Stroup},
  title = {Inheritance of Proofs},
  journal = {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},
  publisher = {John Wiley \& Sons Inc.},
  year = 1998,
  month = jan,
  pages = {51--69 (19 pages)},
  volume = 4,
  number = 1,
  url = {http://www.ifi.uio.no/~msteffen/download/98/inheritance.ps},
  abstract = {The Curry-Howard isomorphism, a fundamental property
		  shared by many type theories, establishes a direct
		  correspondence between programs and proofs. This suggests
		  that the same structuring principles that ease programming
		  should be useful for proving as well. To exploit
		  object-oriented structuring mechanisms for verification, we
		  extend the object-model of Pierce and Turner, based on the
		  higher-order typed $\lambda$-calculus F-omega-sub, with a
		  logical component.
		  
		  By enriching the (functional) signature of objects with a
		  specification, methods and their correctness proofs are
		  packed together in objects. The uniform treatment of
		  methods and proofs gives rise in a natural way to
		  object-oriented proving principles --- including
		  inheritance of proofs, late binding of proofs, and
		  encapsulation of proofs --- as analogues to object-oriented
		  programming principles. We have used Lego, a type-theoretic
		  proof checker, to explore the feasibility of this
		  approach.},
  note = {An extended version appeared as Interner Bericht,
		  Universit{\"a}t Erlangen-N{\"u}rnberg, IMMDVII-5/96}
}
@inproceedings{hofmann.naraschewski.steffen.stroup:inheritance-fool,
  author = {Martin Hofmann and Wolfgang Naraschewski and Martin
		  Steffen and Terry Stroup},
  title = {Inheritance of Proofs},
  booktitle = {Electronic proceedings of the Third Workshop on
		  Foundations of Object-Oriented Languages (FOOL 3)},
  month = jul,
  year = 1996,
  note = {An extended version appeared as Interner Bericht,
		  Universit{\"a}t Erlangen-N{\"u}rnberg, IMMDVII-5/96, which
		  was published in the special issue of Theory and Practice
		  of Object-Oriented Systems (TAPOS), January 1998}
}
@techreport{hofmann.naraschewski.steffen.stroup:inheritance-rep,
  author = {Martin Hofmann and Wolfgang Naraschewski and Martin
		  Steffen and Terry Stroup},
  title = {Inheritance of Proofs},
  type = {Interner Bericht},
  institution = {Universit{\"a}t Erlangen-N{\"u}rnberg, Informatik,
		  IMMDVII},
  year = 1996,
  number = {5/96},
  month = {June},
  note = {presented at the Third FOOL Workshop, 96, also as
		  contribution in a special issue of Theory and Practice of
		  Object-Oriented Systems (TAPOS), January 1998},
  url = {\texttt{ftp://ftp.in\-for\-matik.uni-er\-langen.de/local/inf7/vs/sfbc2/}{\tt fool96.ps}}
}
@inproceedings{ioustinova.sidorova.steffen:abstraction,
  booktitle = {Proceedings of the 9th Asia-Pacific Software Engineering
		  Conference (APSEC 2002, 4.--6.\ December 2002, Gold Coast,
		  Queensland, Australia},
  organization = {IEEE Computer Society},
  title = {Abstraction and Flow Analysis for Model Checking Open
		  Asynchronous Systems},
  author = {Natalia Ioustinova and Natalia Sidorova and Martin
		  Steffen},
  month = dec,
  year = 2002,
  pages = {227--235 (9 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/02/abstraction.pdf},
  date = {1.7.2002}
}
@inproceedings{ioustinova.sidorova.steffen:closing,
  author = {Natalia Ioustinova and Natalia Sidorova and Martin
		  Steffen},
  title = {Closing Open {SDL}-Systems for Model Checking with {DT
		  Spin}},
  booktitle = {Proceedings of Formal Methods Europe (FME'02)},
  crossref = {lncs2391},
  year = 2002,
  pages = {531--548 (18 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/02/closing.pdf},
  date = {8.5.2002}
}
@inproceedings{ioustinova.sidorova.steffen:fmco03,
  author = {Natalia Ioustinova and Natalia Sidorova and Martin
		  Steffen},
  title = {Synchronous Closing and Flow Analysis for Model Checking
		  Timed Systems},
  crossref = {lncs3188},
  year = 2004,
  url = {http://www.ifi.uio.no/~msteffen/download/04/syncclosing.pdf},
  pages = {292-313 (22 pages)},
  doi = {DOI: 10.1007/978-3-540-30101-1_14},
  date = {15.3.2004}
}
@inproceedings{johnsen*:coreabs,
  author = {Einar Broch Johnsen and Reiner H{\"a}hnle and Jan
		  Sch{\"a}fer and Rudi Schlatte and Martin Steffen},
  title = {{ABS}: {A} Core Language For Abstract Behavioral
		  Specification},
  crossref = {lncs6957},
  pages = {142-164},
  annote = {Submitted 28 March 2011}
}
@inproceedings{johnsen*:elastically,
  author = {Einar Broch Johnsen and Ka I Pun and Martin Steffen and
		  Silvia Lizeth and Martin Steffen and Ingrid Chieh Yu},
  title = {Meeting Deadlines, Elastically},
  booktitle = {From Action Systems to Distributed System: The Refinement
		  Approach},
  editor = {Luigia Petre and Emil Sekerinski},
  year = 2016,
  url = {http://www.ifi.uio.no/~msteffen/download/14/elastically.pdf},
  xpages = {21 pages},
  publisher = {CRC press},
  pages = {99-111},
  annoted = {Kaisa-proceedings}
}
@inproceedings{johnsen*:safelocking,
  author = {Einar Broch Johnsen and Thi {Mai Thuong Tran} and Olaf Owe
		  and Martin Steffen},
  title = {Safe Locking for Multi-Threaded {J}ava},
  crossref = {lncs7141},
  pages = {158--173}
}
@article{johnsen*:safelocking-exceptions,
  author = {Einar Broch Johnsen and Thi {Mai Thuong Tran} and Olaf Owe
		  and Martin Steffen},
  title = {Safe Locking for Multi-Threaded {J}ava with Exceptions},
  journal = {Journal of Logic and Algebraic Programming, special issue
		  of selected contributions to NWPT'10},
  year = 2012,
  month = mar,
  annote = {submitted 28.02.2011},
  note = {Available online 3.\ March 2012},
  doi = {http://dx.doi.org/10.1016/j.jlap.2011.11.002},
  url = {http://dx.doi.org/10.1016/j.jlap.2011.11.002}
}
@techreport{johnsen*:safelocking-rep,
  author = {Einar Broch Johnsen and Thi {Mai Thuong Tran} and Olaf Owe
		  and Martin Steffen},
  title = {Safe Locking for Multi-Threaded {J}ava},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2011,
  month = jan,
  type = {Technical Report (revised version)},
  number = 402,
  pages = {32 pages},
  isbn = {82-7368-364-8},
  issn = {0806-3036},
  note = {\url{www.ifi.uio.no/~msteffen/publications.html#techreports}}
}
@inproceedings{johnsen.steffen.stumpf:calculusvta-abstract-nwpt,
  author = {Einar Broch Johnsen and Martin Steffen and Johanna Beate
		  Stumpf},
  title = {A Calculus of Virtually Timed Ambients (extended
		  abstract)},
  year = 2016,
  month = oct,
  url = {http://www.ifi.uio.no/~msteffen/download/16/calculusvta-abstract-nwpt.pdf},
  crossref = {nwpt16}
}
@inproceedings{johnsen.steffen.stumpf:calculusvta-abstract-wadt,
  author = {Einar Broch Johnsen and Martin Steffen and Johanna Beate
		  Stumpf},
  title = {A Calculus of Virtually Timed Ambients (extended
		  abstract)},
  year = 2016,
  month = sep,
  booktitle = {Informal Proceedings of the 23rd International Workshop on
		  Algebraic Development Techniques (WADT 2016)},
  url = {http://www.ifi.uio.no/~msteffen/download/16/calculusvta-abstract-wadt.pdf}
}
@inproceedings{johnsen.steffen.stumpf:calculusvta-wadt,
  author = {Einar Broch Johnsen and Martin Steffen and Johanna Beate
		  Stumpf},
  title = {A Calculus of Virtually Timed Ambients},
  year = 2017,
  booktitle = {To appear in the Post-Proceedings of selected
		  contributions to the 23rd International Workshop on
		  Algebraic Development Techniques (WADT 2016)},
  url = {http://www.ifi.uio.no/~msteffen/download/17/calculusvta-wadt.pdf}
}
@article{johnsen.steffen.stumpf:vta,
  author = {Einar Broch Johnsen and Martin Steffen and Johanna Beate
		  Stumpf},
  title = {Virtually Timed Ambients: A Calculus of Nested
		  Virtualization},
  journal = {Journal of Logic and Algebraic Methods in Programming},
  year = 2017,
  note = {Submitted for Publication in the Journal of Logic and
		  Algebraic Methods in Programming (JLAMP). Special Issue on
		  Selected Contributions of NWPT'16}
}
@inproceedings{johnsen.steffen.stumpf:vtacoeff,
  author = {Einar Broch Johnsen and Martin Steffen and Johanna Beate
		  Stumpf},
  title = {A Type System with Assumptions, Commitments and Coeffects
		  for Virtually Timed Ambients},
  year = 2017,
  month = jun,
  booktitle = {Under Preparation}
}
@inproceedings{kyas.stam.steffen.torjusen:specificationdriven-nwpt,
  author = {Marcel Kyas and Andries Stam and Martin Steffen and Arild
		  Braathen Torjusen},
  title = {A Specification-Driven Interpreter for Testing
		  Asynchronous {C}reol Components (extended abstract)},
  note = {Presented at the 20th Nordic Workshop on Programming
		  Theory, NWPT'08, Tallinn},
  year = 2008,
  month = nov,
  url = {http://www.ifi.uio.no/~msteffen/download//08/specificationdriven-nwpt.pdf},
  crossref = {nwpt08},
  annote = {submitted 3. October 2008}
}
@techreport{abraham.gruener.steffen:threadclasses-rep,
  author = {Erika {\'A}brah{\'a}m and Andreas Gr{\"u}ner and Martin
		  Steffen},
  title = {An Open Structural Operational Semantics for an
		  Object-Oriented calculus with Thread Classes},
  institution = {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2005,
  month = may,
  url = {http://www.informatik.uni-kiel.de/reports/2005/0505.html},
  type = {Technical Report},
  number = 0505,
  abstract = {In this report we present a multithreaded class-calculus
		  featuring \emph{thread classes.}
		  
		  From an observational point of view, considering classes as
		  part of a component makes instantiation a possible
		  interaction between component and environment or observer.
		  For thread classes it means that a component may create
		  external activity, which influences what can be observed.
		  The fact that cross-border instantiation is possible
		  requires that the \emph{connectivity} of the objects needs
		  to be incorporated into the semantics. We extend our prior
		  work not only by adding thread classes, but also in that
		  thread names may be \emph{communicated,} which means that
		  the semantics needs explicitly account for the possible
		  acquaintance of objects with threads.
		  
		  This report formalizes a calculus featuring thread classes,
		  i.e., its syntax, type system, and operational semantics.
		  We furthermore discuss observational aspects of thread
		  classes.},
  keywords = {class-based object-oriented languages, open systems,
		  formal semantics, thread classes, heap abstraction.}
}
@inproceedings{li.qeriqi.steffen.yu:automatictranslation,
  author = {Jingyue Li and Altin Qeriqi and Martin Steffen Ingrid
		  Chieh Yu},
  title = {Automatic Translation of {FBD-PLC}-programs to {NuSMV} for
		  Model Checking Safety-Critical Control Systems},
  booktitle = {Proceedings of the Norsk Informatikkonferanse NIK'16},
  year = 2016
}
@inproceedings{luteberget*:rulebasedincremental,
  author = {Bj{\o}rnar Luteberget and Christian Johansen and Claus
		  Feyling and Martin Steffen},
  title = {Rule-Based Incremental Verification Tools Applied to
		  Railway Designs and Regulations},
  crossref = {lncs9995},
  year = 2016,
  month = nov,
  pages = {772--778},
  doi = {10.1007/978-3-319-48989-6_49}
}
@inproceedings{luteberget.johansen.steffen:rulebased,
  author = {Bj{\o}rnar Luteberget and Christian Johansen and Martin
		  Steffen},
  title = {Rule-based Consistency Checking of Railway Infrastructure
		  Designs},
  crossref = {lncs9681},
  pages = {491-507},
  note = {Best Paper Award for iFM 2016. See also the UiO IFI
		  research report Nr. 450 with the same title}
}
@techreport{luteberget.johansen.steffen:rulebased-rep,
  author = {Bj{\o}rnar Luteberget and Christian Johansen and Martin
		  Steffen},
  title = {Rule-based Consistency Checking of Railway Infrastructure
		  Designs},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2016,
  type = {Technical report},
  number = 450,
  isbn = {978-82-7368-415-8},
  month = jan,
  url = {http://www.ifi.uio.no/~msteffen/download/16/rulebasedconsistency-rep.pdf},
  note = {A shorter version has been submitted for inclusion in
		  conference proceedings}
}
@inproceedings{mai.owe.steffen:safetyping,
  author = {Thi {Mai Thuong Tran} and Olaf Owe and Martin Steffen},
  key = {Mai Thuong},
  title = {Safe Typing for Transactional vs.\ Lock-Based Concurrency
		  in Multi-Threaded {J}ava},
  year = 2010,
  booktitle = {Proceedings of the Second International Conference on
		  Knowledge and Systems Engineering, KSE 2010},
  publisher = {IEEE Computer Society},
  editor = {Son Bao Pham and Tuan-Hao Hoang and Bob McKay and Kaoru
		  Hirota},
  url = {http://www.coltech.vnu.edu.vn/kse2010/},
  month = oct,
  pages = {188 - 193},
  isbn = {ISBN 978-0-7695-4213-3},
  annote = {Re-submitted 23. 03. 2010 Submitted 30.03.2010}
}
@inproceedings{mai.steffen:design-observability,
  author = {Thi {Mai Thuong Tran} and Martin Steffen},
  title = {Design Issues in Concurrent Object-Oriented Languages and
		  Observability},
  year = 2011,
  month = jun,
  booktitle = {Proceedings of the Third International Conference on
		  Knowledge and Systems Engineering (KSE 2011), Hanoi
		  14th-17th Oct, 2011},
  pages = {135-142},
  publisher = {IEEE Computer Society CPS},
  annote = {Submitted 29.06.2011}
}
@inproceedings{mai.steffen:evolution-spec,
  author = {Thi {Mai Thuong Tran} and Martin Steffen},
  title = {Specification and Verification},
  booktitle = {Eternal Task Force 2: Time Awareness and Management.
		  {S}tate-of-the-Art Report},
  year = 2011,
  editior = {Michael Felderer and Phillip Kalb and Michael Hafner},
  month = jan
}
@inproceedings{mai.steffen:safecommits,
  author = {Thi {Mai Thuong Tran} and Steffen, Martin},
  key = {Mai Thuong},
  title = {Safe Commits for {T}ransactional {F}eatherweight {J}ava},
  pages = {290--304},
  crossref = {lncs6396},
  note = {An earlier and longer version has appeared as UiO, Dept.\
		  of Informatics Technical Report 392, Oct.\ 2009},
  annote = {Re-submitted 28.05.2010, Re-submitted 29.03.2010,
		  Submitted 12.02.2010}
}
@inproceedings{nestmann.steffen.stroup:asynchron,
  author = {Uwe Nestmann and Martin Steffen and Terry Stroup},
  title = {{Formale Semantik f{\"u}r asynchronen Methodenaufruf}},
  crossref = {giitg5},
  pages = {169--178 (10 pages)},
  note = {Available as Universit{\"a}t-N{\"u}rnberg Erlangen, IMMD7,
		  Interner Bericht TR-I7-95-11},
  abstract = {Das Methodenaufrufschema \emph{wait-by-necessity} zum
		  Verbergen expliziter Parallelit{\"a}t hinter asynchronen
		  Wertzuweisungen wird exemplarisch durch eine
		  \emph{Strukturelle Operationelle Semantik} (SOS)
		  formalisiert. Diese Spezifikation repr{\"a}sentiert ein
		  eindeutiges Referenzmodell und wurde dar{\"u}berhinaus
		  mittels einer semantisch korrekten {\"U}bersetzung in den
		  $\pi$-Kalk{\"u}l in eine prototypische Implementierung
		  {\"u}berf{\"u}hrt. Sie dienen neben der Validierung der
		  Intuition des Programmiersprach-Ingenieurs auch als Basis
		  f{\"u}r den Entwurf korrekter Compiler sowie zum Testen von
		  Beispielprogrammen. Das vorliegende Papier konzentriert
		  sich auf die Darstellung der SOS-Variante}
}
@techreport{nestmann.steffen.stroup:asynchron.ib,
  author = {Uwe Nestmann and Martin Steffen and Terry Stroup},
  title = {{Formale Semantik f{\"u}r asynchronen Methodenaufruf}},
  institution = {{Universit{\"a}t Erlangen--N{\"u}rnberg, IMMD VII}},
  year = 1995,
  type = {Interner Bericht},
  number = {TR-I7-95-11},
  month = may,
  pages = {11 pages}
}
@techreport{nestmann.steffen:kalkuelbasiert,
  author = {Uwe Nestmann and Martin Steffen},
  title = {Kalk{\"u}basierte {OO}-{S}prachen},
  institution = {Universit{\"a}t Erlangen-N{\"u}rnberg, Informatik,
		  IMMDVII},
  year = 1994,
  pages = {9 pages},
  type = {Technical Report},
  number = {IMMD7-02/94}
}
@inproceedings{owe.schneider.steffen:components,
  author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
  title = {Components, Objects, and Contracts},
  year = 2007,
  month = aug,
  booktitle = {Sixth International Workshop on Specification and
		  Verification of Component-Based Systems, Sept.\ 3--4, 2007,
		  Cavtat, Croatia},
  pages = {95--98},
  annote = {23.07.2007},
  url = {http://www.ifi.uio.no/~msteffen/download/07/components-abstract.pdf}
}
@techreport{owe.schneider.steffen:components-rep,
  author = {Olaf Owe and Gerardo Schneider and Martin Steffen},
  title = {Components, Objects, and Contracts},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2007,
  type = {Research Report},
  number = 363,
  pages = {18 pages},
  month = aug,
  url = {http://www.ifi.uio.no/~msteffen/download/07/components-rep.pdf},
  note = {18 pages. A short version appeared in the proceedings of
		  SAVCBS'07}
}
@inproceedings{owe.steffen.torjusen:modeltesting,
  author = {Olaf Owe and Martin Steffen and Arild Torjusen},
  title = {Model Testing Asynchronously Communicating Objects using
		  Modulo {AC} Rewriting},
  booktitle = {Proceedings of the 6th Workshop on Model-Based Testing
		  MBT'10 (ETAPS Satellite Workshop)},
  year = 2010,
  month = mar,
  pages = {68--84},
  note = {Electronic Notes in Theoretical Computer Science ENTCS,
		  Volume 264, Issue 3.},
  publisher = {Elsevier Science Publishers},
  annote = {Resubmitted MBT 18.12.2009, resubmitted 20.07.2009}
}
@inproceedings{owe.steffen.torjusen:modeltesting-nwpt,
  author = {Olaf Owe and Martin Steffen and Arild Torjusen},
  title = {Model Testing Asynchronously Communicating Objects using
		  Modulo {AC} Rewriting (Extended Abstract)},
  booktitle = {Proceedings of NWPT'09},
  year = 2009,
  month = sep,
  annote = {submitted 10.09.2009},
  url = {09/modeltesting-nwpt09.pdf}
}
@article{pierce.steffen:hos,
  author = {Benjamin C. Pierce and Martin Steffen},
  title = {Higher-Order Subtyping},
  journal = {Theoretical Computer Science},
  year = 1997,
  volume = 176,
  number = {1,2},
  pages = {235-282 (48 pages)},
  note = {A shorter version appeared in the Proceedings IFIP Working
		  Conference on Programming Concepts, Methods and Calculi
		  (p.~511--530), 1994. Also as LFCS technical report
		  ECS-LFCS-94-280 and as Interner Bericht IMMD7-01/94,
		  Universit{\"a}t Erlangen}
}
@inproceedings{pun*:goastray,
  author = {Ka I Pun and Martin Steffen and Volker Stolz and
		  Anna-Katharina Wickert and Eric Bodden and Michael
		  Eichberg},
  title = {Don't let data {Go} astray: {A} Context-Sensitive Taint
		  Analysis for Concurrent Programs in {Go} (extended
		  abstract)},
  crossref = {nwpt16}
}
@inproceedings{pun.steffen.stolz:behaviorinference,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Behaviour Inference for Deadlock Checking},
  booktitle = {Proceeding of the 8th International Symposium on
		  Theoretical Aspects of Software Engineering (TASE'14)},
  pages = {106--113},
  year = 2014,
  publisher = {IEEE},
  url = {http://www.ifi.uio.no/~msteffen/download/14/behaviorinference.pdf}
}
@techreport{pun.steffen.stolz:behaviorinference-firstorder-rep,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Behaviour Inference for Deadlock Checking},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2012,
  type = {Technical report},
  number = {416},
  url = {http://www.ifi.uio.no/~msteffen/download/12/behaviorinference.pdf},
  isbn = {82-7368-379-6},
  xissn = {?},
  month = jul
}
@article{pun.steffen.stolz:deadlock,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Deadlock Checking by a Behavioral Effect System for Lock
		  Handling},
  journal = {Journal of Logic and Algebraic Programming},
  year = 2012,
  volume = 81,
  number = 3,
  pages = {331--354},
  xurl = {http://dx.doi.org/10.1016/j.jlap.2011.11.001},
  month = mar,
  note = {A preliminary version was published as University of Oslo,
		  Dept.\ of Computer Science Technical Report 404, March
		  2011},
  annote = {Available online 6.\ March 2012. Revised version Sept
		  2011. Submitted 21 March 2011}
}
@techreport{pun.steffen.stolz:deadlock-rep,
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Deadlock Checking by a Behavioral Effect System for Lock
		  Handling},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2011,
  number = 404,
  type = {Technical report},
  isbn = {82-7368-366-4},
  issn = {0806-3036},
  month = mar
}
@article{pun.steffen.stolz:deadlockchecking,
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Deadlock Checking by Data Race Detection},
  year = 2014,
  journal = {Journal of Logic and Algebraic Methods in Programming},
  month = mar,
  issn = {2352-2208},
  note = {Available online 13 August 2014,
		  http://dx.doi.org/10.1016/j.jlamp.2014.07.003. A
		  preliminary version was published as University of Oslo,
		  Dept.\ of Computer Science Technical Report 421, October
		  2012, and a shorter version in the proceedings of FSEN'13},
  annote = {accepted 24. July 2014},
  url = {http://www.ifi.uio.no/~msteffen/download/13/deadlockchecking-journal.pdf}
}
@inproceedings{pun.steffen.stolz:deadlockchecking-fsen,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Deadlock Checking by Data Race Detection},
  url = {http://www.ifi.uio.no/~msteffen/download/12/deadlockchecking.pdf},
  booktitle = {Proceedings of the 5th IPM International Conference on
		  Fundamentals of Software Engineering (FSEN'13)},
  crossref = {lncs8161},
  pages = {34--50},
  year = 2013
}
@inproceedings{pun.steffen.stolz:deadlockchecking-nwpt,
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Deadlock Checking by Data Race Detection},
  crossref = {nwpt12},
  url = {http://www.ifi.uio.no/~msteffen/download/12/deadlockchecking-nwpt.pdf}
}
@techreport{pun.steffen.stolz:deadlockchecking-rep,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Deadlock Checking by Data Race Detection},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2012,
  type = {Technical report},
  number = 421,
  url = {http://www.ifi.uio.no/~msteffen/download/12/dlraces-rep.pdf},
  isbn = {82-7368-385-0},
  xissn = {0806-3036},
  month = oct
}
@inproceedings{pun.steffen.stolz:effectpolymorphic,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Effect-Polymorphic Behaviour Inference for Deadlock
		  Checking},
  crossref = {lncs8702},
  pages = {50--64},
  note = {A longer version is available (under the title
		  ``Lock-Polymorphic Behaviour Inference for Deadlock
		  Checking'') as UiO, Dept.\ of Informatics Technical Report
		  436, Sep.\ 2013},
  annote = {Submitted: 13.12.2013 (+19. Sep. 2013)}
}
@article{pun.steffen.stolz:effectpolymorphic-jlap,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Effect-Polymorphic Behaviour Inference for Deadlock
		  Checking},
  volume = 85,
  number = 6,
  year = 2016,
  journal = {Journal of Logic and Algebraic Methods in Programming},
  note = {A longer version is available (under the title
		  ``Lock-Polymorphic Behaviour Inference for Deadlock
		  Checking'') as UiO, Dept.\ of Informatics Technical Report
		  436, Sep.\ 2013},
  doi = {http://dx.doi.org/10.1016/j.jlamp.2016.05.003},
  url = {http://www.ifi.uio.no/~msteffen/download/16/effectpolymorphic.pdf},
  month = oct,
  annote = {8. 3. 2013}
}
@inproceedings{pun.steffen.stolz:lockpolymorphic-nwpt,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Lock-Polymorphic Behaviour Inference for Deadlock Checking
		  (extended abstract)},
  booktitle = {Proceedings of NWPT'13},
  year = 2013,
  month = nov,
  url = {http://www.ifi.uio.no/~msteffen/download/13/lockpolymorphic-nwpt.pdf},
  note = {Available electronically at
		  \url{http://www.ifi.uio.no/~msteffen/download/13/lockpolymorphic-nwpt.pdf}.
		  A longer version is available as UiO, Dept.\ of Informatics
		  Technical Report 436, Sep.\ 2013},
  annote = {Submitted Oct 2013}
}
@techreport{pun.steffen.stolz:lockpolymorphic-rep,
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  title = {Lock-Polymorphic Behaviour Inference for Deadlock
		  Checking},
  institution = {University of Oslo, Dept.\ of Informatics},
  number = {436},
  year = 2013,
  type = {Technical report},
  url = {http://www.ifi.uio.no/~msteffen/download/13/lockpolymorphic-rep.pdf},
  note = {Available electronically at
		  \url{http://www.ifi.uio.no/~msteffen/download/13/lockpolymorphic-rep.pdf}.
		  Submitted to journal publication.},
  isbn = {82-7368-398-2},
  issn = {0806-3036},
  month = sep
}
@inproceedings{pun.steffen.stolz:polymorphic-nwpt,
  author = {Ka I Pun and Martin Steffen and Volker Stolz},
  xxxauthor = {Ka \onelettername{I} Pun and Martin Steffen and Volker
		  Stolz},
  title = {Polymorphic behavioural lock effects for deadlock checking
		  (extended abstract)},
  crossref = {nwpt11},
  url = {http://www.ifi.uio.no/~msteffen/download/11/dlpoly-nwpt.pdf},
  pages = {48--50},
  annote = {Submitted 25 Sep 2011}
}
@inproceedings{pun.steffen:deadlocks-nwpt,
  author = {Ka I Pun and Martin Steffen},
  title = {Deadlock checking by behavior inference for lock handling
		  (extended abstract)},
  booktitle = {Proceedings of the 22nd Nordic Workshop on Programming
		  Theory (NWPT'10)},
  year = 2010,
  month = nov,
  series = {TUCS General Publication},
  volume = 57,
  pages = {8--9},
  publisher = {Turku Centre for Comuter Science},
  annote = {submitted 27.09.2010}
}
@inproceedings{rosenberg.steffen.stolz:leveragingdtrace,
  author = {Carl Martin Rosenberg and Martin Steffen and Volker Stolz},
  title = {Leveraging {DTrace} for Runtime Verification},
  crossref = {lncs10012},
  year = 2016,
  pages = {318--332},
  url = {http://www.ifi.uio.no/~msteffen/download/16/leveragingdtrace.pdf}
}
@misc{mikk.steffen:javaprojekt,
  author = {Erich Mikk and Martin Steffen},
  title = {Javaprojekt: ``{P}rogramming Environment for
		  {S}tatecharts''},
  howpublished = {Included in the proceedings of the ``7.\
		   Deutschen Anwenderforum f{\"u}r Statemate MAGNUM'',
		  26.--27.\ April, 1999},
  year = 1999
}
@inproceedings{sidorova.steffen:atm-verification,
  author = {Natalia Sidorova and Martin Steffen},
  title = {Verification of a Wireless {ATM} Medium-Access Protocol},
  booktitle = {Proceedings of the 7th Asia-Pacific Software Engineering
		  Conference (APSEC 2000), 5.--8.\ December 2000, Singapore},
  organization = {IEEE Computer Society},
  pages = {84--91 (8 pages)},
  year = 2000,
  note = {A preliminary and longer version appeared as
		  Universit{\"a}t Kiel technical report TR-ST-00-3},
  abstract = {We report on a model checking case study of an industrial
		  medium access protocol for wireless ATM. Since the protocol
		  is too large to be verified by any of the existing checkers
		  as a whole, the verification exploits the layered and
		  modular structure of the protocol's SDL specification and
		  proceeds in a bottom-up, compositional way. The
		  compositional arguments are used in combination with
		  abstraction techniques to further reduce the state space of
		  the system. The verification is primarily aimed at
		  debugging the system. After correcting the specification
		  step by step and validating various untimed and
		  time-dependent properties, a model of the whole control
		  component of the medium-access protocol is built and
		  verified. The significance of the case study is in
		  demonstrating that verification tools can handle complex
		  properties of a model as large as shown.},
  keywords = {asynchronous transfer mode; access protocols; formal
		  verification; formal specification; wireless LAN; wireless
		  ATM; medium-access protocol verification; model checking;
		  modular structure; SDL specification; abstraction
		  techniques; state space reduction; system debugging;
		  untimed properties; time-dependent properties},
  xxxurl = {http://www.ifi.uio.no/~msteffen/download/00/}
}
@techreport{sidorova.steffen:atm-verification-rep,
  author = {Natalia Sidorova and Martin Steffen},
  title = {Verification of a Wireless {ATM} Medium-Access Protocol},
  institution = {Lehrstuhl f{{\"u}r} Software-Technologie, Institut f{\"u}r
		  Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2000,
  type = {Technical Report},
  number = {TR-ST-00-3},
  month = may,
  pages = {22 pages},
  note = {22 pages},
  url = {http://www.ifi.uio.no/~msteffen/download/00/atmveri-report.ps},
  abstract = {In this paper we report on a model-checking case study of
		  an industrial medium-access protocol for wireless ATM.
		  Since the protocol is too large to be verified by any of
		  existing checkers as a whole, the verification exploits the
		  layered and modular structure of the protocol's SDL
		  specification and proceeds in a bottom-up, compositional
		  way. The compositional arguments are used in combination
		  with abstraction techniques to further reduce the state
		  space of the system. The verification is primarily aimed at
		  debugging the system. After correcting the specification
		  step by step and validating various untimed and
		  time-dependent properties, a model of the whole control
		  component of the medium-access protocol is built and
		  verified. The significance of the case study is in
		  demonstrating that verification tools can handle complex
		  properties of a model as large as shown.}
}
@inproceedings{sidorova.steffen:embedding,
  author = {Natalia Sidorova and Martin Steffen },
  title = {Embedding Chaos},
  year = 2001,
  pages = {319--334 (15 pages)},
  crossref = {lncs2126},
  url = {http://www.ifi.uio.no/~msteffen/download/01/embedding.pdf}
}
@techreport{sidorova.steffen:mascaracontrol,
  author = {Natalia Sidorova and Martin Steffen},
  title = {Verifying {M}ascara {C}ontrol},
  institution = {Lehrstuhl f{{\"u}r} Software-Technologie, Institut f{\"u}r
		  Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  year = 2000,
  pages = {40 pages},
  note = {40 pages},
  type = {Technical Report},
  number = {TR-ST-00-1},
  month = may,
  url = {http://www.informatik.uni-kiel.de/inf/deRoever/techreports/00/tr-st-00-1.ps.gz},
  abstract = {This document reports on a series of verification
		  experiments on the control-part of Mascara, a medium-access
		  protocol for wireless ATM-networks.}
}
@inproceedings{sidorova.steffen:synchronous,
  author = {Natalia Sidorova and Martin Steffen},
  title = {Synchronous Closing of Timed {SDL} Systems for Model
		  Checking},
  crossref = {lncs2294},
  pages = {79--93 (15 pages)},
  url = {http://www.ifi.uio.no/~msteffen/download/12/petrinetbased.pdf}
}
@inproceedings{sidorova.steffen:verifyinglargesdl,
  author = {Natalia Sidorova and Martin Steffen},
  title = {Verifying Large {SDL}-Specifications using Model Checking},
  crossref = {lncs2078},
  year = 2001,
  month = feb,
  pages = {403--416 (14 pages)}
}
@mastersthesis{siegel.steffen:da,
  author = {Michael Siegel and Martin Steffen},
  title = {Vollst{\"a}ndigkeit eines {B}eweissystems f{\"u}r
		  {H}ennessy-{M}ilner-{L}ogik mit {R}ekursion},
  type = {Diplomarbeit},
  year = 1992,
  note = {71 pages},
  school = {Friedrich-Alexander-Universit{\"a}t,
		  Erlangen-N{\"u}rnberg},
  url = {http://www.ifi.uio.no/~msteffen/download/arbeiten/da.ps}
}
@mastersthesis{siegel.steffen:sa,
  author = {Michael Siegel and Martin Steffen},
  title = {{E}in {B}eweissystem f{\"u}r {H}ennessy-{M}ilner-{L}ogik
		  mit {R}ekursion},
  school = {Friedrich-Alexander-Universit{\"a}t,
		  Erlangen-N{\"u}rnberg},
  type = {Studienarbeit},
  year = 1991,
  note = {61 pages},
  url = {http://www.ifi.uio.no/~msteffen/download/arbeiten/sa.ps},
  abstract = {Als ausdrucksstarke temporale Logik wird seit einigen
		  Jahren verst{\"a}rkt Hennessy-Milner-Logik mit Rekursion
		  zur Spezifikation verteilter Systeme untersucht. Eine
		  wichtige Frage in diesem Zusammenhang stellt die formale
		  Verifizierbarkeit dar, das hei{\ss}t, die Frage nach einem
		  Beweissystem.
		  
		  Wir stellen in unserer Arbeit ein Gentzen-System f{\"u}r
		  Hennessy-Milner-Logik mit Rekursion vor. Damit l{\"a}{\ss}t
		  sich zielgerichtet die semantische Implikation zwischen
		  Formeln der Logik beweisen. Besondere Schwierigkeiten
		  bereiten dabei beliebig geschachtelte Fixpunkte, welche
		  gerade die Ausdrucksst{\"a}rke dieser Logik ausmachen.
		  Aufbauend auf einer Klasse von Algorithmen, die
		  {\"u}berpr{\"u}fen, ob ein Proze{\ss}, modelliert durch ein
		  Transitionssystem, die Spezifikation erf{\"u}llt
		  (sogenannte {\em Model-Checker}), haben wir die dort
		  verwendeten Techniken zur Behandlung der Fixpunkte
		  erweitert, um unser Gentzen-System zu konstruieren. In
		  analoger Weise wie im Model-Checker von Stirling und Walker
		  benutzten wir Konstanten zur eindeutigen Kennzeichnung von
		  Fixpunktformeln.
		  
		  W{\"a}hrend Model-Checking im wesentlichen ein
		  Ein-Schritt-Verfahren der Verifikation darstellt, kann man
		  das Gentzen-System f{\"u}r die semantische Implikation
		  f{\"u}r die schrittweise Verfeinerung und Verifikation
		  benutzen.}
}
@inproceedings{stahl.baukus.lakhnech.steffen:divide,
  author = {Karsten Stahl and Kai Baukus and Yassine Lakhnech and
		  Martin Steffen},
  title = {Divide, Abstract, and Model-Check},
  crossref = {lncs1680},
  pages = {57--76 (20 pages)}
}
@techreport{steffen.pierce:hos-rep,
  author = {Martin Steffen and Benjamin C. Pierce},
  title = {Higher-Order Subtyping},
  institution = {Informatik VII, Universit{\"a}t Erlangen-N{\"u}rnberg},
  year = 1994,
  type = {Interner Bericht},
  number = {IMMD7-01/94},
  month = jan,
  date = {4.2.1994},
  url = {http://www.ifi.uio.no/~msteffen/download/94/fomega-rep.ps},
  note = {Also as Edinburgh LFCS technical report ECS-LFCS-94-280}
}
@inproceedings{steffen.pierce:procomet94,
  author = {Martin Steffen and Benjamin C. Pierce},
  title = {Higher-Order Subtyping},
  pages = {511--530 (20 pages)},
  crossref = {procomet94},
  year = 1994,
  note = {Full version in {\em Theoretical Computer Science},
		  vol.~176, no.~1--2, pp.\  235--282, 1997}
}
@inproceedings{steffen.siegel:validity,
  author = {Martin Steffen and Michael Siegel},
  title = {Validity in the Propositional $\mu$-Calculus},
  booktitle = {Workshop: Logics for Distributed Systems, GMD-Studien Nr.
		  214},
  editor = {U. Goltz and W. Reisig},
  year = 1992,
  publisher = {{GMD, Gesellschaft f{\"u}r Mathematik und
		  Datenverarbeitung}}
}
@misc{steffen.thuong:stockquoter,
  author = {Martin Steffen and Thi Mai Thuong Tran},
  title = {The Stock Quoter Case Study},
  howpublished = {Internal Document},
  month = mar,
  year = 2009
}
@inproceedings{steffen.tran:safecommits-nwpt,
  author = {Martin Steffen and Thi Mai Thuong Tran},
  title = {Safe Commits for {T}ransactional {F}eatherweight {J}ava
		  (extended abstract)},
  booktitle = {Proceedings of the Nordic Workshop on Programming Theory,
		  NWPT'09},
  url = {09/safecommits-nwpt09.pdf},
  year = 2009,
  month = oct,
  annote = {submitted 10.09.2009}
}
@techreport{steffen.tran:safecommits-rep,
  author = {Martin Steffen and Thi Mai Thuong Tran},
  title = {Safe Commits for {T}ransactional {F}eatherweight {J}ava},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2009,
  type = {Technical Report},
  number = 392,
  pages = {23 pages},
  isbn = {82-7368-353-2},
  issn = {0806-3036},
  note = {23 pages},
  month = oct
}
@phdthesis{steffen:habil,
  author = {Martin Steffen},
  title = {Object-Connectivity and Observability for Class-Based,
		  Object-Oriented Languages},
  type = {Habilitation thesis},
  year = 2006,
  month = jul,
  note = {281 pages},
  school = {Technische Faktult{\"a}t der
		  Christian-Albrechts-Universit{\"a}t zu Kiel},
  annote = {Submitted 4th.\ July, accepted 7.\ February 2007}
}
@phdthesis{steffen:phd,
  author = {Martin Steffen},
  title = {Polarized Higher-Order Subtyping},
  publisher = {Dissertation, Universit{\"a}t Erlangen-N{\"u}rnberg},
  year = 1998,
  note = {260 pages},
  school = {Technische Fakult{\"a}t, Friedrich-Alexander-Uni\-ver\-si\-t{\"a}t
		  Er\-langen-N{\"u}rn\-berg},
  abstract = {The calculus of higher-order subtyping, known as
		  $F_\leq^\omega$, a higher-order polymorphic
		  $\lambda$-calculus with subtyping, is expressive enough to
		  serve as core calculus for typed object-oriented languages.
		  The versions considered in the literature usually support
		  only pointwise subtyping of type operators, where two types
		  $S\ U$ and $T\ U$ are in subtype relation, if $S$ and $T$
		  are. In the widely cited, unpublished
		  note~\cite{cardelli:notes}, Cardelli presents
		  $F_\leq^\omega$ in a more general form going beyond
		  pointwise subtyping of type applications in distinguishing
		  between monotone and antimonotone operators. Thus, for
		  instance, $T\ U_1$ is a subtype of $T\ U_2$, if $U_1\leq
		  U_2$ and $T$ is a monotone operator.
		  
		  My thesis extends $F_\leq^\omega$ by polarized application,
		  it explores its proof theory, establishing decidability of
		  polarized $F_\leq^\omega$. The inclusion of polarized
		  application rules leads to an interdependence of the
		  subtyping and the kinding system. This contrasts with pure
		  $F_\leq^\omega$, where subtyping depends on kinding but not
		  vice versa. To retain decidability of the system, the
		  equal-bounds subtyping rule for all-types is rephrased in
		  the polarized setting as a mutual-subtype requirement of
		  the upper bounds.},
  url = {http://www.ifi.uio.no/~msteffen/download/diss/diss.pdf},
  annote = {Defended 12.11.1998}
}
@inproceedings{steffen:polarized-abstract,
  author = {Martin Steffen},
  title = {Polarized Higher-Order Subtyping (Extended Abstract)},
  crossref = {subtyping-workshop97},
  note = {12 pages},
  url = {http://www.ifi.uio.no/~msteffen/download/97/polarized-abstract.ps.gz}
}
@inproceedings{steffen:semanticsgorutinesdefer,
  author = {Martin Steffen},
  title = {A Small-Step Semantics of a Concurrent Calculus With
		  Goroutines and Deferred Functions},
  crossref = {lncs9660},
  pages = {393--406},
  keywords = {semantics, Go, deferred function},
  month = oct,
  url = {http://www.ifi.uio.no/~msteffen/download/16/semantics-goroutinesdefer.pdf}
}
@inproceedings{stumpf.johnsen.steffen:vta-abstract-ifm,
  author = {Johanna Beate Stumpf and Einar Broch Johnsen and Martin
		  Steffen},
  title = {Virtually Timed Ambients: Formalization and Analysis
		  (extended abstract)},
  booktitle = {Informal proceedings of the PhD Symposium at iFM'17
		  (integrated Formal Methods)},
  year = 2017,
  month = jun,
  url = {http://www.ifi.uio.no/~msteffen/download/17/vta-abstract-ifmds.pdf},
  note = {Submitted for presentation}
}
@inproceedings{tran.steffen.truong:compositional,
  author = {Thi {Mai Thuong Tran} and Martin Steffen and Hoang Truong},
  title = {Compositional Static Analysis for Implicit Join
		  Synchronization in a Transactional Setting},
  year = 2013,
  url = {http://www.ifi.uio.no/~msteffen/download/13/compositional.pdf},
  month = sep,
  pages = {212-228},
  crossref = {lncs8137}
}
@article{tran.steffen.truong:compositional-journal,
  author = {Thi {Mai Thuong Tran} and Martin Steffen and Hoang Truong},
  title = {Compositional Static Analysis for Implicit Join
		  Synchronization in a Transactional Setting},
  year = 2014,
  month = sep,
  note = {Submitted for journal publication, as extended version of
		  the accepted SEFM conference contribution},
  annote = {SEFM Journal}
}
@inproceedings{tran.steffen.truong:compositional-nwpt,
  author = {Thi {Mai Thuong Tran} and Martin Steffen and Hoang Truong},
  title = {Compositional Analysis of Resource Bounds for Software
		  Transactions},
  year = 2012,
  month = oct,
  crossref = {nwpt12},
  url = {http://www.ifi.uio.no/~msteffen/download/12/compositional-nwpt.pdf},
  annote = {submitted 21. Sept. 2012}
}
@techreport{tran.steffen.truong:estimating-rep,
  author = {Thi {Mai Thuong Tran} and Martin Steffen and Hoang Truong},
  title = {Estimating Resource Bounds for Software Transactions},
  institution = {University of Oslo, Dept.\ of Informatics},
  year = 2011,
  type = {Technical report},
  number = {414},
  url = {http://urn.nb.no/URN:NBN:no-30010},
  isbn = {82-7368-376-1},
  issn = {0806-3036},
  month = dec
}
@inproceedings{tran.steffen.truong:resources-nwpt,
  author = {Thi {Mai Thuong Tran} and Martin Steffen and Hoang Truong},
  title = {Estimating Resource Bounds for Software Transactions
		  (extended abstract)},
  year = 2011,
  month = oct,
  crossref = {nwpt11},
  url = {http://www.ifi.uio.no/~msteffen/download/11/resources-nwpt.pdf},
  annote = {submitted 23. Sept. 2011},
  pages = {77--79}
}
@inproceedings{traulsen.steffen:constraints-abstract,
  author = {Claus Traulsen and Martin Steffen},
  title = {Using Constraints for Model Checking Buffered Systems
		  (Extended Abstract)},
  booktitle = {Informal Proceeding of the 17th Nordic Workshop on
		  Programming Theory},
  month = sep,
  year = 2005,
  url = {http://www.ifi.uio.no/~msteffen/download/05/constraints-abstract.pdf},
  date = {13.9.2005},
  abstract = {Model checking is a widely used method for software and
		  hardware validation. It shows either the correctness of a
		  program or produces a counter-example, by performing a
		  search on the whole state space. Therefore model checking
		  is very sensitive to the size of the state space. The
		  number of states may grow exponentially with the number of
		  processes in a parallel composition. Especially for systems
		  that communicate asynchronously, the queues contribute to a
		  combinatorial explosion of the state space.
		  
		  In this paper we use constraints to represent states in
		  enumerative model checking. This reduces the state space by
		  merging states that differ only in the data in the queue.
		  In contrast to abstraction, this method is exact, i.e.,
		  only the truly reachable states are considered. The
		  representation with constraints has advantages for systems
		  whose behavior is influenced by random data, such as open
		  systems. To substantiate its benefits, is is compared to
		  the standard representation of states with concrete values
		  for variables and with state-of-the-art model checkers.},
  keywords = {Model Checking, Asynchronous Systems, Queues}
}
@inproceedings{vu.truong.tran.steffen:typesystem,
  author = {Tung Vu Xuan and Hoang Truong Anh and Thi {Mai Thuong
		  Tran} and Martin Steffen},
  title = {A Type System for Finding Upper Resource Bounds of
		  Multi-Threaded Programs with Nested Transactions},
  booktitle = {ACM Proceedings of the 3rd ACM International Symposium on
		  Information and Communication Technology SoICT},
  year = 2012,
  annote = {submitted 8. May 2012},
  month = aug,
  pages = {20-31},
  doi = {10.1145/2350716.2350722},
  publisher = {ACM}
}
@inproceedings{nestmann.steffen:dagstuhl,
  author = {Uwe Nestmann and Martin Steffen},
  title = {Correct Transformational Design of Concurrent Search
		  Structures},
  pages = {23--42 (20 pages)},
  crossref = {freitag*:objectorientation},
  abstract = {Storage and retrieval of large amounts of data are often
		  based on tree-like structures. Efficiency, indispensable in
		  large distributed databases, is achieved by admitting
		  internal concurrency. Concurrent operations behave
		  correctly when they conform with the observable
		  I/O-behaviour of their sequential counterparts.
		  
		  The correct design of concurrent search structures has also
		  been proposed and studied in an object-based language
		  setting. There, concurrent versions are derived from
		  correctly specified sequential ones by means of
		  \emph{program transformation.} In order to formally prove
		  the correctness of such transformations, both an
		  operational semantics at the object level and an underlying
		  process calculus semantics have been explored.
		  
		  In both the database and the object-based language
		  approaches to the correct design of concurrent search
		  structures, the crucial point is the formalisation of an
		  acceptable correctness criterion. In this paper, we use the
		  underlying process calculus semantics of the object-based
		  approach in order to formalise a notion of correctness, as
		  motivated from the database view on concurrent search
		  structures, and show its application to a known example
		  program transformation.}
}
@inproceedings{nestmann.steffen:typing,
  author = {Uwe Nestmann and Martin Steffen},
  title = {Typing Confluence},
  crossref = {fmics97},
  url = {http://www.ercim.org/publication/technical_reports/052-abstract.html},
  pages = {77--101 (25 pages)},
  note = {Also available as report ERCIM-10/97-R052, European
		  Research Consortium for Informatics and Mathematics,
		  1997.},
  abstract = {We investigate confluence properties for concurrent
		  systems of message-passing processes, because such
		  properties have proved to be useful for a variety of
		  applications, ranging from reasoning about concurrent
		  objects to mobile and high-speed telecommunication
		  protocols. Roughly, confluence means that for every two
		  computations starting from a common system state, it is
		  possible to continue the computations, so to reach a common
		  state again. In order to prove confluence for a given
		  system, we are required to demonstrate that for all states
		  reachable by computation from the starting state, the
		  'owing together' of possible computations is possible. In
		  this paper, we aim at proving confluence properties for
		  concurrent systems without having to generate all reachable
		  states. Instead, we use a type system that supports a
		  static analysis of possible sources of non-confluence. In
		  message-passing systems, confluence is invalidated whenever
		  two processes compete for communication with another
		  process. We may statically check the occurrence of such
		  situations by reducing them to the concurrent access on a
		  shared communication port. For the technical development,
		  we focus on the setting of a polarized pi-calculus, where
		  we formalize the notion of port-uniqueness by means of
		  overlapping-free context-redex decompositions. We then
		  present a type system for port-uniqueness that, taking
		  advantage of a subject reduction property, yields a
		  succicnt criterion for guaranteeing confluence.}
}
@proceedings{lncs8702,
  title = {Proceedings of SEFM'14},
  booktitle = {Proceedings of SEFM'14},
  year = 2014,
  month = sep,
  volume = 8702,
  series = {Lecture Notes in Computer Science},
  editor = {Dimitra Giannakopoulou and Gwen Sala{\"u}n},
  publisher = {Springer Verlag}
}
@proceedings{lncs8137,
  title = {Proceedings of SEFM'13},
  booktitle = {Proceedings of SEFM'13},
  year = 2013,
  volume = 8137,
  series = {Lecture Notes in Computer Science},
  editor = {George Eleftherakis and Mike Hinchey and Mike Holcombe},
  publisher = {Springer Verlag}
}
@proceedings{lncs6396,
  title = {Proceedings of the 8th International Conference on
		  Integrated Formal Methods (iFM 2010)},
  booktitle = {Proceedings of the 8th International Conference on
		  Integrated Formal Methods (iFM 2010)},
  year = 2010,
  editor = {Dominique M{\'e}ry and Stephan Merz},
  series = {Lecture Notes in Computer Science},
  volume = 6396,
  isbn = {978-3-642-16264-0},
  month = oct,
  publisher = {Springer Verlag}
}
@proceedings{lncs9660,
  title = {Theory and Practice of Formal Methods. Essays Dedicated to
		  {F}rank de {B}oer on the Occasion of His 60th Birthday
		  (Festschrift)},
  booktitle = {Theory and Practice of Formal Methods. Essays Dedicated to
		  {F}rank de {B}oer on the Occasion of His 60th Birthday
		  (Festschrift)},
  year = 2016,
  editor = {Erika {\'A}brah{\'a}m and Marieke Huisman and Einar Broch
		  Johnsen},
  series = {Lecture Notes in Computer Science},
  volume = 9660,
  publisher = {Springer Verlag}
}
@proceedings{lncs9681,
  title = {Proc.\ of the 12th International Conference on integrated
		  Formal Methods (iFM 2010)},
  booktitle = {Proc.\ of the 12th International Conference on integrated
		  Formal Methods (iFM 2010)},
  year = 2016,
  editor = {Erika {\'A}brah{\'a}m and Marieke Huisman},
  series = {Lecture Notes in Computer Science},
  volume = 9681,
  publisher = {Springer Verlag}
}
@proceedings{lncs9952,
  booktitle = {7th International Symposium On Leveraging Applications of
		  Formal Methods, Verification and Validation (ISOLA'16)},
  title = {7th International Symposium On Leveraging Applications of
		  Formal Methods, Verification and Validation (ISOLA'16)},
  editor = {Tiziana Margaria and Bernhard Steffen},
  year = 2016,
  volume = 9952,
  month = oct,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{nwpt08,
  title = {Proceedings of the Nordic Workshop of Programming Theory
		  '08 (Abstracts), Tallinn},
  booktitle = {Proceedings of the Nordic Workshop of Programming Theory
		  '08 (Abstracts), Tallinn},
  year = 2008,
  editor = {Tarmu Uustalu and J{\"u}ri Vain and Juhan Ernits},
  isbn = {978-9949-430-24-6},
  note = {Institute of Cybernetics at TUT, Tallinn, Technical
		  Report}
}
@proceedings{nwpt07,
  booktitle = {Proceedings of the 19th Nordic Workshop on Programming
		  Theory (NWPT'07). Extended Abstracts. University of Oslo,
		  Dept.\ of Computer Science, Technical Report 366},
  title = {Proceedings of the 19th Nordic Workshop on Programming
		  Theory (NWPT'07). Extended Abstracts. University of Oslo,
		  Dept.\ of Computer Science, Technical Report 366},
  editor = {Einar B. Johnsen and Olaf Owe and Gerardo Schneider},
  year = 2007,
  month = oct
}
@proceedings{lncs7684,
  title = {Revised Selected Papers of the 9th International Workshop
		  on Formal Aspects of Component Software (FACS 2012)},
  booktitle = {Revised Selected Papers of the 9th International Workshop
		  on Formal Aspects of Component Software (FACS 2012)},
  editor = {Corina S. Pasareanu and Gwen Sala{\"u}n},
  year = 2013,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  isbn = {978-3-642-35861-6}
}
@proceedings{lncs5930,
  title = {Concurrency, Compositionality, and Correctness: Essays in
		  Honor of Willem-Paul de Roever},
  booktitle = {Concurrency, Compositionality, and Correctness: Essays in
		  Honor of Willem-Paul de Roever},
  year = 2010,
  editor = {Dennis Dams and Ulrich Hannemann and Martin Steffen},
  series = {Lecture Notes in Computer Science},
  isbn = {978-3-642-11511-0},
  subseries = {Theoretical Computer Science and General Issues},
  url = {http://www.springer.com/computer/theoretical+computer+science/foundations+of+computations/book/978-3-642-11511-0},
  publisher = {Springer Verlag},
  note = {377 pages},
  number = 5930
}
@proceedings{fmics97,
  title = {Second International ERCIM Workshop on Formal Methods in
		  Industrial Critical Systems (Cesena, Italy, July 4--5,
		  1997)},
  booktitle = {Proceedings of the Second International Workshop on Formal
		  Methods for Industrial Critical Systems, FMICS '97},
  year = 1997,
  editor = {Stefania Gnesi and Diego Latella},
  publisher = {Consiglio Nazionale Ricerche di Pisa},
  crossrefonly = 1
}
@book{freitag*:objectorientation,
  editor = {Burkhard Freitag and Clifford Jones and Christian Lengauer
		  and Hans-J{\"o}rg Schek},
  title = {Object-Orientation with Parallelism and Persistence},
  booktitle = {Object-Orientation with Parallelism and Persistence},
  series = {Now: The Springer International Series in Engineering and
		  Computer Science (Hardcover)},
  publisher = {Kluwer Academic Publishers},
  year = 1996,
  crossrefonly = 1
}
@book{giitg5,
  title = {Formale Beschreibungstechniken f{\"u}r verteilte Systeme},
  booktitle = {Formale Beschreibungstechniken f{\"u}r verteilte Systeme},
  publisher = {Universit{\"a}t Kaiserslautern, Fachbereich Informatik},
  year = 1995,
  editor = {Reinhard Gotzhein and Jan Bredereke},
  url = {http://www.informatik.uni-kl.de/aggotz/},
  month = {22./23.\ Juni}
}
@proceedings{entcs-fsen05,
  key = {FSEN'05},
  title = {FSEN '05: IPM International Conference on Foundations of
		  Software Engineering (Theory and Practice). Oct. 1 -- 3,
		  2005},
  booktitle = {FSEN '05: IPM International Conference on Foundations of
		  Software Engineering (Theory and Practice). Oct. 1 -- 3,
		  2005)},
  year = 2005,
  month = may,
  editor = {Farhad Arbab and Marjan Sirjani},
  volume = {159},
  doi = {doi:10.1016/j.entcs.2005.12.072},
  xxxurl = {http://www.elsevier.nl/locate/entcs/volume16.3.html},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  crossrefonly = 1
}
@proceedings{lncs7141,
  key = {FSEN'11},
  title = {Proceedings of the International Conference on Foundations
		  of Software Engineering (Theory and Practice) (FSEN'11)},
  booktitle = {Proceedings of the International Conference on Foundations
		  of Software Engineering (Theory and Practice) (FSEN'11)},
  year = 2012,
  series = {Lecture Notes in Computer Science},
  volume = 7141,
  publisher = {Springer Verlag}
}
@proceedings{lncs8161,
  key = {FSEN'13},
  title = {Proceedings of the International Conference on Foundations
		  of Software Engineering (Theory and Practice) (FSEN'13)},
  booktitle = {Proceedings of the International Conference on Foundations
		  of Software Engineering (Theory and Practice) (FSEN'13)},
  year = 2013,
  series = {Lecture Notes in Computer Science},
  volume = 8161,
  publisher = {Springer Verlag}
}
@proceedings{lncs5014,
  key = {FM08},
  title = {Proceedings of the 15th International Symposium on Formal
		  Methods (FM'08)},
  booktitle = {Proceedings of the 15th International Symposium on Formal
		  Methods (FM'08)},
  year = 2008,
  series = {Lecture Notes in Computer Science},
  editor = {Jorge Cuellar and Tom Maibaum and Kaisa Sere},
  volume = 5014,
  publisher = {Springer Verlag}
}
@proceedings{lncs1680,
  title = {Theoretical and Practical Aspects of {SPIN} Model
		  Checking, Proceedings of 5th and 6th International {SPIN}
		  Workshops, Trento/Toulouse},
  booktitle = {Theoretical and Practical Aspects of {SPIN} Model
		  Checking, Proceedings of 5th and 6th International {SPIN}
		  Workshops, Trento/Toulouse},
  year = 1999,
  editor = {Dennis Dams and Rob Gerth and Stefan Leue and Mieke
		  Massink},
  volume = 1680,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{fct11-iandc,
  title = {Information and Computation: Special issue with selected
		  publications of FCT '11u},
  year = 2013,
  editor = {Olaf Owe and Martin Steffen and Jan Arne Telle},
  volume = 231,
  month = oct,
  issn = {ISSN 0890-5401},
  publisher = {Elsevier}
}
@proceedings{lncs6914,
  key = {FCT'11},
  title = {Proceedings of FCT '11},
  booktitle = {Proceedings of FCT '11: Fundamentals of Computation
		  Theory, 18th International Symposium (Oslo, Norway, August
		  25 -- 28, 2011)},
  year = 2011,
  editor = {Olaf Owe and Martin Steffen and Jan Arne Telle},
  volume = 6914,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  crossrefonly = 1
}
@proceedings{lncs3988,
  title = {Proceedings of Logical Approaches to Computational
		  Barriers: Second Conference on Computability in Europe, CiE
		  2006, Swansea, UK, June 30-July 5, 2006.},
  booktitle = {Logical Approaches to Computational Barriers: CiE 2006},
  year = 2006,
  editor = {Arnold Beckmann and Ulrich Berger and Benedikt L{\"o}we
		  and John V. Tucker},
  doi = {10.1007/11780342},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = 3988,
  month = jul
}
@proceedings{lncs10012,
  booktitle = {Proceedings of the 16th International Conference on
		  Runtime Verification, RV 2016, Madrid, Spain, September
		  23-30, 2016},
  title = {Proceedings of the 16th International Conference on
		  Runtime Verification, RV 2016, Madrid, Spain, September
		  23-30, 2016},
  year = 2016,
  volume = 10012,
  editor = {C{\'e}sar S{\'a}nchez},
  month = sep,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{procomet94,
  key = {PROCOMET'94},
  title = {Working Conference on Programming Concepts, Methods and
		  Calculi, San Miniato, Italy},
  booktitle = {Proceedings of PROCOMET '94},
  year = 1994,
  editor = {Ernst-R{\"u}diger Olderog},
  publisher = {North-Holland},
  organization = {IFIP},
  month = jun,
  crossrefonly = 1
}
@proceedings{nwpt11,
  key = {NWPT'11},
  title = {Proceedings of the 23nd Nordic Workshop on Programming
		  Theory (NWPT'11)},
  booktitle = {Proceedings of the 23nd Nordic Workshop on Programming
		  Theory (NWPT'11)},
  year = 2011,
  month = oct,
  issn = {1404-3041},
  type = {Technical report},
  volume = {254/2011},
  publisher = {M{\"a}lardalen Real-time Research Centre, M{\"a}lardalen
		  University}
}
@proceedings{nwpt12,
  key = {NWPT'12},
  title = {Proceedings of the 24nd Nordic Workshop on Programming
		  Theory (NWPT'12)},
  booktitle = {Proceedings of the 24nd Nordic Workshop on Programming
		  Theory (NWPT'12)},
  year = 2012,
  month = oct,
  publisher = {Dept. of Informatics, University of Bergen, Report Nr.
		  403}
}
@proceedings{nwpt16,
  key = {NWPT'16},
  title = {Proceedings of the 28nd Nordic Workshop on Programming
		  Theory (NWPT'16)},
  booktitle = {Proceedings of the 24nd Nordic Workshop on Programming
		  Theory (NWPT'16)},
  year = 2016
}
@proceedings{subtyping-workshop97,
  booktitle = {Electronic Proceedings of the Types working group Workshop
		  on Subtyping, inheritance and modular development of
		  proofs},
  title = {Electronic Proceedings of the Types working group Workshop
		  on Subtyping, inheritance and modular development of
		  proofs},
  year = 1997,
  editor = {Zhaohui Luo and Sergei Soloviev},
  month = aug
}
@proceedings{lncs9995,
  title = {Proceedings of the International Symposium on Formal
		  Methods ({FM} 2016)},
  booktitle = {Proceedings of the International Symposium on Formal
		  Methods ({FM} 2016)},
  year = 2016,
  editor = {J. Fitzgerald and C. Heitmeyer C and S. Gnesi and A.
		  Philippou and Michael Butler and Wolfram Schulte},
  volume = 9995,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs5423,
  title = {Proceedings of the 7th International Conference on
		  integrated Formal Methods (iFM'09), D{\"u}sseldorf,
		  Germany, 16 -- 19 February, 2009},
  booktitle = {Proceedings of the 7th International Conference on
		  integrated Formal Methods (iFM'09), D{\"u}sseldorf,
		  Germany, 16 -- 19 February, 2009},
  year = 2009,
  editors = {Michael Leuschel and Heike Wehrheim},
  series = {Lecture Notes in Computer Science},
  month = feb,
  volume = 5423,
  publisher = {Springer Verlag}
}
@proceedings{lncs2078,
  title = {Proceedings of the 10th International SDL Forum SDL 2001:
		  Meeting UML},
  booktitle = {Proceedings of the 10th International SDL Forum SDL 2001:
		  Meeting UML},
  year = 2001,
  editor = {Rick Reed and Jeanne Reed},
  volume = 2078,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs2102,
  title = {Proceedings of the 13th International Conference on
		  Computer-Aided Verification, Paris, France},
  booktitle = {Proceedings of the 13th International Conference on
		  Computer-Aided Verification, CAV '01},
  year = 2001,
  editor = {G{\'e}rard Berry and Hubert Comon and Alain Finkel},
  volume = 2102,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs2126,
  title = {SAS'01: 8th International Static Analysis Symposium
		  (Paris, France)},
  booktitle = {Proceedings of the 8th International Static Analysis
		  Symposium, SAS '01},
  year = 2001,
  editor = {Patrick Cousot},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = 2126
}
@proceedings{lncs2178,
  title = {Computer Aided Systems Theory (EUROCAST 2001), A Selection
		  of Papers from the 8th International Workshop on Computer
		  Aided Systems Theory, Las Palmas de Gran Canaria, Spain,
		  February 19--23, 2001.},
  booktitle = {Computer Aided Systems Theory (EUROCAST 2001), Selected
		  and revised papers},
  year = 2001,
  editor = {Roberto Moreno-D\'{i}az and Bruno Buchberger},
  volume = 2178,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs2294,
  title = {Proceedings of the 3rd International Workshop on
		  Verification, Model Checking, and Abstract Interpretation
		  (VMCAI) 2002},
  booktitle = {Proceedings of the 3rd International Workshop on
		  Verification, Model Checking, and Abstract Interpretation
		  (VMCAI) 2002},
  editor = {Agostino Cortesi},
  year = 2002,
  volume = 2294,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs2391,
  title = {Proceedings of Formal Methods Europe: Formal Methods --
		  {G}etting {IT} Right (FME'02)},
  booktitle = {Proceedings of Formal Methods Europe: Formal Methods --
		  {G}etting {IT} Right (FME'02)},
  year = 2002,
  editor = {Lars-Henrik Eriksson and Peter A. Lindsay},
  volume = 2391,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs2303,
  key = {FoSSaCS2002},
  title = {Proceedings of the 5th International Conference on
		  Foundations of Software Science and Computation Structures
		  ({FoSSaCS} 2002), Held as Part of the Joint European
		  Conferences on Theory and Practice of Software ({ETAPS}
		  2002), (Grenoble, France, April 8-12, 2002)},
  booktitle = {Proceedings of {FoSSaCS} 2002},
  year = 2002,
  editor = {Mogens Nielsen and Uffe H. Engberg},
  volume = 2303,
  series = {Lecture Notes in Computer Science},
  month = apr,
  publisher = {Springer Verlag},
  crossrefonly = 1
}
@proceedings{lncs2772,
  title = {Proceedings of the International Symposium on Verification
		  (Theory and Practice), Celebrating Zohar Manna's 64th
		  Birthday, Taormina, Sicily, June 29--July 4, 2003},
  year = 2004,
  booktitle = {International Symposium on Verification (Theory and
		  Practice), July 2003},
  editor = {Nachum Derschowitz},
  volume = 2772,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  annote = {Check the data}
}
@proceedings{lncs2852,
  title = {Proceedings of the First International Symposium on Formal
		  Methods for Components and Objects (FMCO 2002), Leiden},
  booktitle = {FMCO 2002},
  year = 2003,
  editor = {Marcello M. Bonsangue and Frank S. de Boer and Willem-Paul
		  de Roever and Susanne Graf},
  series = {Lecture Notes in Computer Science},
  volume = 2852,
  publisher = {Springer Verlag}
}
@proceedings{lncs6957,
  title = {Proceedings of the 9th International Symposium on Formal
		  Methods for Components and Objects, FMCO 2010, Selected
		  Papers},
  booktitle = {Proceedings of the 9th International Symposium on Formal
		  Methods for Components and Objects, FMCO 2010, Selected
		  Papers},
  year = 2011,
  editor = {B.K. Aichernig and F.S. de Boer and M.M. Bonsangue},
  series = {Lecture Notes in Computer Science},
  volume = 6957,
  isbn = {978-3-642-25270-9},
  ee = {http://dx.doi.org/10.1007/978-3-642-25271-6},
  publisher = {Springer Verlag}
}
@proceedings{lncs6286,
  title = {Proceedings of the 8th International Symposium on Formal
		  Methods for Components and Objects, FMCO 2009, Selected
		  Papers},
  booktitle = {Proceedings of the 8th International Symposium on Formal
		  Methods for Components and Objects, FMCO 2009, Selected
		  Papers},
  year = 2009,
  editor = {Marcello M. Bonsangue and Frank S. de Boer and Stefan
		  Hallerstede and Michael Leuschel},
  series = {Lecture Notes in Computer Science},
  volume = 6286,
  publisher = {Springer Verlag}
}
@proceedings{lncs3385,
  title = {Proceedings of the 6th International Workshop on
		  Verification, Model Checking, and Abstract Interpretation
		  (VMCAI 2005), January 17-19, 2005},
  booktitle = {Proceedings of the 6th International Workshop on
		  Verification, Model Checking, and Abstract Interpretation
		  (VMCAI 2005)},
  year = 2005,
  editor = {Radhia Cousot},
  volume = 3385,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs3188,
  title = {Proceedings of the Second International Symposium on
		  Formal Methods for Components and Objects (FMCO 2003)},
  booktitle = {Proceedings of the Second International Symposium on
		  Formal Methods for Components and Objects (FMCO 2003)},
  year = 2004,
  editor = {Marcello Bonsangue and Frank S. de Boer and Willem-Paul de
		  Roever and Susanne Graf},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = 3188
}
@proceedings{lncs3657,
  title = {Proceedings of the Third International Symposium on Formal
		  Methods for Components and Objects (FMCO 2004)},
  booktitle = {Proceedings of the Third International Symposium on Formal
		  Methods for Components and Objects (FMCO 2004)},
  year = 2005,
  editor = {Marcello Bonsangue and Frank S. de Boer and Willem-Paul de
		  Roever and Susanne Graf},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = 3657
}
@proceedings{lncs3535,
  title = {Proceedings of the 7th IFIP International Conference on
		  Formal Methods for Open Object-Based Distributed Systems
		  (FMOODS '05), Athens, Greece},
  booktitle = {FMOODS '05},
  year = 2005,
  editor = {Martin Steffen and Gianluigi Zavattaro},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = 3535
}
@proceedings{lncs4037,
  title = {Proceedings of the 8th IFIP International Conference on
		  Formal Methods for Open Object-Based Distributed Systems
		  (FMOODS '06), Bologna, Italy},
  booktitle = {FMOODS '06},
  year = 2006,
  editor = {Roberto Gorrieri and Heike Wehrheim},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  volume = 4037
}
@proceedings{lncs2884,
  title = {Proceedings of the 6th IFIP International Conference on
		  Formal Methods for Open Object-Based Distributed Systems
		  (FMOODS '03), Paris},
  booktitle = {FMOODS '03},
  year = 2003,
  editor = {Elie Najm and Uwe Nestmann and Perdita Stevens},
  series = {Lecture Notes in Computer Science},
  volume = 2884,
  month = nov,
  publisher = {Springer Verlag}
}
@proceedings{lncs3407,
  key = {ICTAC04},
  title = {Proceedings of the International Colloquium on Theoretical
		  Aspects of Computing, ICTAC 2004},
  booktitle = {ICTAC'04},
  year = 2004,
  volume = 3407,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@proceedings{lncs5961,
  editor = {Farhad Arbab and Marjan Sirjani},
  title = {Fundamentals of Software Engineering, Third IPM
		  International Conference, FSEN 2009, Kish Island, Iran,
		  April 15-17, 2009, Revised Selected Papers},
  booktitle = {FSEN},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5961},
  year = {2010},
  isbn = {978-3-642-11622-3},
  ee = {http://dx.doi.org/10.1007/978-3-642-11623-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

This file was generated by bibtex2html 1.97.