My research interests are in the areas of:

• The design and verification of distributed multiprocessor systems.
• Design Methodologies including formal methods.
  
• Defining and Describing Distributed Services.
• AI in Games of Strategy.

Modern society has become reliant on software systems for many mission-critical and life-critical functions. One approach to verifying these software systems is to use formal mathematical logics, theorem provers and model checkers. My work has used a variety of formalisms such as Mixed Intuitionistic Linear Logic (MILL) and variants of the pi-calculus for the specification and verification of mission critical distributed systems as typified by communications and security protocols. As part of the Enterprise Ireland funded research project IMPROVE, I am working on the specification and verification of the family of protocols that can be found in modern Public Key Infrastructures.

In isolation, these formalisms will be of little practical value unless they are integrated into a design methodology that covers the complete development cycle from analysis, design, development and verification. These design methodologies have to be "designer-friendly". I have been involved in several national and international projects that address this and related issues. The goal of these projects is to develop object-oriented methodologies to aid a designer in bringing a design from initial requirements specification to a formal model.

In the area of web services, the Client-Server Matching project is investigating ways to provide a web-based framework to allow users to have universal access to web services from various access devices possibly via a series of intermediate services. This framework is dynamic and requires minimal configuration, but is still flexible enough to offer universal access as new applications/services and access devices are developed.

I am also interested in applications of Artificial Intelligence (AI) in Strategic Games. Although significant advances have been made in computer Chess, there is still a long way to go in the development of "intelligent" search algorithms for computer games, particularly games of strategy. My research analyses existing "expert" games to find recurrent partial patterns and their outcomes. When these partial positions re-occur, their associated outcomes are used to forward prune the search tree.

Publications:

Journals

• David Sinclair and James Power, “Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic”. Electronic Notes in Theoretical Computer Science, Volume 133, Pages 255-273. Edited by J. Bicarregui; A. Butterfield; A. Arenas. 2005


• James F. Power and David Sinclair. “A Formal Model of Forth Control Words in the Pi-calculus”. Journal of Universal Computer Science, vol. 10 iss. 9, pp. 1273-1293. 2004.


• David Sinclair. “The GST load balancing algorithm for parallel and distributed systems”. International Journal of Approximate Readoning (19). pp 39- 56. 1998.

Refereed Conference Proceedings

• O. Lyttleton, D. Sinclair, D. Tracey, “Mediating between Heterogeneous Ontologies using Schema Matching Techniques”. In proceedings of IEEE Information Reuse and Integration 2005 (IRI05), Las Vegas, August 2005


• David Sinclair, David Gray and Geoff Hamilton. “Synthesising Attacks on Cryptographic Protocols”. 2nd International Conference on Automated Technology for Verification and Analysis (ATVA 2004). Lecture Notes in Computer Science (LNCS 3299), pp. 49-63. Springer, London, November 2004.


• David Sinclair and James Power. “Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic”, 9th International Workshop of Formal Methods in Industrial Critical Systems (FMICS 2004), Linz, Austria, pp 263-280. Austrian Computer Society, ISBN 3902457031, September 2004.


• Frédéric Oehl, David Sinclair, Olga Kouchnarenko and Gérard Cece. “Automatic Approximation for the Verification of Cryptographic Protocols”. Formal Aspects of Security ’02. Lecture Notes in Computer Science (LNCS 2629), pp. 33-48. Springer, London, December 2002.


• Frédéric Oehl and David Sinclair. “Combining ISABELLE and Timbruk for Cryptographic Protocol Verification”. Workshop on Internet Security Communication (SECI) 2002. Tunis, Tunisia. September 2002.


• Frédéric Oehl and David Sinclair. “Combining Theorem Prover and Model Checker to verify Cryptographic Protocols”. Modelling and Verification of Parallel Processes ’02. Nantes, France. June 2002.


• Frederic Oehl and David Sinclair. “Combining two approaches for the verification of cryptographic protocols”. Specification and Verification of Emerging Systems ‘01. Paphos, Cryprus. December 2001.


• Benyamin Aziz, David Gray, Geoff Hamilton, Frederic Oehl and David Sinclair. “Implementing Protocol Verification for E-Commerce”. Advances in Infrastructure for Electronic Business, Science, and Education on the Internet. L'Aquila, Italy. August 2001.


• James Power and David Sinclair. “A Formal Model of Forth Control Words in the Pi-Calculus”. 6th International Workshop on Formal Methods for Industrial Critical Systems. Paris, France. July 2001.


• David Gray, Geoff Hamilton, James Power, David Sinclair. “A Specification of TCP/IP using Mixed Intuitionistic Linear Logic”. IEEE/IFIP Joint Workshop on Formal Specifications of Computer-Based Systems. Washington DC, USA. April 2001.


• David Sinclair, James Power, Paul Gibson, David Gray, Geoff Hamilton. “Specifying and Verifying IP with Linear Logic”. IEEE International Workshop on Distributed Systems Validation and Verification. Taiwan. April 2000.


• David Sinclair, James Power, Paul Gibson, David Gray, Geoff Hamilton, “Four Logics and a Protocol”, 3rd. Irish Workshop in Formal Methods, Galway, Ireland. July 1999.


• David Sinclair. “Using Example-Based Reasoning for Selective Move Generation in Two-Player Adversarial Games”. 4th European Workshop on Case-Based Reasoning; Lecture Notes in Artificial Intelligence 1448. Dublin, Ireland. September 1998.


• David Sinclair. “Using an Object-Oriented Methodology to bring a Hybrid System from Initial Concept to Formal Definition”. Hybrid and Real-Time Systems, Grenoble, France. March 1997


• David Sinclair. “The GST Load Balancing Algorithm for Parallel and Distributed Systems”. 1st International Workshop on Approximate Reasoning in Scheduling. Zurich, Switzerland. February, 1997.


• D.Sinclair, L. Cuypers, K. Verschaeve, E. Holz, A. Birbas, V. Mariatos, N. Kyrloglou, J-L Roux . “A formal approach to HW/SW co-design: the INSYDE project”. IEEE Symposium and Workshop on Engineering of Computer-Based Systems. Friedrichshafen, Germany. March 1996.


• D.Sinclair, B. Stone and G. Clynch. “An Object Oriented Methodology from Requirements to Validation”. 2nd Object Oriented Information Systems Conference. Dublin, Ireland. December 1995.


• D.Sinclair, E. Holz, D. Witaszek, M.Wasowski. “Validation of hybrid systems by co-simulation”. Hybrid Systems III. New Jersey, USA. October 1995.


• David Sinclair. “Synthesis of 2-Dimensional Grey Scale Filters by 3x3 Cellular Automata”, 3rd International Workshop on Parallel Image Analysis. Maryland, USA. June 1994.