Publications of Arend Rensink

Object-orientation

• Model checking dynamic states in GROOVE (with Harmen Kastenberg). In A. Valmari, editor, Model Checking Software (SPIN), volume 3925 of Lecture Notes in Computer Science, pages 299-305. Springer-Verlag, 2006. (PDF, BibTeX)
• Engineering object-oriented semantics using graph transformations (with Harmen Kastenberg and Anneke Kleppe). CTIT Technical Report TR-CTIT-06-12, Department of Computer Science, University of Twente, March 2006. (PDF, BibTeX)
• Ensuring structural constraints in graph-based models with type inheritance (with Gabriele Taentzer). In M. Cerioli, editor, Fundamental Approaches to Software Engineering (FASE), volume 3442 of Lecture Notes in Computer Science, pages 64-79. Springer-Verlag, 2005. (PDF, BibTeX)
• Formal Methods for Open Object-Based Distributed Systems V (with Bart Jacobs, editors). Kluwer Academic Publishers, 2002. (BibTeX)
• Visualisatie van het objectgeoriënteerde paragdigma. TINFON --- Tijdschrift voor Informatica-Onderwijs, 11(2):80-83, 2002. NIOC 2002 special issue (in dutch). (PDF, BibTeX)
• Formal foundations for reasoning about composition (with Maurice Glandrup). Position paper at the OOPSLA 2001 Advanced Separation of Concerns Workshop, 2001. (PDF, BibTeX)
• On a temporal logic for object-based systems (with Dino Distefano and Joost-Pieter Katoen). CTIT Technical Report TR-CTIT-00-06, Faculty of Informatics, University of Twente, March 2000. (PDF, BibTeX)
• On a temporal logic for object-based systems (with Dino Distefano and Joost-Pieter Katoen). In S. F. Smith and C. L. Talcott, editors, Formal Methods for Open Object-based Distributed Systems, pages 305-326. Kluwer Academic Publishers, 2000. Report version: TR-CTIT-00-06, Faculty of Informatics, University of Twente. (PostScript, BibTeX)
• Towards model checking OCL (with Dino Distefano and Joost-Pieter Katoen). In Defining Precise Semantics for UML (satellite workshop of ECOOP 2000), 2000. Position paper. (PostScript, BibTeX)
• YOO (Why Object-Orientation). CTIT Technical Report TR-CTIT-00-12, Faculty of Informatics, University of Twente, September 2000. Report of a satellite workshop of Concur 2000. (PostScript, PDF, BibTeX)
• A typed functional calculus with state. In M. Müllhäuser, editor, Special Issues in Object-Oriented Programming. dpunkt.verlag, March 1997. (PostScript, BibTeX)

Graphs, graph transformations and model checking

