[1] Erika Ábrahám, Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen. Observability, connectivity, and replay in a sequential calculus of classes. In Bonsangue et al. [192], pages 296-316 (21 pages). [ bib | .pdf ]
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 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 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 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
[2] Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen. Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming, 78(7):491-518 (28 pages), 2009. Special issue with selected contributions of NWPT'07. The paper is a reworked version of an earlier UiO Technical Report TR-364, Oct. 2007. [ bib | DOI | .pdf ]
[3] Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen. Abstract interface behavior of an object-oriented language with futures and promises (extended abstract). In Johnsen et al. [157]. [ bib | .pdf ]
[4] Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen. Behavioral interface description of an object-oriented language with futures and promises. Technical Report 364, University of Oslo, Dept. of Informatics, October 2007. 38 pages. [ bib | .pdf ]
[5] Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen. Memory-aware bounded model checking for linear hybrid systems. In Proceedings of the 9th. Workshop for “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV06), January 2006. 10 pages. [ bib | .pdf ]
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.

[6] Erika Ábrahám, Bernd Becker, Felix Klaedke, and Martin Steffen. Optimizing bounded model checking for linear hybrid systems. In Cousot [190], pages 396-412 (17 pages). [ bib | .pdf ]
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.

[7] Erika Ábrahám, Bernd Becker, Felix Klaedke, and Martin Steffen. Optimizing bounded model checking for linear hybrid systems. Technical report TR214, Albert-Ludwigs-Universität Freiburg, Fakultät für Angewandte Wissenschaften, Institut für Informatik, November 2004. [ bib | http ]
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.

[8] Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen. Bounded model checking with parametric data structures. Electronic Notes in Theoretical Computer Science, 174(3):3-16 (14 pages), May 2007. Special Issue for the Proceedings of the Fourth International Workshop on Bounded Model Checking (BMC06). [ bib | DOI | http ]
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.

[9] Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Deductive verification for multithreaded Java (extended abstract). In Proceedings of the “11. Kolloquium Programmiersprachen und Grundlagen der Programmierung”, 2001, Rurberg, pages 121-126, 2001. [ bib ]
[10] Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, and Martin Steffen. A structural operational semantics for a concurrent class calculus. Technical Report 0307, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, August 2003. [ bib | .html ]
The concurrent ν-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 ν-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.

