Static analysis of unbounded structures in object-oriented programs

Leiden Repository

Static analysis of unbounded structures in object-oriented programs

Title: Static analysis of unbounded structures in object-oriented programs
Author: Grabe, Immo
Publisher: Leiden Institute of Advanced Computer Science (LIACS), Faculty of Science, Leiden University
Issue Date: 2012-12-19
Keywords: Object creation
Concurrency
Multi-threading
Dynamic logic
Deadlock detection
Futures
Static analysis
Abstract: In this thesis we investigate different techniques and formalisms to address complexity introduced by unbounded structures in object-oriented programs. We give a representation of a weakest precondition calculus for abstract object creation in dynamic logic. Based on this calculus we define symbolic execution including abstract object creation. We investigate the complex behaviour introduced by multi-threading and give a formalism based on the transformation of multi-threaded reentrant call-graphs to thread automata and the application of context free language reachability to decide deadlock freedom of such programs. We give a formalisation of the observable interface behaviour of a concurrent, object-oriented language with futures and promises. The calculus captures the core of the Creol language and allows for a comparison with the concurrency model of thread-based, object-oriented languages like Java or C#. We give a technique to detect deadlock freedom for an Actor-like subset of the Creol language.
Description: Promotores: F.S. de Boer, M. Steffen
With Summary in Dutch
Supervisor:
Faculty: Faculteit der Wiskunde en Natuurwetenschappen
Citation: Grabe, I., 2012, Doctoral Thesis, Leiden University
ISBN: 97890889115475
Sponsor: The work in this thesis has been carried out at the Christian--Albrechts--Universit"at zu Kiel, the Centrum Wiskunde & Informatica (CWI), and the Universiteit Leiden. The research was partially funded by the EU-project IST-33826 emph{href{http://www.cwi.nl/projects/credo/}{Credo}: Modeling and analysis of evolutionary structures for distributed services}, the EU-project FP7-231620 emph{href{http://www.cse.chalmers.se/research/hats/}{HATS}: Highly Adaptable and Trustworthy Software using Formal Methods}, and the German-Norwegian DAAD-NWO exchange project {textsl{Avabi}} (Automated validation for behavioral interfaces of asynchronous active objects).
Handle: http://hdl.handle.net/1887/20325
 

Files in this item

Description Size View
application/pdf Full Text 1.024Mb View/Open
application/pdf Cover 274.5Kb View/Open
application/pdf Title Pages_Contents 127.7Kb View/Open
application/pdf Chapter 1 94.98Kb View/Open
application/pdf Part I: Chapter 2 248.2Kb View/Open Full text at publisher site
application/pdf Part II: Chapter 3 218.6Kb View/Open Full text at publisher site
application/pdf Part III: Chapter 4 484.1Kb View/Open Full text at publisher site
application/pdf Part IV: Chapter 5 292.2Kb View/Open Full text at publisher site
application/pdf Appendix 152.4Kb View/Open
application/pdf Abstract 99.60Kb View/Open
application/pdf Summary in Dutch 89.70Kb View/Open
application/pdf Curriculum Vitae_Bibliography 112.0Kb View/Open
application/pdf Propositions 101.0Kb View/Open

This item appears in the following Collection(s)