• Safety and liveness in concurrent pointer programs (with Dino Distefano and Joost-Pieter Katoen). In Fourth International Symposium on Formal Methods for Components and Objects, Lecture Notes in Computer Science. Springer-Verlag, 2006. To be published. (BibTeX)
• Model checking dynamic states in GROOVE (with Harmen Kastenberg). In A. Valmari, editor, Model Checking Software (SPIN), volume 3925 of Lecture Notes in Computer Science, pages 299-305. Springer-Verlag, 2006. (PDF, BibTeX)
• Defining object-oriented execution semantics using graph transformations (with Harmen Kastenberg and Anneke Kleppe). In R. Gorrieri and H. Wehrheim, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS), volume 4037 of Lecture Notes in Computer Science, pages 186-201. Springer-Verlag, 2006. (PDF, BibTeX)
• Engineering object-oriented semantics using graph transformations (with Harmen Kastenberg and Anneke Kleppe). CTIT Technical Report TR-CTIT-06-12, Department of Computer Science, University of Twente, March 2006. (PDF, BibTeX)
• Graph transformation semantics for a QVT language (with Ronald Nederpel). In International Workshop on Graph Transformation and Visual Modeling Techniques, Electronic Notes in Theoretical Computer Science, 2006. To appear. (PDF, BibTeX)
• Summary 2: Graph grammar verification through abstraction (with Paolo Baldan and Barbara Koenig). In B. Koenig, U. Montanari and Ph. Gardner, editors, Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, number 04241 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany, 2005. (BibTeX)
• Graph Transformation for Verification and Concurrency (with Reiko Heckel and Barbara König, editors). CTIT Technical Report TR-CTIT-05-34. Department of Computer Science, University of Twente, August 2005. Workshop proceedings. (PDF, BibTeX)
• The joys of graph transformation. Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica, 9, 2005. (PDF, BibTeX)
• Time and space issues in the generation of graph transition systems. In International Workshop on Graph-Based Tools (GraBaTs), volume 127 of Electronic Notes in Theoretical Computer Science, pages 127-139. Elsevier Science Publishers, 2005. (PDF, BibTeX)
• Abstract graph transformation (with Dino Distefano). CTIT Technical Report TR-CTIT-05-04, Department of Computer Science, University of Twente, January 2005. (PDF, BibTeX)
• Abstract graph transformation (with Dino Distefano). In International Workshop on Software Verification and Validation (SVV), Electronic Notes in Theoretical Computer Science, 2005. To appear. Technical report version: CTIT TR-CTIT-05-04, University of Twente. (PDF, BibTeX)
• Ensuring structural constraints in graph-based models with type inheritance (with Gabriele Taentzer). In M. Cerioli, editor, Fundamental Approaches to Software Engineering (FASE), volume 3442 of Lecture Notes in Computer Science, pages 64-79. Springer-Verlag, 2005. (PDF, BibTeX)
• Canonical graph shapes. In D. A. Schmidt, editor, Programming Languages and Systems --- European Symposium on Programming (ESOP), volume 2986 of Lecture Notes in Computer Science, pages 401-415. Springer-Verlag, 2004. (PDF, BibTeX)
• The GROOVE simulator: A tool for state space generation. In J. Pfalz, M. Nagl and B. Böhlen, editors, Applications of Graph Transformations with Industrial Relevance (AGTIVE), volume 3062 of Lecture Notes in Computer Science, pages 479-485. Springer-Verlag, 2004. (PDF, BibTeX)
• Representing first-order logic using graphs. In H. Ehrig, G. Engels, F. Parisi-Presicce and G. Rozenberg, editors, International Conference on Graph Transformations (ICGT), volume 3256 of Lecture Notes in Computer Science, pages 319-335. Springer-Verlag, 2004. (PDF, BibTeX)
• State space abstraction using shape graphs. In Automatic Verification of Infinite-State Systems (AVIS), Electronic Notes in Theoretical Computer Science. Elsevier, 2004. To appear. (PDF, BibTeX)
• Model checking graph transformations: A comparison of two approaches (with Ákos Schmidt and Dániel Varró). In H. Ehrig, G. Engels, F. Parisi-Presicce and G. Rozenberg, editors, International Conference on Graph Transformations (ICGT), volume 3256 of Lecture Notes in Computer Science, pages 226-241. Springer-Verlag, 2004. (PDF, BibTeX)
• Who is pointing when to whom: On model-checking pointer structures (with Dino Distefano and Joost-Pieter Katoen). CTIT Technical Report TR-CTIT-03-12, Department of Computer Science, University of Twente, September 2003. (PDF, BibTeX)
• A logic of local graph shapes. CTIT Technical Report TR-CTIT-03-35, Faculty of Informatics, University of Twente, August 2003. (PDF, BibTeX)
• Towards model checking graph grammars. In M. Leuschel, S. Gruner and S. Lo Presti, editors, Workshop on Automated Verification of Critical Systems (AVoCS), Technical Report DSSE-TR-2003-2, pages 150-160. University of Southampton, 2003. (PDF, BibTeX)
• Model checking birth and death (with Dino Distefano and Joost-Pieter Katoen). In R.A. Baeza-Yates, U. Montanari and N. Santoro, editors, Foundations of Information Technology in the Era of Network and Mobile Computing, volume 223 of IFIP Conference Proceedings, pages 435-447. Kluwer Academic Publishers, 2002. Full report version: TR-CTIT-01-40, University of Twente. (BibTeX)
• Model checking dynamic allocation and deallocation (with Dino Distefano and Joost-Pieter Katoen). CTIT Technical Report TR-CTIT-01-40, Department of Computer Science, University of Twente, March 2002. (PDF, BibTeX)

Model Driven Architecture

