Conference Articles, Journal Articles and Books

• Preprints, workshop articles and other publications

2008

Compositional Reasoning in Model-Based Verification of Adaptive Embedded Systems
Ina Schaefer, Arnd Poetzsch-Heffter. In: 6th IEEE Intl. Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town South Africa. (to appear), November, 2008

Slicing for Model Reduction in Adaptive Embedded Systems Development
Ina Schaefer, Arnd Poetzsch-Heffter. In: Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2008), Leipzig, Germany. May, 2008

Certifying Code Generation with Coq
Jan Olaf Blech, Benjamin Grégoire. In: Proceedings of the 7th Workshop on Compiler Optimization meets Compiler Verification (COCV 2008), Budapest, Hungary. ENTCS, April, 2008

Linking Programs to Architectures: An Object-Oriented Hierarchical Software Model based on Boxes
Jan Schäfer, Markus Reitz, Jean-Marie Gaillourdet, Arnd Poetzsch-Heffter. In: A. Rausch et al. ed., The Common Component Modeling Example: Comparing Software Component Models. LNCS, volume 5153, Springer, p. 238--266, to appear, 2008

CoBoxes: Unifying Active Objects and Structured Heaps
Jan Schäfer, Arnd Poetzsch-Heffter. In: G. Barthe and F. de Boer ed., 10th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2008). LNCS, volume 5051, Springer, p. 201--219, to appear, 2008

2007

From Model-Based Design to Formal Verification of Adaptive Embedded Systems
Rasmus Adler, Ina Schaefer, Tobias Schüle, Eric Vecchié. In: 9th International Conference on Formal Engineering Methods (ICFEM 2007), Boca Raton, FL. LNCS, Springer, November, 2007

A Parameterized Type System for Simple Loose Ownership Domains
Jan Schäfer, Arnd Poetzsch-Heffter. In: Journal of Object Technology. Special Issue ECOOP 2007, volume 5, number 6, p. 71--100, http://www.jot.fm/issues/issue_2007_06/article3, June, 2007

A Representation-Independent Behavioral Semantics for Object-Oriented Components
Arnd Poetzsch-Heffter, Jan Schäfer. In: 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). LNCS, volume 4468, Springer, p. 157--173, June, 2007

A Certifying Code Generation Phase
Jan Olaf Blech, Arnd Poetzsch-Heffter. In: Proceedings of the 6th Workshop on Compiler Optimization meets Compiler Verification (COCV 2007), Braga, Portugal. ENTCS, March, 2007

