Memorial University   THEODORE S. NORVELL MUN Engineering
  RESEARCH  
   
 
 

My research interests include formal methods of programming software and hardware, specification languages, tools for formal program development, languages and compilers for hardware programming and hardware/software codesign, and program animation for teaching programming

See my publications page for papers.

Current research projects

Some of my current research projects are listed below

  • The Teaching Machine. Program animation means showing what's going on inside the computer as programs execute. The Teaching Machine is a program animator for C++ and Java. It is used in teaching these languages and for teaching programming concepts. The Teaching Machine provides visualizations automatically, i.e. with no annotation of the code. More recently the Teaching Machine has evolved to also support "program defined visualizations", which makes it now more suitable for data structure and algorithm animation.

    This project is a collaboration with Michael Bruce-Lockhart. Much of the programming was done by Derek Reilly. Some students who have contributed include John Anderson, Michael Burton, Shawn Cross, Stephen Hale, and Sun Hao. Other collaborators have included Yannis Cotronis, Pierluigi Crescenzi, and Siddharth Shah.

  • HARPO. HARPO stands for HARdware Programming with Objects. HARPO/L is a programming language for hardware/software codesign. The language is based on the idea of a network of cooperating, multi- threaded objects. My students and I have been designing the language and investigating methods of compiling it and similar languages to programmable hardware such as Coarse-Grained Reconfigurable Architectures. Currently we are looking at methods of proving concurrent programs free of certain classes of error and that they meet their specifications. Some of the students who are working or have worked on this with me include Rani Gnanaolivu, Ashraful Tuhin, Ken Zhang, Xiangwen Li, Lei Zhang, Yan Hao, and Shuang Wu.

    Here is a snapshot of the HARPO language, as of December 2010.

  • SIMPPLE. SIMPPLE is a project to develop an editor and proof checker for calculational program development. SIMPPLE's wide spectrum language is based on a strongly and polymorphically typed version of Eric Hehner's 'Practical Theory of Programming' (aka Predicative Programming). Stephen Motty has been working on using existing theorem provers to automatically verify each step. Bharathwaj Raghunathan helped with the XML editor that forms the basis of SIMPPLE's GUI.

    Although our focus is on verifying program derivations, we expect that SIMPPLE will be applicable to a number of areas of mathematics.


Past projects

  • Verification of Monitors. Fazilatunnessa Saimon, Dennis Peters, and I have developed a method of automatically verifying monitors using Microsoft Research's Verifier for Concurrent C.

  • Predicative programming and generic algorithm development. General algorithmic approaches --such as binary search, divide and conquer, greediness, and dynamic programming-- can be formalized as generic algorithms and proved correct independently of any intended application. We can then specialize these algorithms to particular applications, and so reuse not only the algorithm, but also its proof. Leila Mofara worked on this project.

  • SMALL. SMALL is a low level synchronous language for programming hardware (especially FPGAs). My students Ying Shen and Wei Song collaborated on it with me.

  • Robotics. Together with Ray Gosine and Siu O'Young, I supervised Faustina Hwang and Jamie King who were working on the coordination of multiple cooperating robots.

  • Xanthine/Xylia. Xanthine and Xylia are two different attempts to produce an XML editing platform suitable as a user interface for the SIMPPLE tool set. Xylia was a joint project with Dennis Peters. Some of the students who worked on it were Pouria Shaker, Naeim Semsarilar, and John Milley. Xanthine is a more recent approach, based on simultaneously supporting W3C's DOM interface and Swing's Document interface. Xanthine and Xylia eventually gave way to a Mozilla-based XML editor called GEFN, which I am developing as the underlying platform for SIMPLE 's user-interface.