• An abstract metamodel for aspect languages (with Wilke Havinga, Tom Staijen, Lodewijk Bergmans and Klaas van den Berg). In Open and Dynamic Aspect Languages (Satellite workshop of AOSD), 2006. (BibTeX)
• Graph transformation semantics for a QVT language (with Ronald Nederpel). In International Workshop on Graph Transformation and Visual Modeling Techniques, Electronic Notes in Theoretical Computer Science, 2006. To appear. (PDF, BibTeX)
• Model Driven Architecture (with Uwe Aßmann and Mehmet Aksit, editors). volume 3599 of Lecture Notes in Computer Science. Springer-Verlag, 2005. (BibTeX)
• Modelling mobile health systems: an application of augmented MDA for the extended healthcare enterprise (with Val Jones and Ed Brinksma). In Proc. Ninth IEEE International EDOC Enterprise Computing Conference (EDOC), pages 58-69. IEEE Computer Society, 2005. (BibTeX)
• Subjects, models, languages, transformations. In Jean Bezivin and Reiko Heckel, editors, Language Engineering for Model-Driven Software Development, number 04101 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany, 2005. (BibTeX)
• Model Driven Architecture: Foundations and Applications (with , editor). CTIT Technical Report TR-CTIT-03-27. Faculty of Informatics, University of Twente, June 2003. Workshop proceedings. (PDF, BibTeX)

Formal theory of testing

• Fair testing (with Walter Vogler). CTIT Technical Report TR-CTIT-05-64, Department of Computer Science, University of Twente, December 2005. Submitted for publication. (PDF, BibTeX)
• Action refinement in conformance testing (with Machiel van der Bijl and Jan Tretmans). In F. Khendek and R. Dssouli, editors, Testing of Communicating Systems (TESTCOM), volume 3205 of Lecture Notes in Computer Science, pages 81-96. Springer-Verlag, 2005. Technical report version: TR-CTIT-05-51, Department of Informatics, University of Twente. (PDF, BibTeX)
• Action refinement in testiong with UIOCO (with Machiel van der Bijl and Jan Tretmans). CTIT Technical Report TR-CTIT-05-10, Department of Informatics, University of Twente, February 2005. (PDF, BibTeX)
• Component based testing with ioco (with Machiel van der Bijl and Jan Tretmans). In A. Petrenko and A. Ulrich, editors, Formal Apporaches to Testing of Software (FATES), volume 2931 of Lecture Notes in Computer Science, pages 86-100. Springer-Verlag, 2004. Full report: TR-CTIT-03-34, University of Twente. (PDF, BibTeX)
• Component based testing with ioco (with Machiel van der Bijl and Jan Tretmans). CTIT Technical Report TR-CTIT-03-34, Faculty of Informatics, University of Twente, August 2003. (PDF, BibTeX)
• Applications of fair testing (with Ed Brinksma and Walter Vogler). In Protocol Specification, Testing, and Verification, XVI. IFIP, Chapman & Hall, 1996. (PostScript, BibTeX)
• Fair testing (with Ed Brinksma and Walter Vogler). In I. Lee and S. A. Smolka, editors, Concurrency Theory (CONCUR), volume 962 of Lecture Notes in Computer Science, pages 313-327. Springer-Verlag, 1995. (PostScript, BibTeX)

Action refinement

