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!
A poster about my work with Adam was presented at the SICSA DEMOfest, 2011.
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.
Manuela Bujorianu (graduated in 2006)
Thomas Wilson (graduated in 2008)
Back to my home page
- 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,
- 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,
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
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
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.
Formal Development of an SML Program Using the LEGO Theorem-Prover,
Savitri Maharaj. Technical report, AT&T Bell Labs, Murray Hill, NJ, 1991.
Z in LEGO , Savitri Maharaj, MSc thesis, the University of Edinburgh,
- 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