[11] Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, and Martin Steffen. Classes, object connectivity, and observability (extended abstract). In Informal Electronic Proceedings of the “12. Kolloquium Programmiersprachen und Grundlagen der Programmierung”. University Freiburg, April 2004. [ bib | http ]
[12] Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, and Martin Steffen. Object connectivity and full abstraction for a concurrent calculus of classes. In ICTAC04 [196], pages 37-51 (15 pages). [ bib | DOI | .pdf ]
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 Java. One distinctive feature, however, of the concurrent object calculus is that it is object-based, whereas the mainstream of object-oriented languages is 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 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 (“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
[13] Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, and Martin Steffen. Object connectivity and full abstraction for a concurrent calculus of classes. Preliminary technical report, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, January 2005. [ bib | http ]
[14] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. An assertion-based proof system for multithreaded Java. Theoretical Computer Science, 331:251-290 (40 pages), 2005. [ bib | DOI ]
[15] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A deductive proof system for multithreaded Java with exceptions. Fundamenta Informaticae, 82(4):391-463 (73 pages), 2008. 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. [ bib | http ]
[16] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Inductive proof outlines for exceptions in multithreaded Java. In Arbab and Sirjani [163], pages 281-297 (17 pages). An extended version appeared in Fundamentae Informaticae. [ bib | .pdf ]
In this paper we give an operational semantics and introduce an assertional proof system for exceptions in a multithreaded Java sublanguage.

Keywords: Java, multi-threading, exceptions, proof systems
[17] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Inductive proof outlines for multithreaded Java with exceptions. Technical Report 0313, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, December 2003. [ bib | .html ]
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 assertional proof method for JavaMT (“Multi-Threaded Java”), a small concurrent sublanguage of Java, covering concurrency and especially exception handling. We show soundness and relative completeness of the proof method.

[18] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A Hoare logic for monitors in Java. Techical report TR-ST-03-1, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, April 2003. 80 pages. [ bib | .pdf ]
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. To reason about safety-properties of multithreaded programs, we introduce in this paper a tool-supported assertional proof method for JavaMT (“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.

[19] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Inductive proof-outlines for monitors in Java. In Najm et al. [195], pages 155-169 (15 pages). A longer version appeared as technical report TR-ST-03-1, April 2003. [ bib | .pdf ]
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
[20] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Heap-abstraction for an object-oriented calculus with thread classes. Journal of Software and Systems Modelling (SoSyM), 7(2):177-208 (32 pages), May 2008. [ bib | DOI | .pdf ]
[21] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Dynamic heap-abstraction for open, object-oriented systems with thread classes (extended abstract). In Beckmann et al. [170], pages 1-10 (10 pages). 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. [ bib | DOI | .pdf ]
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 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 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 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
[22] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Dynamic heap-abstraction for open, object-oriented systems with thread classes. In Radu Iosif and Dino Distefano, editors, 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, pages 47-61 (14 pages), July 2005. [ bib ]
[23] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Dynamic heap-abstraction for open, object-oriented systems with thread classes. Technical Report 0601, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, January 2006. 40 pages. A slightly shorter version is accepted for inclusion into the Journal of Software and Systems Modeling (SoSym). [ bib | .html ]
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 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 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 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
[24] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Abstract interface behavior of object-oriented languages with monitors. In Gorrieri and Wehrheim [194], pages 218-232 (15 pages). [ bib | DOI | http ]
We characterize the observable behavior of multi-threaded, object-oriented programs with 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
[25] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Abstract interface behavior of object-oriented languages with monitors. Technical Report 0612, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, October 2006. 43 pages. [ bib ]
[26] Erika Ábrahám, Andreas Grüner, and Martin Steffen. Abstract interface behavior of object-oriented languages with monitors. Theory of Computing Systems, 43(3-4):322-361 (40 pages), December 2008. [ bib | DOI | .pdf ]
Keywords: oo languages, formal semantics, thread-based concurrency, monitors, open systems, observable behavior
[27] Erika Ábrahám, Thi Mai Thuong Tran, and Martin Steffen. Observable interface behavior and inheritance. Mathematical Structures in Computer Science (Special Issue on Behavioral Types), 26:561-605, November 2014. Published online 13 November 2014. The paper is a reworked version of the earlier UiO IFI technical report 409. [ bib | DOI | http ]
[28] Erika Ábrahám, Thi Mai Thuong Tran, and Martin Steffen. Observable interface behavior and inheritance (extended abstract). In NWPT'11 [173]. [ bib | .pdf ]
[29] Erika Ábrahám, Thi Mai Thuong Tran, and Martin Steffen. Observable interface behavior and inheritance. Technical Report 409, University of Oslo, Dept. of Informatics, April 2011. www.ifi.uio.no/~msteffen/publications.html#techreports. [ bib ]
[30] Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A compositional operational semantics for JavaMT. In Derschowitz [186], pages 290-303 (14 pages). A preliminary version appeared as Technical Report TR-ST-02-2, May 2002. [ bib | http ]
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. This report contains a compositional version of the operational semantics of JavaMT.

[31] Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A compositional operational semantics for Java_MT. Technical Report TR-ST-02-2, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, May 2002. 15 pages. [ bib | .ps.gz ]
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. This report contains a compositional version of the operational semantics of Java_MT.

[32] Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Verification for Java's reentrant multithreading concept. In Nielsen and Engberg [185], pages 4-20 (17 pages). A longer version, including the proofs for soundness and completeness, appeared as Technical Report TR-ST-02-1, March 2002. [ bib | http ]
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model offers coordination via lock-synchronization, and 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 assertional proof method for JavaMT (“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.

[33] Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Verification for Java's reentrant multithreading concept: Soundness and completeness. Technical Report TR-ST-02-1, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, 2002. 95 pages. [ bib | http ]
Besides the features of a class-based object-oriented language, Jav integrates concurrency via its thread-classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. To reason about multithreaded programs, we introduce in this paper an assertional proof method for safety properties for JavaMT (“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.

[34] Erika Ábrahám-Mumm, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A tool-supported proof system for monitors in Java. In Bonsangue et al. [187], pages 1-32 (33 pages). [ bib | http ]
To reason about safety properties of multithreaded Java programs, we introduce a tool-supported assertional proof method for JavaMT (“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.

[35] Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen. Assertion-based analysis of hybrid systems with PVS. In Moreno-Díaz and Buchberger [182], pages 94-109 (16 pages). [ bib | .pdf ]
[36] Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen. Verification of hybrid systems: Formalization and proof rules in PVS. In Proceedings of the Seventh IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2001), 2001. 10 pages. A preliminary and longer version appeared as technical report TR-ST-01-1. [ bib ]
[37] Erika Ábrahám-Mumm, Ulrich Hannemann, and Martin Steffen. Verification of hybrid systems: Formalization and proof rules in PVS. Technical Report TR-ST-01-1, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, January 2001. [ bib ]
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 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 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.

[38] Eric Bodden, Ka I Pun, Martin Steffen, Volker Stolz, and Anna-Katharina Wickert. Information flow analysis for Go. In Margaria and Steffen [155], pages 431-445. [ bib ]
[39] Dennis Dams, Yassine Lakhnech, and Martin Steffen. Iterating transducers. Journal of Logic and Algebraic Programming, special issue on Model Checking, 52-53:109-127 (19 pages), July 2002. This is an extended version of the conference version under the same title, Computer Aided Verification (CAV'01), LNCS 2102. [ bib | .pdf ]
[40] Dennis Dams, Yassine Lakhnech, and Martin Steffen. Iterating transducers. In Berry et al. [180], pages 286-297 (12 pages). [ bib | .pdf ]
[41] Dennis Dams, Yassine Lakhnech, and Martin Steffen. Iterating transducers for safety of abstraction. Internal Report TR-ST-00-2, Christian-Albrechts-Universität, Lehrstuhl Softwaretechnologie, May 2000. [ bib ]
[42] Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen. Automated test driver generation for Java components. In Netherland's Testing Day “TestDag'08”, Delft, November 2008. White Paper. [ bib | .pdf ]
[43] Frank S. de Boer, Marcello M. Bonsangue, Martin Steffen, and Erika Ábrahám. A fully abstract trace semantics for UML components. In Bonsangue et al. [192], pages 49-69 (21 pages). [ bib | .pdf ]
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.

[44] Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen. Java test driver generation from object-oriented interaction traces. Electronic Notes in Theoretical Computer Science, 243:33-47 (15 pages), July 2009. 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. [ bib | DOI | .pdf ]
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 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 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, 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.

[45] Frank S. de Boer, Mario Bravetti, Immo Grabe, Matias Lee, Martin Steffen, and Gianluigi Zavattaro. A Petri net based analysis of deadlock for active objects and futures. In Pasareanu and Salaün [158], pages 110-127. [ bib | .pdf ]
[46] Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen. Test driver generation from object-oriented interaction traces (extended abstract). In Johnsen et al. [157], pages 52-54. [ bib | .pdf ]
[47] Frank S. de Boer, Immo Grabe, and Martin Steffen. Static deadlock detection for active objects (extended abstract). In ENTCS Proceedings of NWPT'09, September 2009. [ bib | .pdf ]
[48] Frank de Boer, Immo Grabe, and Martin Steffen. Termination detection for active objects. Journal of Logic and Algebraic Programming, 81(4):541-557, May 2012. [ bib | DOI | http ]
[49] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Encapsulating lazy behavioral subtyping. In Specification, Transformation, Navigation. Festschrift dedicated to Bernd Krieg-Brückner on the Occasion of his 60th Birthday, pages 52-67 (16 pages). University Bremen, 2009. [ bib | .pdf ]
[50] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Science of Computer Programming, 76:915-941, 2011. [ bib | DOI | .pdf ]
[51] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Lazy behavioral subtyping. In Cuellar et al. [166], pages 52-67 (16 pages). [ bib | .pdf ]
[52] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Lazy behavioral subtyping. Journal of Logic and Algebraic Programming, 79(7):578-607, April 2010. 30 pages. Article in Press, Preprint available at 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. [ bib | DOI | .pdf ]
[53] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Lazy behavioral subtyping (extended abstract). In Uustalu et al. [156]. Presented at the 20th Nordic Workshop on Programming Theory, NWPT '08, Tallinn. [ bib | .pdf ]
[54] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Lazy behavioral subtyping (revised version). Technical Report 368, University of Oslo, Dept. of Informatics, March 2008. 21 pages. [ bib | .pdf ]
[55] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Lazy behavioral subtyping: Single inheritance and interfaces. Research Report 384, Department of Informatics, University of Oslo, May 2009. 38 pages. Submitted for journal publication. Available at http://einarj.at.ifi.uio.no/rr384.pdf. [ bib ]
[56] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Incremental reasoning for multiple inheritance. In Proceedings of the 7th International Conference on integrated Formal Methods (iFM'09), Düsseldorf, Germany, 16 - 19 February, 2009 [178], pages 215-230. [ bib | .pdf ]
[57] Johan Dovland, Einar Broch Johnsen, Olaf Owe, and Martin Steffen. Incremental reasoning for multiple inheritance. Research Report 373, Department of Informatics, University of Oslo, April 2008. 21 pages. [ bib | .pdf ]
[58] Michael Egner, Uwe Nestmann, and Martin Steffen. Confluent Processes for Transformation Correctness (preliminary version). Interner Bericht IMMD7-1/95, Informatik VII, Universität Erlangen-Nürnberg, January 1995. [ bib ]
Program transformations are central for the correct development of parallel object-based programs in the language πoβλ. A π-calculus translation provides a formal semantics for the π oβλ-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.

[59] Daniel Fava, Martin Steffen, Volker Stolz, and Stian Valle. An operational semantics for a weak memory model with buffered writes, message passing, and goroutines. In Informal proceedings of the PhD Symposium at iFM'17 (integrated Formal Methods), 2017. Submitted for publication. [ bib | .pdf ]
[60] Daniel Fava, Martin Steffen, Volker Stolz, and Stian Valle. An operational semantics for a weak memory model with buffered writes, message passing, and goroutines. Technical Report 466, University of Oslo, Dept. of Informatics, April 2017. [ bib ]
[61] Harald Fecher and Martin Steffen. Characteristic μ-calculus formulas for underspecified transition systems. volume 128. Elsevier Science Publishers, April 2005. Proceedings of the 11th International Workshop on Expressiveness in Concurrency (Express 04), 30 August, 2004, London, Great Britain. 13 pages. [ bib | .pdf ]
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 μ-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 μ-calculus descriptions.

Keywords: underspecification, transition systems, bisimulation, simulation, μ-calculus
[62] Anastasia Gkolfi, Crystal Chang Din, Einar Broch Johnsen, Martin Steffen, and Ingrid Chieh Yu. Translating active objects into colored Petri nets for communication analysis. In Accepted for publication in the LNCS post-proceedings of “Fundamentals of Software Engineering”, FSEN'2017, 2017. [ bib ]
[63] Immo Grabe, Mohammad Mahdi Jaghoori, Bernhard Aichernig, Tobias Blechmann, Frank de Boer, Andreas Griesmayer, Einar Broch Johnsen, Joachim Klein, Sascha Küppelholz, Marcel Kyas, Wolfgang Leister, Rudolf Schlatte, Andries Stam, Martin Steffen, Simon Tschirner, Lian Xuedong, and Wang Yi. Credo methodology. Modeling and analyzing a peer-to-peer system in Credo. In Volker Stolz and Einar Broch Johnsen, editors, Special Issue for the proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software, 2009, Malaysia. Elsevier Science Publishers, 2010. ENTCS Volume 266. 15 pages. [ bib ]
[64] Immo Grabe, Mohammad Mahdi Jaghoori, Bernhard Aichernig, Tobias Blechmann, Frank de Boer, Andreas Griesmayer, Einar Broch Johnsen, Joachim Klein, Sascha Küppelholz, Marcel Kyas, Wolfgang Leister, Rudolf Schlatte, Andries Stam, Martin Steffen, Simon Tschirner, Lian Xuedong, and Wang Yi. Credo methodology (extended version). In Bonsangue et al. [189], pages 41-69. 29 pages. [ bib | DOI ]
[65] Immo Grabe, Marcel Kyas, Martin Steffen, and Arild B. Torjusen. Executable interface specifications for testing asynchronous Creol components. In Arbab and Sirjani [197], pages 324-339 (15 pages). [ bib | .pdf ]
[66] Immo Grabe, Martin Steffen, and Arild Braathen Torjusen. Executable interface specifications for testing asynchronous Creol components. Technical Report 375, University of Oslo, Dept. of Informatics, July 2008. 26 pages. [ bib | .pdf ]
[67] Hallstein A. Hansen, Gerardo Schneider, and Martin Steffen. Reachability analysis of planar autonomous systems. In FSEN'11 [164], pages 206-220. [ bib ]
[68] Hallstein A. Hansen, Gerardo Schneider, and Martin Steffen. Reachability analysis of complex planar hybrid systems. Science of Computer Programming, 78(12):2511-2536, December 2013. 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. [ bib | DOI ]
[69] Hallstein A. Hansen, Gerardo Schneider, and Martin Steffen. Reachability analysis of complex planar autonomous systems. Technical report 412, University of Oslo, Dept. of Informatics, November 2011. [ bib | http ]
[70] Martin Hofmann, Wolfgang Naraschewski, Martin Steffen, and Terry Stroup. Inheritance of proofs. Theory and Practice of Object Systems (Tapos), Special Issue on the Third Workshop on Foundations of Object-Oriented Languages (FOOL 3, LICS and Federated Logic Conferences Workshop), July 1996, 4(1):51-69 (19 pages), January 1998. An extended version appeared as Interner Bericht, Universität Erlangen-Nürnberg, IMMDVII-5/96. [ bib | .ps ]
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 λ-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.

[71] Martin Hofmann, Wolfgang Naraschewski, Martin Steffen, and Terry Stroup. Inheritance of proofs. In Electronic proceedings of the Third Workshop on Foundations of Object-Oriented Languages (FOOL 3), July 1996. An extended version appeared as Interner Bericht, Universität Erlangen-Nürnberg, IMMDVII-5/96, which was published in the special issue of Theory and Practice of Object-Oriented Systems (TAPOS), January 1998. [ bib ]
[72] Martin Hofmann, Wolfgang Naraschewski, Martin Steffen, and Terry Stroup. Inheritance of proofs. Interner Bericht 5/96, Universität Erlangen-Nürnberg, Informatik, IMMDVII, June 1996. 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. [ bib | www: ]
[73] Natalia Ioustinova, Natalia Sidorova, and Martin Steffen. Abstraction and flow analysis for model checking open asynchronous systems. In Proceedings of the 9th Asia-Pacific Software Engineering Conference (APSEC 2002, 4.-6. December 2002, Gold Coast, Queensland, Australia, pages 227-235 (9 pages). IEEE Computer Society, December 2002. [ bib | .pdf ]
[74] Natalia Ioustinova, Natalia Sidorova, and Martin Steffen. Closing open SDL-systems for model checking with DT Spin. In Eriksson and Lindsay [184], pages 531-548 (18 pages). [ bib | .pdf ]
[75] Natalia Ioustinova, Natalia Sidorova, and Martin Steffen. Synchronous closing and flow analysis for model checking timed systems. In Bonsangue et al. [191], pages 292-313 (22 pages). [ bib | DOI | .pdf ]
[76] Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudi Schlatte, and Martin Steffen. ABS: A core language for abstract behavioral specification. In Aichernig et al. [188], pages 142-164. [ bib ]
[77] Einar Broch Johnsen, Ka I Pun, Martin Steffen, Silvia Lizeth, Martin Steffen, and Ingrid Chieh Yu. Meeting deadlines, elastically. In Luigia Petre and Emil Sekerinski, editors, From Action Systems to Distributed System: The Refinement Approach, pages 99-111. CRC press, 2016. [ bib | .pdf ]
[78] Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen. Safe locking for multi-threaded Java. In FSEN'11 [164], pages 158-173. [ bib ]
[79] Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen. Safe locking for multi-threaded Java with exceptions. Journal of Logic and Algebraic Programming, special issue of selected contributions to NWPT'10, March 2012. Available online 3. March 2012. [ bib | DOI | http ]
[80] Einar Broch Johnsen, Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen. Safe locking for multi-threaded Java. Technical Report (revised version) 402, University of Oslo, Dept. of Informatics, January 2011. www.ifi.uio.no/~msteffen/publications.html#techreports. [ bib ]
[81] Einar Broch Johnsen, Martin Steffen, and Johanna Beate Stumpf. A calculus of virtually timed ambients (extended abstract). In NWPT'16 [175]. [ bib | .pdf ]
[82] Einar Broch Johnsen, Martin Steffen, and Johanna Beate Stumpf. A calculus of virtually timed ambients (extended abstract). In Informal Proceedings of the 23rd International Workshop on Algebraic Development Techniques (WADT 2016), September 2016. [ bib | .pdf ]
[83] Einar Broch Johnsen, Martin Steffen, and Johanna Beate Stumpf. A calculus of virtually timed ambients. In To appear in the Post-Proceedings of selected contributions to the 23rd International Workshop on Algebraic Development Techniques (WADT 2016), 2017. [ bib | .pdf ]
[84] Einar Broch Johnsen, Martin Steffen, and Johanna Beate Stumpf. Virtually timed ambients: A calculus of nested virtualization. Journal of Logic and Algebraic Methods in Programming, 2017. Submitted for Publication in the Journal of Logic and Algebraic Methods in Programming (JLAMP). Special Issue on Selected Contributions of NWPT'16. [ bib ]
[85] Einar Broch Johnsen, Martin Steffen, and Johanna Beate Stumpf. A type system with assumptions, commitments and coeffects for virtually timed ambients. In Under Preparation, June 2017. [ bib ]
[86] Marcel Kyas, Andries Stam, Martin Steffen, and Arild Braathen Torjusen. A specification-driven interpreter for testing asynchronous Creol components (extended abstract). In Uustalu et al. [156]. Presented at the 20th Nordic Workshop on Programming Theory, NWPT'08, Tallinn. [ bib | .pdf ]
[87] Erika Ábrahám, Andreas Grüner, and Martin Steffen. An open structural operational semantics for an object-oriented calculus with thread classes. Technical Report 0505, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, May 2005. [ bib | .html ]
In this report we present a multithreaded class-calculus featuring 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 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 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.
[88] Jingyue Li, Altin Qeriqi, and Martin Steffen Ingrid Chieh Yu. Automatic translation of FBD-PLC-programs to NuSMV for model checking safety-critical control systems. In Proceedings of the Norsk Informatikkonferanse NIK'16, 2016. [ bib ]
[89] Bjørnar Luteberget, Christian Johansen, Claus Feyling, and Martin Steffen. Rule-based incremental verification tools applied to railway designs and regulations. In Fitzgerald et al. [177], pages 772-778. [ bib | DOI ]
[90] Bjørnar Luteberget, Christian Johansen, and Martin Steffen. Rule-based consistency checking of railway infrastructure designs. In Ábrahám and Huisman [154], pages 491-507. Best Paper Award for iFM 2016. See also the UiO IFI research report Nr. 450 with the same title. [ bib ]
[91] Bjørnar Luteberget, Christian Johansen, and Martin Steffen. Rule-based consistency checking of railway infrastructure designs. Technical report 450, University of Oslo, Dept. of Informatics, January 2016. A shorter version has been submitted for inclusion in conference proceedings. [ bib | .pdf ]
[92] Thi Mai Thuong Tran, Olaf Owe, and Martin Steffen. Safe typing for transactional vs. lock-based concurrency in multi-threaded Java. In Son Bao Pham, Tuan-Hao Hoang, Bob McKay, and Kaoru Hirota, editors, Proceedings of the Second International Conference on Knowledge and Systems Engineering, KSE 2010, pages 188 - 193. IEEE Computer Society, October 2010. [ bib | http ]
[93] Thi Mai Thuong Tran and Martin Steffen. Design issues in concurrent object-oriented languages and observability. In Proceedings of the Third International Conference on Knowledge and Systems Engineering (KSE 2011), Hanoi 14th-17th Oct, 2011, pages 135-142. IEEE Computer Society CPS, June 2011. [ bib ]
[94] Thi Mai Thuong Tran and Martin Steffen. Specification and verification. In Eternal Task Force 2: Time Awareness and Management. State-of-the-Art Report, January 2011. [ bib ]
[95] Thi Mai Thuong Tran and Martin Steffen. Safe commits for Transactional Featherweight Java. In Méry and Merz [152], pages 290-304. An earlier and longer version has appeared as UiO, Dept. of Informatics Technical Report 392, Oct. 2009. [ bib ]
[96] Uwe Nestmann, Martin Steffen, and Terry Stroup. Formale Semantik für asynchronen Methodenaufruf. In Gotzhein and Bredereke [162], pages 169-178 (10 pages). Available as Universität-Nürnberg Erlangen, IMMD7, Interner Bericht TR-I7-95-11. [ bib ]
Das Methodenaufrufschema wait-by-necessity zum Verbergen expliziter Parallelität hinter asynchronen Wertzuweisungen wird exemplarisch durch eine Strukturelle Operationelle Semantik (SOS) formalisiert. Diese Spezifikation repräsentiert ein eindeutiges Referenzmodell und wurde darüberhinaus mittels einer semantisch korrekten Übersetzung in den π-Kalkül in eine prototypische Implementierung überführt. Sie dienen neben der Validierung der Intuition des Programmiersprach-Ingenieurs auch als Basis für den Entwurf korrekter Compiler sowie zum Testen von Beispielprogrammen. Das vorliegende Papier konzentriert sich auf die Darstellung der SOS-Variante

[97] Uwe Nestmann, Martin Steffen, and Terry Stroup. Formale Semantik für asynchronen Methodenaufruf. Interner Bericht TR-I7-95-11, Universität Erlangen-Nürnberg, IMMD VII, May 1995. [ bib ]
[98] Uwe Nestmann and Martin Steffen. Kalkübasierte OO-Sprachen. Technical Report IMMD7-02/94, Universität Erlangen-Nürnberg, Informatik, IMMDVII, 1994. [ bib ]
[99] Olaf Owe, Gerardo Schneider, and Martin Steffen. Components, objects, and contracts. In Sixth International Workshop on Specification and Verification of Component-Based Systems, Sept. 3-4, 2007, Cavtat, Croatia, pages 95-98, August 2007. [ bib | .pdf ]
[100] Olaf Owe, Gerardo Schneider, and Martin Steffen. Components, objects, and contracts. Research Report 363, University of Oslo, Dept. of Informatics, August 2007. 18 pages. A short version appeared in the proceedings of SAVCBS'07. [ bib | .pdf ]
[101] Olaf Owe, Martin Steffen, and Arild Torjusen. Model testing asynchronously communicating objects using modulo AC rewriting. In Proceedings of the 6th Workshop on Model-Based Testing MBT'10 (ETAPS Satellite Workshop), pages 68-84. Elsevier Science Publishers, March 2010. Electronic Notes in Theoretical Computer Science ENTCS, Volume 264, Issue 3. [ bib ]
[102] Olaf Owe, Martin Steffen, and Arild Torjusen. Model testing asynchronously communicating objects using modulo AC rewriting (extended abstract). In Proceedings of NWPT'09, September 2009. [ bib | .pdf ]
[103] Benjamin C. Pierce and Martin Steffen. Higher-order subtyping. Theoretical Computer Science, 176(1,2):235-282 (48 pages), 1997. 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ät Erlangen. [ bib ]
[104] Ka I Pun, Martin Steffen, Volker Stolz, Anna-Katharina Wickert, Eric Bodden, and Michael Eichberg. Don't let data Go astray: A context-sensitive taint analysis for concurrent programs in Go (extended abstract). In NWPT'16 [175]. [ bib ]
[105] Ka I Pun, Martin Steffen, and Volker Stolz. Behaviour inference for deadlock checking. In Proceeding of the 8th International Symposium on Theoretical Aspects of Software Engineering (TASE'14), pages 106-113. IEEE, 2014. [ bib | .pdf ]
[106] Ka I Pun, Martin Steffen, and Volker Stolz. Behaviour inference for deadlock checking. Technical report 416, University of Oslo, Dept. of Informatics, July 2012. [ bib | .pdf ]
[107] Ka I Pun, Martin Steffen, and Volker Stolz. Deadlock checking by a behavioral effect system for lock handling. Journal of Logic and Algebraic Programming, 81(3):331-354, March 2012. A preliminary version was published as University of Oslo, Dept. of Computer Science Technical Report 404, March 2011. [ bib ]
[108] Ka I Pun, Martin Steffen, and Volker Stolz. Deadlock checking by a behavioral effect system for lock handling. Technical report 404, University of Oslo, Dept. of Informatics, March 2011. [ bib ]
[109] Ka I Pun, Martin Steffen, and Volker Stolz. Deadlock checking by data race detection. Journal of Logic and Algebraic Methods in Programming, March 2014. 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. [ bib | .pdf ]
[110] Ka I Pun, Martin Steffen, and Volker Stolz. Deadlock checking by data race detection. In FSEN'13 [165], pages 34-50. [ bib | .pdf ]
[111] Ka I Pun, Martin Steffen, and Volker Stolz. Deadlock checking by data race detection. In NWPT'12 [174]. [ bib | .pdf ]
[112] Ka I Pun, Martin Steffen, and Volker Stolz. Deadlock checking by data race detection. Technical report 421, University of Oslo, Dept. of Informatics, October 2012. [ bib | .pdf ]
[113] Ka I Pun, Martin Steffen, and Volker Stolz. Effect-polymorphic behaviour inference for deadlock checking. In Giannakopoulou and Salaün [150], pages 50-64. A longer version is available (under the titleLock-Polymorphic Behaviour Inference for Deadlock Checking”) as UiO, Dept. of Informatics Technical Report 436, Sep. 2013. [ bib ]
[114] Ka I Pun, Martin Steffen, and Volker Stolz. Effect-polymorphic behaviour inference for deadlock checking. Journal of Logic and Algebraic Methods in Programming, 85(6), October 2016. A longer version is available (under the titleLock-Polymorphic Behaviour Inference for Deadlock Checking”) as UiO, Dept. of Informatics Technical Report 436, Sep. 2013. [ bib | DOI | .pdf ]
[115] Ka I Pun, Martin Steffen, and Volker Stolz. Lock-polymorphic behaviour inference for deadlock checking (extended abstract). In Proceedings of NWPT'13, November 2013. Available electronically at 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. [ bib | .pdf ]
[116] Ka I Pun, Martin Steffen, and Volker Stolz. Lock-polymorphic behaviour inference for deadlock checking. Technical report 436, University of Oslo, Dept. of Informatics, September 2013. Available electronically at http://www.ifi.uio.no/~msteffen/download/13/lockpolymorphic-rep.pdf. Submitted to journal publication. [ bib | .pdf ]
[117] Ka I Pun, Martin Steffen, and Volker Stolz. Polymorphic behavioural lock effects for deadlock checking (extended abstract). In NWPT'11 [173], pages 48-50. [ bib | .pdf ]
[118] Ka I Pun and Martin Steffen. Deadlock checking by behavior inference for lock handling (extended abstract). In Proceedings of the 22nd Nordic Workshop on Programming Theory (NWPT'10), volume 57 of TUCS General Publication, pages 8-9. Turku Centre for Comuter Science, November 2010. [ bib ]
[119] Carl Martin Rosenberg, Martin Steffen, and Volker Stolz. Leveraging DTrace for runtime verification. In Sánchez [171], pages 318-332. [ bib | .pdf ]
[120] Erich Mikk and Martin Steffen. Javaprojekt: “Programming environment for Statecharts”. Included in the proceedings of the “7. Deutschen Anwenderforum für Statemate MAGNUM”, 26.-27. April, 1999, 1999. [ bib ]
[121] Natalia Sidorova and Martin Steffen. Verification of a wireless ATM medium-access protocol. In Proceedings of the 7th Asia-Pacific Software Engineering Conference (APSEC 2000), 5.-8. December 2000, Singapore, pages 84-91 (8 pages). IEEE Computer Society, 2000. A preliminary and longer version appeared as Universität Kiel technical report TR-ST-00-3. [ bib ]
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
[122] Natalia Sidorova and Martin Steffen. Verification of a wireless ATM medium-access protocol. Technical Report TR-ST-00-3, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, May 2000. 22 pages. [ bib | .ps ]
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.

[123] Natalia Sidorova and Martin Steffen. Embedding chaos. In Cousot [181], pages 319-334 (15 pages). [ bib | .pdf ]
[124] Natalia Sidorova and Martin Steffen. Verifying Mascara Control. Technical Report TR-ST-00-1, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, May 2000. 40 pages. [ bib | .ps.gz ]
This document reports on a series of verification experiments on the control-part of Mascara, a medium-access protocol for wireless ATM-networks.

[125] Natalia Sidorova and Martin Steffen. Synchronous closing of timed SDL systems for model checking. In Cortesi [183], pages 79-93 (15 pages). [ bib | .pdf ]
[126] Natalia Sidorova and Martin Steffen. Verifying large SDL-specifications using model checking. In Reed and Reed [179], pages 403-416 (14 pages). [ bib ]
[127] Michael Siegel and Martin Steffen. Vollständigkeit eines Beweissystems für Hennessy-Milner-Logik mit Rekursion. Diplomarbeit, Friedrich-Alexander-Universität, Erlangen-Nürnberg, 1992. 71 pages. [ bib | .ps ]
[128] Michael Siegel and Martin Steffen. Ein Beweissystem für Hennessy-Milner-Logik mit Rekursion. Studienarbeit, Friedrich-Alexander-Universität, Erlangen-Nürnberg, 1991. 61 pages. [ bib | .ps ]
Als ausdrucksstarke temporale Logik wird seit einigen Jahren verstärkt Hennessy-Milner-Logik mit Rekursion zur Spezifikation verteilter Systeme untersucht. Eine wichtige Frage in diesem Zusammenhang stellt die formale Verifizierbarkeit dar, das heißt, die Frage nach einem Beweissystem. Wir stellen in unserer Arbeit ein Gentzen-System für Hennessy-Milner-Logik mit Rekursion vor. Damit läßt sich zielgerichtet die semantische Implikation zwischen Formeln der Logik beweisen. Besondere Schwierigkeiten bereiten dabei beliebig geschachtelte Fixpunkte, welche gerade die Ausdrucksstärke dieser Logik ausmachen. Aufbauend auf einer Klasse von Algorithmen, die überprüfen, ob ein Prozeß, modelliert durch ein Transitionssystem, die Spezifikation erfüllt (sogenannte 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ährend Model-Checking im wesentlichen ein Ein-Schritt-Verfahren der Verifikation darstellt, kann man das Gentzen-System für die semantische Implikation für die schrittweise Verfeinerung und Verifikation benutzen.

[129] Karsten Stahl, Kai Baukus, Yassine Lakhnech, and Martin Steffen. Divide, abstract, and model-check. In Dams et al. [167], pages 57-76 (20 pages). [ bib ]
[130] Martin Steffen and Benjamin C. Pierce. Higher-order subtyping. Interner Bericht IMMD7-01/94, Informatik VII, Universität Erlangen-Nürnberg, January 1994. Also as Edinburgh LFCS technical report ECS-LFCS-94-280. [ bib | .ps ]
[131] Martin Steffen and Benjamin C. Pierce. Higher-order subtyping. In Olderog [172], pages 511-530 (20 pages). Full version in Theoretical Computer Science, vol. 176, no. 1-2, pp. 235-282, 1997. [ bib ]
[132] Martin Steffen and Michael Siegel. Validity in the propositional μ-calculus. In UGoltz and WReisig, editors, Workshop: Logics for Distributed Systems, GMD-Studien Nr. 214. GMD, Gesellschaft für Mathematik und Datenverarbeitung, 1992. [ bib ]
[133] Martin Steffen and Thi Mai Thuong Tran. The stock quoter case study. Internal Document, March 2009. [ bib ]
[134] Martin Steffen and Thi Mai Thuong Tran. Safe commits for Transactional Featherweight Java (extended abstract). In Proceedings of the Nordic Workshop on Programming Theory, NWPT'09, October 2009. [ bib | .pdf ]
[135] Martin Steffen and Thi Mai Thuong Tran. Safe commits for Transactional Featherweight Java. Technical Report 392, University of Oslo, Dept. of Informatics, October 2009. 23 pages. [ bib ]
[136] Martin Steffen. Object-Connectivity and Observability for Class-Based, Object-Oriented Languages. Habilitation thesis, Technische Faktultät der Christian-Albrechts-Universität zu Kiel, July 2006. 281 pages. [ bib ]
[137] Martin Steffen. Polarized Higher-Order Subtyping. PhD thesis, Technische Fakultät, Friedrich-Alexander-Universität Erlangen-Nürnberg, 1998. 260 pages. [ bib | .pdf ]
The calculus of higher-order subtyping, known as F_<=^ω, a higher-order polymorphic λ-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 [?], Cardelli presents F_<=^ω 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<= U_2 and T is a monotone operator. My thesis extends F_<=^ω by polarized application, it explores its proof theory, establishing decidability of polarized F_<=^ω. The inclusion of polarized application rules leads to an interdependence of the subtyping and the kinding system. This contrasts with pure F_<=^ω, 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.

[138] Martin Steffen. Polarized higher-order subtyping (extended abstract). In Luo and Soloviev [176]. 12 pages. [ bib | .ps.gz ]
[139] Martin Steffen. A small-step semantics of a concurrent calculus with goroutines and deferred functions. In Ábrahám et al. [153], pages 393-406. [ bib | .pdf ]
Keywords: semantics, Go, deferred function
[140] Johanna Beate Stumpf, Einar Broch Johnsen, and Martin Steffen. Virtually timed ambients: Formalization and analysis (extended abstract). In Informal proceedings of the PhD Symposium at iFM'17 (integrated Formal Methods), June 2017. Submitted for presentation. [ bib | .pdf ]
[141] Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong. Compositional static analysis for implicit join synchronization in a transactional setting. In Eleftherakis et al. [151], pages 212-228. [ bib | .pdf ]
[142] Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong. Compositional static analysis for implicit join synchronization in a transactional setting. September 2014. Submitted for journal publication, as extended version of the accepted SEFM conference contribution. [ bib ]
[143] Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong. Compositional analysis of resource bounds for software transactions. In NWPT'12 [174]. [ bib | .pdf ]
[144] Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong. Estimating resource bounds for software transactions. Technical report 414, University of Oslo, Dept. of Informatics, December 2011. [ bib | http ]
[145] Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong. Estimating resource bounds for software transactions (extended abstract). In NWPT'11 [173], pages 77-79. [ bib | .pdf ]
[146] Claus Traulsen and Martin Steffen. Using constraints for model checking buffered systems (extended abstract). In Informal Proceeding of the 17th Nordic Workshop on Programming Theory, September 2005. [ bib | .pdf ]
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
[147] Tung Vu Xuan, Hoang Truong Anh, Thi Mai Thuong Tran, and Martin Steffen. A type system for finding upper resource bounds of multi-threaded programs with nested transactions. In ACM Proceedings of the 3rd ACM International Symposium on Information and Communication Technology SoICT, pages 20-31. ACM, August 2012. [ bib | DOI ]
[148] Uwe Nestmann and Martin Steffen. Correct transformational design of concurrent search structures. In Freitag et al. [161], pages 23-42 (20 pages). [ bib ]
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 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.

[149] Uwe Nestmann and Martin Steffen. Typing confluence. In Gnesi and Latella [160], pages 77-101 (25 pages). Also available as report ERCIM-10/97-R052, European Research Consortium for Informatics and Mathematics, 1997. [ bib | .html ]
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.

[150] Dimitra Giannakopoulou and Gwen Salaün, editors. Proceedings of SEFM'14, volume 8702 of Lecture Notes in Computer Science. Springer Verlag, September 2014. [ bib ]
[151] George Eleftherakis, Mike Hinchey, and Mike Holcombe, editors. Proceedings of SEFM'13, volume 8137 of Lecture Notes in Computer Science. Springer Verlag, 2013. [ bib ]
[152] Dominique Méry and Stephan Merz, editors. Proceedings of the 8th International Conference on Integrated Formal Methods (iFM 2010), volume 6396 of Lecture Notes in Computer Science. Springer Verlag, October 2010. [ bib ]
[153] Erika Ábrahám, Marieke Huisman, and Einar Broch Johnsen, editors. Theory and Practice of Formal Methods. Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (Festschrift), volume 9660 of Lecture Notes in Computer Science. Springer Verlag, 2016. [ bib ]
[154] Erika Ábrahám and Marieke Huisman, editors. Proc. of the 12th International Conference on integrated Formal Methods (iFM 2010), volume 9681 of Lecture Notes in Computer Science. Springer Verlag, 2016. [ bib ]
[155] Tiziana Margaria and Bernhard Steffen, editors. 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'16), volume 9952 of Lecture Notes in Computer Science. Springer Verlag, October 2016. [ bib ]
[156] Tarmu Uustalu, Jüri Vain, and Juhan Ernits, editors. Proceedings of the Nordic Workshop of Programming Theory '08 (Abstracts), Tallinn, 2008. Institute of Cybernetics at TUT, Tallinn, Technical Report. [ bib ]
[157] Einar B. Johnsen, Olaf Owe, and Gerardo Schneider, editors. Proceedings of the 19th Nordic Workshop on Programming Theory (NWPT'07). Extended Abstracts. University of Oslo, Dept. of Computer Science, Technical Report 366, October 2007. [ bib ]
[158] Corina S. Pasareanu and Gwen Salaün, editors. Revised Selected Papers of the 9th International Workshop on Formal Aspects of Component Software (FACS 2012), Lecture Notes in Computer Science. Springer Verlag, 2013. [ bib ]
[159] Dennis Dams, Ulrich Hannemann, and Martin Steffen, editors. Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever, number 5930 in Lecture Notes in Computer Science. Springer Verlag, 2010. 377 pages. [ bib | http ]
[160] Stefania Gnesi and Diego Latella, editors. Second International ERCIM Workshop on Formal Methods in Industrial Critical Systems (Cesena, Italy, July 4-5, 1997). Consiglio Nazionale Ricerche di Pisa, 1997. [ bib ]
[161] Burkhard Freitag, Clifford Jones, Christian Lengauer, and Hans-Jörg Schek, editors. Object-Orientation with Parallelism and Persistence. Now: The Springer International Series in Engineering and Computer Science (Hardcover). Kluwer Academic Publishers, 1996. [ bib ]
[162] Reinhard Gotzhein and Jan Bredereke, editors. Formale Beschreibungstechniken für verteilte Systeme. Universität Kaiserslautern, Fachbereich Informatik, 22./23. Juni 1995. [ bib | http ]
[163] Farhad Arbab and Marjan Sirjani, editors. FSEN '05: IPM International Conference on Foundations of Software Engineering (Theory and Practice). Oct. 1 - 3, 2005, volume 159 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, May 2005. [ bib | DOI ]
[164] Proceedings of the International Conference on Foundations of Software Engineering (Theory and Practice) (FSEN'11), volume 7141 of Lecture Notes in Computer Science. Springer Verlag, 2012. [ bib ]
[165] Proceedings of the International Conference on Foundations of Software Engineering (Theory and Practice) (FSEN'13), volume 8161 of Lecture Notes in Computer Science. Springer Verlag, 2013. [ bib ]
[166] Jorge Cuellar, Tom Maibaum, and Kaisa Sere, editors. Proceedings of the 15th International Symposium on Formal Methods (FM'08), volume 5014 of Lecture Notes in Computer Science. Springer Verlag, 2008. [ bib ]
[167] Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink, editors. Theoretical and Practical Aspects of SPIN Model Checking, Proceedings of 5th and 6th International SPIN Workshops, Trento/Toulouse, volume 1680 of Lecture Notes in Computer Science. Springer Verlag, 1999. [ bib ]
[168] Olaf Owe, Martin Steffen, and Jan Arne Telle, editors. Information and Computation: Special issue with selected publications of FCT '11u, volume 231. Elsevier, October 2013. [ bib ]
[169] Olaf Owe, Martin Steffen, and Jan Arne Telle, editors. Proceedings of FCT '11, volume 6914 of Lecture Notes in Computer Science. Springer Verlag, 2011. [ bib ]
[170] Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors. Proceedings of Logical Approaches to Computational Barriers: Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006., volume 3988 of Lecture Notes in Computer Science. Springer Verlag, July 2006. [ bib | DOI ]
[171] César Sánchez, editor. Proceedings of the 16th International Conference on Runtime Verification, RV 2016, Madrid, Spain, September 23-30, 2016, volume 10012 of Lecture Notes in Computer Science. Springer Verlag, September 2016. [ bib ]
[172] Ernst-Rüdiger Olderog, editor. Working Conference on Programming Concepts, Methods and Calculi, San Miniato, Italy. IFIP, North-Holland, June 1994. [ bib ]
[173] Proceedings of the 23nd Nordic Workshop on Programming Theory (NWPT'11), volume 254/2011. Mälardalen Real-time Research Centre, Mälardalen University, October 2011. [ bib ]
[174] Proceedings of the 24nd Nordic Workshop on Programming Theory (NWPT'12). Dept. of Informatics, University of Bergen, Report Nr. 403, October 2012. [ bib ]
[175] Proceedings of the 28nd Nordic Workshop on Programming Theory (NWPT'16), 2016. [ bib ]
[176] Zhaohui Luo and Sergei Soloviev, editors. Electronic Proceedings of the Types working group Workshop on Subtyping, inheritance and modular development of proofs, August 1997. [ bib ]
[177] JFitzgerald, CHeitmeyer C, SGnesi, APhilippou, Michael Butler, and Wolfram Schulte, editors. Proceedings of the International Symposium on Formal Methods (FM 2016), volume 9995 of Lecture Notes in Computer Science. Springer Verlag, 2016. [ bib ]
[178] Proceedings of the 7th International Conference on integrated Formal Methods (iFM'09), Düsseldorf, Germany, 16 - 19 February, 2009, volume 5423 of Lecture Notes in Computer Science. Springer Verlag, February 2009. [ bib ]
[179] Rick Reed and Jeanne Reed, editors. Proceedings of the 10th International SDL Forum SDL 2001: Meeting UML, volume 2078 of Lecture Notes in Computer Science. Springer Verlag, 2001. [ bib ]
[180] Gérard Berry, Hubert Comon, and Alain Finkel, editors. Proceedings of the 13th International Conference on Computer-Aided Verification, Paris, France, volume 2102 of Lecture Notes in Computer Science. Springer Verlag, 2001. [ bib ]
[181] Patrick Cousot, editor. SAS'01: 8th International Static Analysis Symposium (Paris, France), volume 2126 of Lecture Notes in Computer Science. Springer Verlag, 2001. [ bib ]
[182] Roberto Moreno-Díaz and Bruno Buchberger, editors. 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., volume 2178 of Lecture Notes in Computer Science. Springer Verlag, 2001. [ bib ]
[183] Agostino Cortesi, editor. Proceedings of the 3rd International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI) 2002, volume 2294 of Lecture Notes in Computer Science. Springer Verlag, 2002. [ bib ]
[184] Lars-Henrik Eriksson and Peter A. Lindsay, editors. Proceedings of Formal Methods Europe: Formal Methods - Getting IT Right (FME'02), volume 2391 of Lecture Notes in Computer Science. Springer Verlag, 2002. [ bib ]
[185] Mogens Nielsen and Uffe H. Engberg, editors. 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), volume 2303 of Lecture Notes in Computer Science. Springer Verlag, April 2002. [ bib ]
[186] Nachum Derschowitz, editor. Proceedings of the International Symposium on Verification (Theory and Practice), Celebrating Zohar Manna's 64th Birthday, Taormina, Sicily, June 29-July 4, 2003, volume 2772 of Lecture Notes in Computer Science. Springer Verlag, 2004. [ bib ]
[187] Marcello M. Bonsangue, Frank S. de Boer, Willem-Paul de Roever, and Susanne Graf, editors. Proceedings of the First International Symposium on Formal Methods for Components and Objects (FMCO 2002), Leiden, volume 2852 of Lecture Notes in Computer Science. Springer Verlag, 2003. [ bib ]
[188] B.K. Aichernig, F.S. de Boer, and M.M. Bonsangue, editors. Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010, Selected Papers, volume 6957 of Lecture Notes in Computer Science. Springer Verlag, 2011. [ bib ]
[189] Marcello M. Bonsangue, Frank S. de Boer, Stefan Hallerstede, and Michael Leuschel, editors. Proceedings of the 8th International Symposium on Formal Methods for Components and Objects, FMCO 2009, Selected Papers, volume 6286 of Lecture Notes in Computer Science. Springer Verlag, 2009. [ bib ]
[190] Radhia Cousot, editor. Proceedings of the 6th International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI 2005), January 17-19, 2005, volume 3385 of Lecture Notes in Computer Science. Springer Verlag, 2005. [ bib ]
[191] Marcello Bonsangue, Frank S. de Boer, Willem-Paul de Roever, and Susanne Graf, editors. Proceedings of the Second International Symposium on Formal Methods for Components and Objects (FMCO 2003), volume 3188 of Lecture Notes in Computer Science. Springer Verlag, 2004. [ bib ]
[192] Marcello Bonsangue, Frank S. de Boer, Willem-Paul de Roever, and Susanne Graf, editors. Proceedings of the Third International Symposium on Formal Methods for Components and Objects (FMCO 2004), volume 3657 of Lecture Notes in Computer Science. Springer Verlag, 2005. [ bib ]
[193] Martin Steffen and Gianluigi Zavattaro, editors. Proceedings of the 7th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '05), Athens, Greece, volume 3535 of Lecture Notes in Computer Science. Springer Verlag, 2005. [ bib ]
[194] Roberto Gorrieri and Heike Wehrheim, editors. Proceedings of the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '06), Bologna, Italy, volume 4037 of Lecture Notes in Computer Science. Springer Verlag, 2006. [ bib ]
[195] Elie Najm, Uwe Nestmann, and Perdita Stevens, editors. Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS '03), Paris, volume 2884 of Lecture Notes in Computer Science. Springer Verlag, November 2003. [ bib ]
[196] Proceedings of the International Colloquium on Theoretical Aspects of Computing, ICTAC 2004, volume 3407 of Lecture Notes in Computer Science. Springer Verlag, 2004. [ bib ]
[197] Farhad Arbab and Marjan Sirjani, editors. Fundamentals of Software Engineering, Third IPM International Conference, FSEN 2009, Kish Island, Iran, April 15-17, 2009, Revised Selected Papers, volume 5961 of Lecture Notes in Computer Science. Springer, 2010. [ bib ]

This file was generated by bibtex2html 1.97.