• Program Verification
• Object Calculi

This thesis presents some original results in the framework of program verification, referred in particular to object-oriented languages. Object-oriented concepts and programs are expressed using object calculi, since they allow to formalize the basic ideas behind the object-oriented approach, without considering the details which are peculiar of each particular language. We will initially present a very simple object calculus, which models the classical object-oriented features, and which has the computational power of Church's untyped lambda-calculus. This calculus has a functional behavior, and in the following of the thesis it will be extended to include types, to formalize the natural imperative behavior of object-oriented languages, and to extend the model to concurrent languages. The verification of the properties of object-oriented programs will be based on abstract interpretation, since in many cases it can be more precise than other widely used techniques of analysis, like for example model checking or type inference. We will present in detail the theory behind this verification method that will be used as a unified approach in the rest of thesis. The approach will be used in three examples of analysis of object calculi, applied to the fields of safety, optimization and security. The first analysis, related to safety, is intended to verify that threads belonging to a unique concurrent program do not access shared resources simultaneously. We will extend the simple calculi presented at the beginning of the thesis with primitives for locking and unlocking objects, and using a very simple abstraction, we will be able to be more precise in our results than other approaches based on type systems. The second analysis, related to optimization, is in some way complementary to the first one. In fact, in this second case, our aim is to avoid the use of unnecessary locks in concurrent programs, since they often cause an overhead in computation. We will further extend our language with constructs for tracing the objects and the threads which acquire locks on them. The analysis will then check the dependencies between the various locks, to see if some of them may be safely deleted from programs without incurring in an erroneous behavior due to simultaneous accesses to shared resources. The third analysis will be intended to check a property of secure information flow in concurrent programs. The language will be further extended to include information levels and the analysis will check if, for each point of the computation, the values contained in variables are, in some ways, dependent of other variables with higher information levels.