NWPT 2007
 The 19th Nordic Workshop on Programming Theory
Oslo, October 10-12, 2007

ABSTRACTS OF INVITED SPEAKERS' TALKS

• Gilles Barthe (INRIA Sophia-Antipolis, France)
  Certificate Translation
  Abstract:
  
  Program verification techniques based on programming logics and verification condition generators provide a powerful means to reason about programs. Whereas these techniques have very often been employed in the context of high-level languages in order to benefit from their structural nature, it is often required, especially in the context of mobile code, to prove the correctness of compiled programs. Thus it is highly desirable to have a means of bringing the benefits of source code verification to code consumers.
  We propose certificate translation, a mechanism that allows to transfer evidence from source programs to compiled programs. It builds upon the notion of certificate, which is used in Proof Carrying Code architectures to convey to the code consumer easily verifiable evidence that programs respect some policy. A certificate translator is an algorithm that turns certificates of source programs into certificates of compiled programs; its definition is tightly bound to the compiler used for programs, and the main difficulty in defining one stems from the optimizations performed by the compiler.
  
  
• Davide Sangiorgi (University of Bologna, Italy)
  A historical perspective on bisimulation and coinduction
  Abstract:
  
  I will discuss (a few aspects of) origins of bisimulation and bisimilarity, in the three fields where they have been independently discovered: Computer Science, Modal Logic, Set Theory.
  Bisimulation and bisimilarity are coinductive notions, and as such intimately related to fixed points. Therefore I will also present some some historical remarks on coinduction and fixed points.
  Finally, if there is time, I will present some problems for future work, that have to do with enhancing the bisimulation proof method.
  
  
• Neelam Soundarajan (Ohio State Univeristy, USA)
  Design Refinement: From Design Patterns to System Design
  (This is a report about work in progress. The work is being conducted jointly with Dr. Jason Hallstrom of Clemson University and Jason Kirschenbaum, graduate student at Ohio State University.)
  Abstract:
  
  Refinement has been a central theme of software engineering for many years. Indeed, the field is often considered to have been born at about the same time as when the concept of procedural refinement, or stepwise refinement, was initially developed. The concept of data refinement, developed a few years later, extends the ideas underlying procedural refinement and provides a powerful set of techniques for use by software developers in designing and implementing ADTs as well as object-oriented (OO) systems. (Interestingly, some of these ideas seem to have been anticipated by the designers of Simula, the original OO language designed at IfI.) Equally important, corresponding to each refinement concept, suitable reasoning techniques or refinement calculi have been developed that the software engineer can use to verify the correctness of the refinement steps he or she has performed in the design and implementation of a given system. The result has been a dramatic improvement in the quality and reliability of software developed using these techniques.
  The thesis underlying the work that this talk is based on is that there is another type of refinement, design refinement, that corresponds to going from a set of design patterns to the design of a system or part thereof. The goals of our work are to elaborate on the notion of design refinement and to develop suitable reasoning techniques that software engineers can appeal to in order to verify that, in their system design, the patterns in question have indeed been used correctly.
  
  

---

Last modified, 4 September 2007.