Research interests:

I am interested in the use of simulation techniques, including agent-based simulation and virtual worlds, to understand real-world socio-economic phenomena. I am currently collaborating with Adam Kleczkowski from Mathematics on a project using agent-based simulation to model the effect of human behavioural changes on the spread of disease epidemics across a spatial network. Our models include consideration of the economic cost of behavioural changes (for example, if people stay home from work to avoid infection, there is cost to society), in relation to the economic benefit from reducing the size of the epidemic. We are currently writing up some interesting results: watch this space!

In previous work, I investigated the use of formal, mathematical techniques for the development of critical systems. Some specific areas of interest include: 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. I collaborated with Thomas Wilson and Robert Clark, on the Omnibus project. I have also worked with Carron Shankland and Muffy Calder on studying the symbolic semantics of the LOTOS specification language; with Juan Biccaregui on formalizing VDM within the PVS theorem prover; with Elsa Gunter on formalizing the semantics of Standard ML within the HOL theorem prover; with the Lego group at Edinburgh University; and with Edward Farrell of the University of the West Indies.

PhD students:

Publications:

• Savi Maharaj, Tamsin McCaldin, Adam Kleczkowski. A Participatory Simulation Model for Studying Attitudes to Infection Risk, in Proceedings of the Summer Computer Simulation Conference 2011 (SCSC 2011), ACM Digital Library, July 2011
• Kleczkowski A, Maharaj S. Stay at home, Wash Your Hands: Epidemic Dynamics with Awareness of Infection. In the Proceedings of the Summer Computer Simulation Conference, Ottawa, July 2010.
• S. MAHARAJ, C. McCAIG, and C. E. SHANKLAND, Studying the effects of adding spatiality to a process algebra model. 8th Workshop on Process Algebra and Stochastically Timed Activities :153-158, 2009. Edinburgh.
• 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. (Awarded Best Paper at SEFM'05)
• Algebraic Methodology and Software Technology, Proceedings of the 10th International Conference, AMAST 2004. Edited by Charles Rattray, Savitri Maharaj, and Carron Shankland. Springer LNCS 3116, July 2004
• 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