• Action refinement (with Roberto Gorrieri). In J. A. Bergstra, A. Ponse and S. A. Smolka, editors, Handbook of Process Algebra, chapter 16, pages 1047-1147. Elsevier, 2001. (BibTeX)
• Vertical implementation (with Roberto Gorrieri). Information and Computation, 170:95-133, 2001. Extended version of ``Vertical Bisimulation'' (TAPSOFT '97). Full report version: Hildesheimer Informatik-Bericht 9/98, University of Hildesheim. (PostScript, BibTeX)
• Action contraction. In C. Palamidessi, editor, Concurrency Theory (CONCUR), volume 1877 of Lecture Notes in Computer Science, pages 290-304. Springer-Verlag, 2000. Report version: TR-CTIT-00-13, Faculty of Informatics, University of Twente. (PostScript, BibTeX)
• Action contraction using coupled simulation. CTIT Technical Report TR-CTIT-00-13, Faculty of Informatics, University of Twente, October 2000. A conference version of this report was presented at Concur 2000. (PostScript, PDF, BibTeX)
• Process algebra with action dependencies (with Heike Wehrheim). CTIT Technical Report 99-02, University of Twente, 1999. Appeared in Acta Informatica, vol. 38. (PDF, BibTeX)
• Vertical bisimulation (with Roberto Gorrieri). Hildesheimer Informatik-Bericht 9/98, University of Hildesheim, June 1998. (PostScript, BibTeX)
• Dependency-based action refinement (with Heike Wehrheim). In I. Prívara and P. Ruzicka, editors, Mathematical Foundations of Computer Science (MFCS), volume 1295 of Lecture Notes in Computer Science, pages 468-477. Springer-Verlag, 1997. (PostScript, BibTeX)
• Comparing syntactic and semantic action refinement (with Ursula Goltz and Roberto Gorrieri). Information and Computation, 125(2):118-143, March 1996. (BibTeX)
• An event-based SOS for a language with refinement. In J. Desel, editor, Structures in Concurrency Theory, Workshops in Computing, pages 294-309. Springer-Verlag, 1995. (PostScript, BibTeX)
• Methodological aspects of action refinement. In E.-R. Olderog, editor, Programming Concepts, Methods and Calculi, volume A-56 of IFIP Transactions, pages 227-246. IFIP, 1994. (PostScript, BibTeX)
• Models and Methods for Action Refinement. PhD thesis, University of Twente, Enschede, Netherlands, August 1993. (BibTeX)
• Abstraction and refinement in configuration structures (with Ruggero Costantini). Hildesheimer Informatik-Berichte 18/92, Institut für Informatik, University of Hildesheim, November 1992. (PostScript, BibTeX)

Process algebra

• Fair testing (with Walter Vogler). CTIT Technical Report TR-CTIT-05-64, Department of Computer Science, University of Twente, December 2005. Submitted for publication. (PDF, BibTeX)
• Component based testing with ioco (with Machiel van der Bijl and Jan Tretmans). CTIT Technical Report TR-CTIT-03-34, Faculty of Informatics, University of Twente, August 2003. (PDF, BibTeX)
• Action refinement (with Roberto Gorrieri). In J. A. Bergstra, A. Ponse and S. A. Smolka, editors, Handbook of Process Algebra, chapter 16, pages 1047-1147. Elsevier, 2001. (BibTeX)
• Vertical implementation (with Roberto Gorrieri). Information and Computation, 170:95-133, 2001. Extended version of ``Vertical Bisimulation'' (TAPSOFT '97). Full report version: Hildesheimer Informatik-Bericht 9/98, University of Hildesheim. (PostScript, BibTeX)
• Process algebra with action dependencies (with Heike Wehrheim). Acta Informatica, 38:155-234, 2001. Report version: TR-CTIT-99-02, Faculty of Informatics, University of Twente. (BibTeX)
• Bisimilarity of open terms. Information and Computation, 156(1/2):345-385, January 2000. EXPRESS '97 special issue; report version: Hildesheimer Informatik-Bericht 5/97, University of Hildesheim. (BibTeX)
• A mobile calculus with data (with Thomas Gehrke). Technical Report 99-04, Technical University of Braunschweig, Institute for Software, October 1999. (PostScript, BibTeX)
• Process algebra with action dependencies (with Heike Wehrheim). CTIT Technical Report 99-02, University of Twente, 1999. Appeared in Acta Informatica, vol. 38. (PDF, BibTeX)
• Spezifikation eines RPC-Speichers mit der Sprache ProFun (with Thomas Firley and Thomas Gehrke). In H. König and P. Langendörfer, editors, Formale Beschreibungstechniken für verteilte Systeme, pages 136-147. Shaker Verlag, Aachen, 1998. Report version: Hildesheimer Informatik-Bericht 4/98. (BibTeX)
• An algebraic semantics for message sequence chart documents (with Thomas Gehrke, Michaela Huhn and Heike Wehrheim). In S. Budkowski, A. Cavalli and E. Najm, editors, Formal Description Techniques. Chapman-Hall, 1998. Full report version: Hildesheimer Informatik-Bericht 5/98. (PostScript, BibTeX)
• An algebraic semantics for message sequence chart documents (with Thomas Gehrke, Michaela Huhn and Heike Wehrheim). Hildesheimer Informatik-Bericht 5/98, University of Hildesheim, May 1998. (PostScript, BibTeX)
• Process creation and full sequential composition in a name-passing calculus (with Thomas Gehrke). In C. Palamidessi and J. Parrow, editors, Expressiveness in Concurrency, volume 7 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1997. Corrected version in Hildesheimer Informatik-Bericht 97/7, University of Hildesheim. (PostScript, BibTeX)
• Bisimilarity of open terms. In C. Palamidessi and J. Parrow, editors, Expressiveness in Concurrency, volume 7 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1997. Full report version: Hildesheimer Informatik-Bericht 5/97, University of Hildesheim, May 1997. (BibTeX)
• Applications of fair testing (with Ed Brinksma and Walter Vogler). In Protocol Specification, Testing, and Verification, XVI. IFIP, Chapman & Hall, 1996. (PostScript, BibTeX)
• Fair testing (with Ed Brinksma and Walter Vogler). In I. Lee and S. A. Smolka, editors, Concurrency Theory (CONCUR), volume 962 of Lecture Notes in Computer Science, pages 313-327. Springer-Verlag, 1995. (PostScript, BibTeX)
• Weak sequential composition in process algebras (with Heike Wehrheim). In B. Jonsson and J. Parrow, editors, Concurrency Theory (CONCUR), volume 836 of Lecture Notes in Computer Science, pages 226-241. Springer-Verlag, 1994. (PostScript, BibTeX)

Partial order models

• Process algebra with action dependencies (with Heike Wehrheim). CTIT Technical Report 99-02, University of Twente, 1999. Appeared in Acta Informatica, vol. 38. (PDF, BibTeX)
• Algebra and theory of order-deterministic pomsets. Notre Dame Journal of Formal Logic, 37(2):283-320, 1996. (BibTeX)
• Denotational, causal, and operational determinism in event structures. In H. Kirchner, editor, Trees in Algebra and Programming (CAAP), volume 1059 of Lecture Notes in Computer Science, pages 272-286. Springer-Verlag, 1996. Full report version: HIB 29/95, Institut für Informatik, University of Hildesheim. (PostScript, BibTeX)
• Causal traces. Hildesheimer Informatik-Bericht 39/95, Institut für Informatik, University of Hildesheim, December 1995. (PostScript, BibTeX)
• A complete theory of deterministic event structures. In I. Lee and S. A. Smolka, editors, Concurrency Theory (CONCUR), volume 962 of Lecture Notes in Computer Science, pages 160-174. Springer-Verlag, 1995. (PostScript, BibTeX)
• Denotational, causal, and operational determinism in event structures. Hildesheimer Informatik-Bericht 29/95, Institut für Informatik, University of Hildesheim, September 1995. Appeared in CAAP '96. (PostScript, BibTeX)
• An event-based SOS for a language with refinement. In J. Desel, editor, Structures in Concurrency Theory, Workshops in Computing, pages 294-309. Springer-Verlag, 1995. (PostScript, BibTeX)
• Finite Petri nets as models for recursive causal behaviour (with Ursula Goltz). Theoretical Computer Science, 124:169-179, 1994. (BibTeX)
• Deterministic pomsets. Hildesheimer Informatik-Berichte 30/94, Institut für Informatik, University of Hildesheim, November 1994. (PostScript, BibTeX)
• Models and Methods for Action Refinement. PhD thesis, University of Twente, Enschede, Netherlands, August 1993. (BibTeX)
• Order isomorphism does not preserve global event independence. Bull. Eur. Ass. Theoret. Comput. Sci., 51:228-235, October 1993. Also available as Hildesheimer Informatik-Bericht 10/93, Institut für Informatik, University of Hildesheim. (PostScript, BibTeX)
• Abstraction and refinement in configuration structures (with Ruggero Costantini). Hildesheimer Informatik-Berichte 18/92, Institut für Informatik, University of Hildesheim, November 1992. (PostScript, BibTeX)
• Posets for configurations!. In W. R. Cleaveland, editor, Concur '92, volume 630 of Lecture Notes in Computer Science, pages 269-285. Springer-Verlag, 1992. (PostScript, BibTeX)

Last change: 26-04-02