Research interests:

I am interested in the use of formal, mathematical techniques for the development of critical systems. Some specific areas of interest are: the use of theorem-proving tools, particularly those based on higher-order logics and type theory, for formal reasoning about specifications, programming languages and programs; the design and semantics of formal specification languages. Currently, I am working with Thomas Wilson and Robert Clark, on the Omnibus project.

PhD students:

Publications:

• WILSON, T., MAHARAJ, S. and CLARK, R.G., Flexible and Configurable Verification Policies with Omnibus, Software and Systems Modeling, Springer, published online June 2007, DOI 10.1007/s10270-007-0060-1, ISSN 1619-1374.

• Bujorianu M, Bujorianu L-M, Maharaj S. Distributed Stochastic Hybrid Systems. In the proceedings of the World Congress of the International Federation on Automation and Control (IFAC 2005) , Elsevier Press, ISBN 0-08-045108-X, June 2006 .
• Maharaj S, Rattray C, Shankland C (editors). Theoretical Computer Science. 351(2), February 2006

• WILSON, T., MAHARAJ, S. and CLARK, R.G., Omnibus: a clean language and supporting tool for integrating different assertion-based verification techniques pp 43-52 in Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005), Newcastle, July 2005.

• WILSON, T., MAHARAJ, S. and CLARK, R.G., Omnibus Verification Policies: A Flexible, Configurable Approach to Assertion-Based Software Verification, pp 150-159 in 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, Germany, IEEE Computer Society, September 2005. (Best Paper at conference)

• IEEE 1394 Tree Identify Protocol: Introduction to the Case Study. Savi Maharaj, Judi Romijn, and Carron Shankland. In Formal Aspects of Computing Science 14(3), pp 200-214, 2003.

• A Modal Logic for Full LOTOS based on Symbolic Transition Systems. Muffy Calder, Savi Maharaj, and Carron Shankland. In The Computer Journal (ISSN 0010-4620), Vol 45, No 1, February 2002, pp 55-61
• Towards a Formalization of Viewpoints Testing. Marius Bujorianu, Manuela Bujorianu, and Savi Maharaj. In the proceedings of Formal Approaches to Testing of Software, Brno, August 2002, Rob Hierons and Thierry Jeron eds, pp 137-1
• An Adequate Logic for Full LOTOS. Muffy Calder, Savi Maharaj, and Carron Shankland.  In the proceedings of Formal Methods Europe, Springer-Verlag LNCS 2021, ISBN 3-540-41791-5, pp 384-395, March 2001.
• S. Maharaj, J. Romijn and C. Shankland (eds). Proceedings of International Workshop on Applications of Formal Methods to IEEE Standard 1394, Mar 2001. ISBN 1-85769-1431.
• A PVS Theory of Symbolic Transition Systems. Savi Maharaj. In the supplemental proceedings of Theorem Proving in Higher Order Logics, 2001, University of Edinburgh Division of Informatics Research Report EDI-INF-RR-0046, pp 255-266. August 2001
• A Survey of Formal Methods Applied to Leader Election in IEEE 1394. Savi Maharaj and Carron Shankland. Journal of Universal Computer Science (ISSN: 0948-6968), Springer, November 2000.
• A Survey of Formal Methods applied to IEEE 1394. Savi Maharaj and Carron Shankland. pp 25-26, proceedings of the Joint Workshop on Formal Specifications of Computer-Based Systems (ISBN 1-85-769121-0), Edinburgh, Scotland, April 2000.
• Towards a Method of Test Case Extraction from Correctness Proofs. Savi Maharaj. pp 45-46, proceedings of the 14th International Workshop on Algebraic Development Techniques, Bonas, France, November 1999.
• On the Verification of VDM Specification and Refinement with PVS, Sten Agerholm, Juan Bicarregui and Savi Maharaj, 1998, pp 157-189 of "Proof in VDM: case studies" (ISBN 3540761861), ed. Juan Bicarregui, Springer-Verlag, March 1998.
• On Verification of VDM Specification and Refinement with PVS, Savi Maharaj and Juan Bicarregui, 1997. pp 280-289, proceedings of the 12th IEEE International Conference in Automated Software Engineering (ISBN: 0-8186-7961-1) Abstract
• A Type-theoretic Analysis of Modular Specifications, Savitri Maharaj. PhD thesis, the University of Edinburgh, 1996. Abstract
• Studying the ML module system in HOL, Elsa Gunter and Savi Maharaj. In The Computer Journal: Special Issue on Theorem Proving in Higher Order Logics , 1995. An updated version of our 1994 paper. Abstract
• Studying the ML module system in HOL, Savi Maharaj and Elsa Gunter. In Higher Order Logic Theorem Proving and Its Applications , Springer-Verlag LNCS 859, 1994.
• Encoding Z-style Schemas in Type Theory, Savi Maharaj. In TYPES '93: Types for Proofs and Programs, Springer-Verlag LNCS 806, 1994. Abstract
• The LEGO library, Claire Jones and Savi Maharaj, 1993. Much revised by others afterwards, and probably now obsolete.
• The Formal Development of an SML Program Using the LEGO Theorem-Prover, Savitri Maharaj. Technical report, AT&T Bell Labs, Murray Hill, NJ, 1991. Abstract
• Implementing Z in LEGO , Savitri Maharaj, MSc thesis, the University of Edinburgh, 1990. Abstract
• A Computer Package for Studying Graph Polynomials, Savitri Maharaj, Technical Report, Dept of Mathematics and Computer Science, the University of the West Indies, 1988. Abstract