Research Areas

My main research area is currently Component-based Software Development. Previously, I worked on Formal Program Development in Computational Logic.

Component-based Software Development

My focus is on a software component model with encapsulation and compositionality. As a first step, I have (with Zheng Wang) surveyed existing component models, and proposed (with Perla Velasco Elizondo and Zheng Wang) exogenous connectors for components.

I have been working on a logical approach to the semantics and specification of components, interfaces, composition and correctness. With Mario Ornaghi, Juliana Küster Filipe, Hirokazu Yatsu, Kenji Taguchi and Alan Wills, I have considered the semantic foundations of components that are larger than single objects, viz. objected-oriented design frameworks and Catalysis frameworks.

With Michel Vanden Bossche, I have considered the potential role of logic programming in component-based software development.

Formal Program Development in Computational Logic

My research in component-based software development is firmly rooted in my work in formal program development in computational logic.

My first piece of work here (with Steven Prestwich) is a top-down method (for deriving recursive procedures) that can be partially automated. To formalise the underlying intuition and ideas, I then studied the theoretical foundations and defined a formal framework with Mario Ornaghi. Using this framework, we have been able to study different forms of specifications, clarify the distinction between specifications and programs, give an incompleteness result, formalise a distinction between synthesis and transformation, define the halting problem and state halting principles, and define and synthesise steadfast programs. Steadfast programs are correct and correctly reusable; that is, their correctness is preserved through inheritance hierarchies. These results provide the foundations for an object-oriented approach to deductive synthesis of logic programs.

Our approach can be extended to constraint logic programs. We have also applied our ideas to program transformation, with Alberto Pettorossi and Maurizio Proietti. With Pierre Flener and Julian Richardson, we have defined program schemas and their correctness, and used them to guide program synthesis. With Yves Deville, I compiled a survey of logic program synthesis for the Journal of Logic Programming (Special Issue: Ten Years of Logic Programming). With Geraint Wiggins, I gave an invited advanced tutorial on Logic Program Synthesis at the Eleventh International Conference on Logic Programming, 1994. With Pierre Flener, Mario Ornaghi, and Julian Richardson, I gave a tutorial on Schema-Guided Generation of Correctly Reusable Programs at the Twelfth IEEE International Automated Software Engineering Conference, 1999.

Algorithm Synthesis

A logic program represents the logic component of an algorithm. For simple algorithms, I have applied my work in logic program synthesis directly to algorithm synthesis.

Publications

A list of some of my publications can be found here.

PhD projects

A list of PhD projects that I offer can be found here.

Contact Details