Immutable Objects for a Java-like Language
Christian Haack, Erik Poll, Jan Schäfer, Aleksy Schubert. In: Rocco De Nicola ed., 16th European Symposium on Programming (ESOP'07). LNCS, volume 4421, Springer, p. 347--362, Won the ETAPS award for the best theory paper at ETAPS, March, 2007

Modular Shape Analysis for Dynamically Encapsulated Programs
Noam Rinetzky, Arnd Poetzsch-Heffter, Ganesan Ramalingam, Mooly Sagiv, Eran Yahav. In: Rocco De Nicola ed., 16th European Symposium on Programming (ESOP'07). LNCS, volume 4421, Springer, March, 2007

Translation Validation for System Abstractions
Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter. In: 7th Workshop on Runtime Verification (RV'07), Vancouver, Canada. LNCS. volume 4839, Springer, March, 2007

Infering Ownership Types for Encapsulated Object-Oriented Program Components
Arnd Poetzsch-Heffter, Kathrin Geilmann, Jan Schäfer. In: T. Reps, M. Sagiv, and J. Bauer ed., Program Analysis and Compilation, Theory and Practice: Essays dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday. LNCS, volume 4444, Springer, p. 120--144, 2007

2006

Simple Loose Ownership Domains
Jan Schäfer, Arnd Poetzsch-Heffter. In: ECOOP Workshop on Formal Techniques for Java-like Programs, FTfJP 2006. July, 2006

Modular Invariants for Layered Object Structures
Peter Müller, Arnd Poetzsch-Heffter, Gary T. Leavens. In: Science of Computer Programming. volume 62, number 3, Elsevier, p. 253--286, 2006

Composable Component-Oriented Derivative Contracts
Markus Reitz, Ulrich Nögel. In: Transactions on Information Science and Applications. volume 9, number 3, WSEAS , p. 1756--1764, 2006

Derivative Contracts as Active Documents
Markus Reitz, Ulrich Nögel. In: 7th International Conference on Computers and Mathematics in Business and Economics (MCBE06). WSEAS, 2006

Flexible Design- und Bewertungsverfahren für Derivatverträge
Markus Reitz, Ulrich Nögel. In: Uni-Spektrum - Hochschulmagazin der TU Kaiserslautern. TU Kaiserslautern, p. 7, 2006

ComDeCo: Composable Derivative Contracts
Markus Reitz. In: Workshop End-User Development. Lecture Notes in Informatics, volume P-93, GI, p. 564--567, 2006

Software evolvability by component-orientation
Markus Reitz. In: 2nd International IEEE Workshop on Software Evolvability. IEEE Computer Society Proceedings, volume P2698, IEEE Computer Society, p. 66--73, 2006

Components: A Valuable Investment for Financial Engineering
Markus Reitz, Ulrich Nögel. In: 4th International Conference on Principles and Practice of Programming in Java (PPPJ06). International Conference Proceeding Series, volume 178, ACM, p. 153--162, 2006

Modular Specification of Encapsulated Object-Oriented Components
Arnd Poetzsch-Heffter, Jan Schäfer. In: Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem-Paul de Roever ed., Formal Methods for Components and Objects, Fourth International Symposium, FMCO 2005. LNCS, volume 4111, Springer, p. 313--341, 2006

Active Documents - Taking Advantage of component-orientation beyond pure reuse
Markus Reitz. In: Workshop on Component-Oriented Programming (WCOP 06). Interner Bericht 2006-11, Universität Karlsruhe, p. 67--74, 2006

2005

Towards Proof Generating Compilers
Arnd Poetzsch-Heffter, Marek J. Gawkowski. In: J. Knoop, G. C. Necula, W. Zimmermann ed., Electronic Notes in Theoretical Computer Science. volume 132, number 1, Elsevier, p. 37--51, 2005

2004

Formal Verification of a Commercial Smart Card Applet with Multiple Tools
Bart Jacobs, Claude Marché, Nicole Rauch. In: C. Rattray, S. Maharaj, C. Shankland ed., Algebraic Methodology and Software Technology (AMAST 04). LNCS, volume 3116, Springer, p. 241--257, July, 2004

Semantics-directed implementation of method-call interception
Ralf Lämmel, Christian Stenzel. In: IEE Proceedings - Software. volume 151, number 2, p. 109-127, April, 2004

Application and Formal Specification of Sorted Term-Position Algebras
Arnd Poetzsch-Heffter, Nicole Rauch. In: Jose L. Fiadeiro ed., 17th International Workshop on Recent Trends in Algebraic Development Techniques, WADT 2004, Barcelona, Spain. LNCS, volume 3423, Springer, p. 201--217, March, 2004

A Type System for Checking Applet Isolation in Java Card
Werner Dietl, Peter Müller, Arnd Poetzsch-Heffter. In: Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS 2004). LNCS, volume 3362, Springer, 2004

2003

Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL
Nicole Rauch, Burkhart Wolff. In: Thomas Arts and Wan Fokkink ed., Proc. 8th International Workshop on Formal Methods<br> for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science (ENTCS), volume 80, Elsevier, p. 40--56, June, 2003

Modular Specification of Frame Properties in JML
Peter Müller, Arnd Poetzsch-Heffter, Gary T. Leavens. In: Concurrency and Computation: Practice and Experience. volume 15, John Wiley & Sons, Ltd., p. 117--154, 2003

MultiMedia Instruction in Safe and Secure Systems
Bernd Krieg-Brückner, Dieter Hutter, Arne Lindow, Christopf Lüth, et al.. In: Recent Trends in Algebraic Development Techniques, 17th International Workshop, WADT 2002. LNCS, volume 2755, Springer, p. 82--117, 2003

2002

Precondition Generation for a Java Subset
Nicole Rauch. In: D. Haneberg, G. Schellhorn and W. Reif ed., FM-TOOLS 2002, The 5th Workshop on Tools for System Design and Verification, Reisensburg, Germany. Report 2002-11, Universität Augsburg, Institut für Informatik, p. 1--6, July, 2002

Using Data Groups to Specify and Check Side Effects
K. Rustan M. Leino, Arnd Poetzsch-Heffter, Yunhong Zhou. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation. volume 37, number 5, p. 246--257, June, 2002

Modular Specification and Verification of Object-Oriented Programs
Peter Müller. In: Modular Specification and Verification of Object-Oriented Programs. Lecture Notes in Computer Science, volume 2262, Fernuniversität Hagen, Springer Verlag, 2002

Predicate Transformation as a Proof Strategy
Nicole Rauch, Arnd Poetzsch-Heffter. In: Erik Poll ed., Proc. 4th ECOOP Workshop: Formal Techniques for Java-like Programs, Technical Report NIII-R0204. Computing Science Department, University of Nijmegen, p. 117--128, 2002

2001

How Java's Language Design Reflects the Requirements of Mobile Code
Arnd Poetzsch-Heffter. In: Informationstechnik und Technische Informatik. volume 43, number 3, Oldenbourg Verlag, p. 125--131, 2001

A Type System for Checking Applet Isolation in Java Card
Peter Müller, Arnd Poetzsch-Heffter. In: Formal Techniques for Java Programs. 2001

2000

Dynamic Components as Semantic Entities: Concept and Static Support
Arnd Poetzsch-Heffter. In: Goerigk, W. ed., Programmiersprachen und Rechenkonzepte mit Schwerpunkt Softwarekomponenten. Christian-Albrechts-Universität Kiel, p. 1--6, Bericht Nr.~2007, 2000

Formal Techniques for Java Programs
Sophia Drossopoulou, Susan Eisenbach, Bart Jacobs, Gary T. Leavens, Peter Müller. In: Malenfant, J. and Moisan, S. and Moreira, A. ed., Lecture Notes in Computer Science, volume 1964, Springer-Verlag, Available, 2000

Modular Specification and Verification Techniques for Object-Oriented Software Components
Peter Müller, Arnd Poetzsch-Heffter. In: Leavens, G. T. and Sitaraman, M. ed., Foundations of Component-Based Systems. Cambridge University Press, (to appear), 2000

An Architecture for Interactive Program Provers
Jörg Meyer, Arnd Poetzsch-Heffter. In: Graf, S. and Schwartzbach, M. ed., TACAS, Tools and Algorithms for the Construction and Analysis of Systems. LNCS, volume 1785, p. 63--77, Available, 2000

A Type System for Controlling Representation Exposure in Java
Peter Müller, Arnd Poetzsch-Heffter. In: Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{"u}ller, P. and Poetzsch-Heffter, A. ed., Formal Techniques for Java Programs. Technical Report 269, Fernuniversität Hagen, Available, 2000

1999

Formal Techniques for Java Programs
Bart Jacobs, Gary T. Leavens, Peter Müller, Arnd Poetzsch-Heffter. In: Moreira, A. and Demeyer, D. ed., Object-Oriented Technology. ECOOP'99 Workshop Reader. Lecture Notes in Computer Science, volume 1743, Springer-Verlag, Available, 1999

Universes: A Type System for Controlling Representation Exposure
Peter Müller, Arnd Poetzsch-Heffter. In: Poetzsch-Heffter, A. and Meyer, J. ed., Programming Languages and Fundamentals of Programming. Technical Report, volume 263, Fernuniversität Hagen, Available, 1999

A Programming Logic for Sequential Java
Arnd Poetzsch-Heffter, Peter Müller. In: D. Swierstra ed., ESOP '99. LNCS, volume 1576, Springer, 1999

Making Executable Interface Specifications More Expressive
Peter Müller, Jörg Meyer, Arnd Poetzsch-Heffter. In: Cap, C. H. ed., JIT '99 Java-Informations-Tage 1999. Informatik Aktuell, Springer-Verlag, Available, 1999

Interactive Verification Environments for Object-Oriented Languages
Jörg Meyer, Arnd Poetzsch-Heffter. In: Journal of Universal Computer Science. volume 5, number 3, p. 208--225, Available, 1999

1998

Logical Foundations for Typed Object-Oriented Languages
Arnd Poetzsch-Heffter, Peter Müller. In: Gries, D. and De~Roever, W. ed., Programming Concepts and Methods. Available, 1998

1997

Specification and Verification of Object-Oriented Programs
Arnd Poetzsch-Heffter. Habilitation thesis, Technical University of Munich, Available, January, 1997

A Logic for the Verification of Object-Oriented Programs
Arnd Poetzsch-Heffter, Peter Müller. In: Berghammer, R. and Simon, F. ed., Programming Languages and Fundamentals of Programming. Technical Report, volume 9717, Christian-Albrechts-Universität Kiel, Available, 1997

Formal Specification Techniques for Object-Oriented Programs
Peter Müller, Arnd Poetzsch-Heffter. In: Jarke, M. and Pasedach, K. and Pohl, K. ed., Informatik 97: Informatik als Innovationsmotor. Informatik Aktuell, Springer-Verlag, Available, 1997

Preserving the Correctness of Object-Oriented Programs under Extension
Peter Müller, Arnd Poetzsch-Heffter. In: Berghammer, R. and Simon, F. ed., Programming Languages and Fundamentals of Programming. Technical Report, volume 9717, Christian-Albrechts-Universität Kiel, Available, 1997

Developing Provably Correct Programs From Object-Oriented Components
Peter Müller, Arnd Poetzsch-Heffter. In: Leavens, Gary T. and Sitaraman, Murali ed., Foundations of Component-Based Systems. Available. HTML version available from http://www.cs.iastate.edu/~leavens/FoCBS/FoCBS.html, 1997

Prototyping Realistic Programming Languages Based on Formal Specifications
Arnd Poetzsch-Heffter. In: Acta Informatica. volume 34, p. 737--772, Available, 1997

1996

Using Occurrence and Evolving Algebras for the Specification of Language-Based Programming Tools
Arnd Poetzsch-Heffter. In: M. Wirsing ed., Algebraic Methodology and Software Technology, 5th International Conference, AMAST '96. LNCS 1101, Springer-Verlag, p. 583--586, Available, 1996

1995

Interface Specifications for Program Modules Supporting Selective Updates and Sharing and their Use in Correctness Proofs
Arnd Poetzsch-Heffter. In: G. Snelting ed., Softwaretechnik 95. Available, 1995

1994

Deriving Partial Correctness Logics From Evolving Algebras
Arnd Poetzsch-Heffter. In: B. Pehrson and I. Simon ed., IFIP 13th World Computer Congress '94. Elsevier, p. 434--439, Available, August, 1994

Developing Efficient Interpreters Based on Formal Language Specifications
Arnd Poetzsch-Heffter. In: P. Fritzson ed., Compiler Construction. LNCS 786, Springer-Verlag, p. 233--247, Available, 1994

1993

Programming Language Specification and Prototyping Using the MAX System
Arnd Poetzsch-Heffter. In: M. Bruynooghe and J. Penjam ed., Programming Language Implementation and Logic Programming. LNCS 714, Springer-Verlag, p. 137--150, Available, 1993

1992

Logic-Based Specification of Visibility Rules
Arnd Poetzsch-Heffter. In: U. Kastens, P. Pfahler ed., Compiler Construction. LNCS, volume 641, Available, 1992

1991

Implementing High-Level Identification Specifications
Arnd Poetzsch-Heffter. In: J. Maluszynski and M. Wirsing ed., Programming Language Implementation and Logic Programming. LNCS, volume 528, Available, 1991