I grew up in Trinidad and Tobago, where I graduated with a BSc in Maths and Computer Science from the University of the West Indies. After a short (but sufficient!) stint as a COBOL programmer, I came to Scotland where I did MSc and PhD degrees in Computer Science at the University of Edinburgh. My PhD was partly funded through summer jobs at what was then called AT&T Bell Labs, where I worked within an exciting research department which, sadly, no longer exists. After the PhD (phew!) I spent a year on an ERCIM fellowship which allowed me to visit the CROAP group at INRIA in France and the Department for Computation and Information at RAL in England. I then returned to Scotland to become a lecturer at the University of Stirling. I am married to Neil and we have two children, Sharda and Jamie.
A Participatory Simulation Model for Studying Attitudes to Infection Risk. Summer Computer Simulation Conference 2011 (SCSC 2011)
The Society for Modeling and Simulation International
Studying the effects of adding spatiality to a process algebra model. 8th Workshop on Process Algebra and Stochastically Timed Activities (PASTA 2009): Edinburgh, UK
Process Algebra and Stochastically Timed Activities (PASTA)
http://www.dcs.ed.ac.uk/pepa/group/pastaworkshop/
Omnibus Verification Policies: A Flexible, Configurable Approach to Assertion-Based Software Verification. 3rd IEEE International Conference on Software Engineering and Formal Methods
Stay at Home, Wash Your Hands: Epidemic Dynamics with Awareness of Infection. Summer Simulation Multiconference
I am interested in the use of simulation techniques, including agent-based simulation and virtual worlds, to understand real-world socio-economic phenomena. I also work on the use of interactive simulations and games for science communication, education, and in the development of decision support tools for diverse users. My current projects focus on applications within tree and plant health and agriculture in the UK and in India. 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.
Multimodal data analysis for monitoring invasive aquatic weeds in India
PI: Dr Savi Maharaj
Funded by: Royal Academy of Engineering
–
Protecting Food Security in SE Asian Countries by Developing Early-Warning and Ready-Response Systems for Invasive Weed Incursions
PI: Dr Savi Maharaj
Funded by: Academy of Medical Sciences
–
Exploiting serious games for public engagement and citizen science in plant health
PI: Dr Savi Maharaj
Funded by: Scottish Informatics & Computer Science Alliance
–
Gamification: scoping the use of games to engage and learn
PI: Dr Savi Maharaj
Funded by: Department for Environment Food & Rural Affairs
–
Article
Pirbasti MA, Akbari V, Bhowmik D, Maharaj S & Marino A (2024) Detection and Mapping of Water Hyacinth Growth Cycle in Anzali International Wetland using Sentinel-2 Time Series. IEEE Journal of Selected Topics in Applied Earth Observations and Remote Sensing, 17, pp. 13346 - 13357. https://doi.org/10.1109/jstars.2024.3427002
Conference Paper (unpublished)
Akbari V, Datta A, Bhowmik D, Marino A, Kumar S, Rupavatharam S, Prabhu GN, Kleczkowski A, R. P. Sujeetha JA & Maharaj S (2022) Multitemporal multispectral drone imagery for water hyacinth mapping in Patancheru lake, Hyderabad, India. Bostater CR (Editor) & Neyt X (Editor) Remote Sensing of the Ocean, Sea Ice, Coastal Waters, and Large Water Regions 2022, Berlin, Germany, 05.09.2022-08.09.2022. https://doi.org/10.1117/12.2639004
Article
Detecting Water Hyacinth Infestation in Kuttanad, India, Using Dual-Pol Sentinel-1 SAR Imagery
Simpson MD, Akbari V, Marino A, Prabhu GN, Bhowmik D, Rupavatharam S, Datta A, Kleczkowski A, Sujeetha JARP, Gunjotikar Anantrao G, Kampurath Poduvattil V, Kumar S, Maharaj S & Hunter PD (2022) Detecting Water Hyacinth Infestation in Kuttanad, India, Using Dual-Pol Sentinel-1 SAR Imagery. Remote Sensing, 14 (12), Art. No.: 2845. https://doi.org/10.3390/rs14122845
Conference Paper (published)
Monitoring water hyacinth in Kuttanad, India using Sentinel-1 SAR data
Simpson M, Marino A, Prabhu GN, Bhowmik D, Rupavatharam S, Datta A, Kleczkowski A, Sujeetha JARP & Maharaj S (2021) Monitoring water hyacinth in Kuttanad, India using Sentinel-1 SAR data. In: 2020 IEEE India Geoscience and Remote Sensing Symposium (InGARSS). IEEE International India Geoscience and Remote Sensing Symposium 2020 (InGARSS), Online, 02.12.2020-05.12.2020. Piscataway, NJ, USA: IEEE. https://doi.org/10.1109/InGARSS48198.2020.9358977
Conference Paper (published)
Comparing a Game v. Non-Game approach for plant provenance public education
Docherty C, Rutherford A, Jones G & Maharaj S (2021) Comparing a Game v. Non-Game approach for plant provenance public education. In: Gabron S (ed.) GSGS '21 - International Conference on Gamification and Serious Game Proceeding. Gamification & Serious Game Symposium. GSGS '21 - International Conference on Gamification and Serious Game, Lausanne, Switzerland, 28.06.2021-09.07.2021. Dublin: Digital Kingdom. https://gsgs.ch/wp-content/uploads/2021/07/gsgs21.pdf
Conference Paper (published)
Akbari V, Simpson M, Maharaj S, Marino A, Bhowmik D, Prabhu GN, Rupavatharam S, Datta A, Kleczkowski A & Sujeetha JARP (2021) Monitoring Aquatic Weeds In Indian Wetlands Using Multitemporal Remote Sensing Data With Machine Learning Techniques. In: 2021 IEEE International Geoscience and Remote Sensing Symposium IGARSS. International Geoscience and Remote Sensing Symposium (IGARSS), Belgium, 12.07.2021-16.07.2021. Piscataway, NJ, USA: IEEE. https://doi.org/10.1109/IGARSS47720.2021.9553207
Review
Monitoring the spread of water hyacinth (Pontederia crassipes): challenges and future developments
Datta A, Maharaj S, Prabhu GN, Bhowmik D, Marino A, Akbari V, Rupavatharam S, Sujeetha JAR, Anantrao GG, Poduvattil VK, Kumar S & Kleczkowski A (2021) Monitoring the spread of water hyacinth (Pontederia crassipes): challenges and future developments. Frontiers in Ecology and Evolution, 9, Art. No.: 631338. https://doi.org/10.3389/fevo.2021.631338
Article
Ameerbakhsh O, Maharaj S, Hussain A & McAdam B (2019) A comparison of two methods of using a serious game for teaching marine ecology in a university setting. International Journal of Human-Computer Studies, 127, pp. 181-189. https://doi.org/10.1016/j.ijhcs.2018.07.004
Conference Paper (published)
An exploratory case study of interactive simulation for teaching Ecology
Ameerbakhsh O, Maharaj S, Hussain A, Paine CET & Taiksi S (2016) An exploratory case study of interactive simulation for teaching Ecology. In: 2016 15th International Conference on Information Technology Based Higher Education and Training (ITHET). ITHET 2016: 15th International Conference on Information Technology Based Higher Education and Training, Istanbul, Turkey, 08.09.2016-10.09.2016. Piscataway, NJ, USA: IEEE. https://doi.org/10.1109/ITHET.2016.7760725
Presentation / Talk
Gamification for public engagement with invasive tree pests and diseases
Maharaj S, Jones G, Greene P & Docherty C (2016) Gamification for public engagement with invasive tree pests and diseases. First International European Citizen Science Association (ESCA) Conference 2016: Citizen Science - Innovation in Open Science, Society and Policy, Berlin, 19.05.2016-21.05.2016.
Article
Cook D, Aurambout J, Villalta O, Liu S, Edwards J & Maharaj S (2016) A bio-economic 'war game' model to simulate plant disease incursions and test response strategies at the landscape scale. Food Security, 8 (1), pp. 37-48. https://doi.org/10.1007/s12571-015-0524-z
Article
Williams L, Rasmussen S, Kleczkowski A, Maharaj S & Cairns N (2015) Protection motivation theory and social distancing behaviour in response to a simulated infectious disease epidemic. Psychology, Health and Medicine, 20 (7), pp. 832-837. https://doi.org/10.1080/13548506.2015.1028946
Conference Paper (unpublished)
Gamification for public engagement with invasive tree pests and diseases
Maharaj S (2015) Gamification for public engagement with invasive tree pests and diseases. European Citizen Science Association conference, Berlin.
Article
Spontaneous social distancing in response to a simulated epidemic: a virtual experiment
Kleczkowski A, Maharaj S, Rasmussen S, Williams L & Cairns N (2015) Spontaneous social distancing in response to a simulated epidemic: a virtual experiment. BMC Public Health, 15, Art. No.: 973. https://doi.org/10.1186/s12889-015-2336-7
Research Report
Gamification within plant health in the Forestry Commission
Maharaj S & Greene P (2015) Gamification within plant health in the Forestry Commission. Forestry Commission Scotland. University of Stirling. http://www.forestry.gov.uk/pdf/Gamification_in_the_FC.pdf/$FILE/Gamification_in_the_FC.pdf
Conference Paper (published)
Banerjee S & Maharaj S (2015) Strategic Interactions and Information Exchange on Networks: An Agent Based Simulation Model of Landowner Behavior in Conservation Incentive Schemes. In: Miguel F, Amblard F, Barcelo J & Madella M (eds.) Advances in Computational Social Science and Social Simulation: Proceedings of the Social Simulation Conference 2014 Barcelona, Catalunya (Spain), September 15. Social Simulation Conference, Universitat Autonoma Barcelona, 01.09.2014-05.09.2014. Barcelona: Universitat Autònoma de Barcelona Press, pp. 42-46. http://ddd.uab.cat/pub/poncom/2014/125597/advcomsocsci_a2014.pdf
Conference Paper (published)
Reflections on a virtual experiment addressing human behavior during epidemics
Delaney L, Kleczkowski A, Maharaj S, Rasmussen S & Williams L (2013) Reflections on a virtual experiment addressing human behavior during epidemics. In: SummerSim '13 2013 Summer Simulation Multiconference Toronto, Canada — July 07 - 10, 2013. Simulation series, 45.11. Summer Computer Simulation Conference 2013, Toronto, Canada, 07.07.2013-10.07.2013. Vista, CA: Society for Modeling & Simulation International. http://dl.acm.org/citation.cfm?id=2557732&CFID=279840820&CFTOKEN=77799498
Article
Controlling epidemic spread by social distancing: Do it well or not at all
Maharaj S & Kleczkowski A (2012) Controlling epidemic spread by social distancing: Do it well or not at all. BMC Public Health, 12 (679). https://doi.org/10.1186/1471-2458-12-679
Conference Paper (published)
A Participatory Simulation Model for Studying Attitudes to Infection Risk
Maharaj S, Kleczkowski A & McCaldin T (2011) A Participatory Simulation Model for Studying Attitudes to Infection Risk. In: Proceedings of the Summer Computer Simulation Conference 2011 (SCSC 2011). Summer Computer Simulation Conference 2011 (SCSC 2011), The Hague, NL, 27.06.2011-30.06.2011. California: Society for Modeling and Simulation International Vista / ACM Digital Library, pp. 8-13.
Conference Paper (published)
Stay at Home, Wash Your Hands: Epidemic Dynamics with Awareness of Infection
Kleczkowski A & Maharaj S (2010) Stay at Home, Wash Your Hands: Epidemic Dynamics with Awareness of Infection. In: SummerSim '10 2010 Summer Simulation Multiconference. Summer Simulation Multiconference, Ottawa, Canada, 01.07.2010. San Diego: Society for Computer Simulation International, pp. 141-146. http://dl.acm.org/citation.cfm?id=1999432
Conference Paper (published)
Studying the effects of adding spatiality to a process algebra model
Maharaj S, McCaig C & Shankland C (2009) Studying the effects of adding spatiality to a process algebra model. In: Clark A & Guerriero M (eds.) 8th Workshop on Process Algebra and Stochastically Timed Activities: PASTA 2009. 8th Workshop on Process Algebra and Stochastically Timed Activities (PASTA 2009): Edinburgh, UK, Edinburgh, 26.08.2009-26.08.2009. Edinburgh, UK: University of Edinburgh, pp. 153-158. http://www.dcs.ed.ac.uk/pepa/group/pastaworkshop/PASTA09/proceedings.pdf
Technical Report
A Case Study in Integrated Assertion-Based Verification with Omnibus
Wilson T, Maharaj S & Clark R (2009) A Case Study in Integrated Assertion-Based Verification with Omnibus. Technical Report CSM, 176. Department of Computing Science and Mathematics, University of Stirling.
Article
Flexible and Configurable Verification Policies with Omnibus
Wilson T, Maharaj S & Clark R (2008) Flexible and Configurable Verification Policies with Omnibus. Software and Systems Modeling, 7 (3), pp. 257-272. http://www.springerlink.com/content/9543347t1h403181/fulltext.pdf; https://doi.org/10.1007/s10270-007-0060-1
Technical Report
Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors
Wilson T, Maharaj S & Clark R (2007) Push-Button Tools for Application Developers, Full Formal Verification for Component Vendors. Technical Report CSM, 167. Department of Computing Science and Mathematics, University of Stirling.
Other
Maharaj S (Editor), Shankland C (Editor) & Rattray C (Editor) (2006) Theoretical Computer Science. Theoretical Computer Science, 351 (2). http://www.sciencedirect.com/science/journal/03043975/351/2
Conference Paper (published)
Wilson T, Maharaj S & Clark R (2005) Omnibus verification policies: A flexible, configurable approach to assertion-based software verification. In: Aichernig B & Beckert B (eds.) SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings. 3rd IEEE International Conference on Software Engineering and Formal Methods, Koblenz, Germany, 07.09.2005-09.09.2005. Los Alamitos, CA: The Institute of Electrical and Electronics Engineers, Inc, pp. 150-159. http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10529
Conference Paper (published)
Distributed stochastic hybrid systems
Bujorianu ML, Bujorianu MC & Maharaj S (2005) Distributed stochastic hybrid systems. In: Zitek P (ed.) Proceedings of the 16th IFAC World Congress, 2005. IFAC Proceedings Volumes, 16. 16th World Congress of the International Federation on Automation and Control (IFAC 2005), Czech Republic, 04.07.2005-08.07.2005. Amsterdam: Elsevier for International Federation of Automatic Control, pp. 158-163. http://www.ifac-papersonline.net/Detailed/27660.html
Conference Paper (published)
Wilson T, Maharaj S & Clark R (2005) Omnibus: a clean language and supporting tool for integrating different assertion-based verification techniques. In: Butler M, Jones C, Romanovsky A & Troubitsyna E (eds.) Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005). Technical Report Series, CS-TR-915. Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005), Newcastle, 19.07.2005-19.07.2005. Newcastle upon Tyne: University of Newcastle upon Tyne, pp. 43-52. http://rodin.cs.ncl.ac.uk/REFT.htm
Edited Proceedings
Rattray C, Maharaj S & Shankland C (eds.) (2004) Algebraic Methodology and Software Technology: 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004. Proceedings. Lecture Notes in Computer Science, 3116. AMAST'2004 - 10th International Conference on Algebraic Methodology And Software Technology. Berlin Heidelberg: Springer.
Article
IEEE 1394 Tree Identify Protocol: Introduction to the case study
Maharaj S, Romijn J & Shankland C (2003) IEEE 1394 Tree Identify Protocol: Introduction to the case study. Formal Aspects of Computing, 14 (3), pp. 200-214. https://doi.org/10.1007/s001650300001
Other
Cooke J (Editor), Maharaj S (Editor), Romijn J (Editor) & Shankland C (Editor) (2003) Formal Methods applied to IEEE 1394: A Comparative Case Study. Special issue of Formal Aspects of Computing. Formal Aspects of Computing, 14 (3). http://link.springer.com/journal/165/14/3
Article
A modal logic for Full LOTOS based on symbolic transition systems
Calder M, Maharaj S & Shankland C (2002) A modal logic for Full LOTOS based on symbolic transition systems. Computer Journal, 45 (1), pp. 55-61. https://doi.org/10.1093/comjnl/45.1.55
Conference Paper (published)
Towards a Formalization of Viewpoints Testing
Bujorianu MC, Maharaj S & Bujorianu ML (2002) Towards a Formalization of Viewpoints Testing. In: Hierons R & Thierry J (eds.) Formal Approaches to Testing of Software: FATES’02 A Satellite Workshop of CONCUR’02, Brno, Czech Republic, August 24th 2002 Proceedings. FATES’02: A Satellite Workshop of CONCUR’02, Brno, Czech Republic, 24.08.2002-24.08.2002. Switzerland: Springer, pp. 137-151. http://kar.kent.ac.uk/13752/1/FormalRob.pdf
Edited Proceedings
Shankland C, Romijn J & Maharaj S (eds.) (2001) IEEE 1394 (Firewire) Workshop: International Workshop on Applications of Formal Methods to IEEE 1394 Standard. IEEE 1394 (FireWire) Workshop: International Workshop on Application of Formal Methods to IEEE 1394 Standard, Stirling, Scotland, 13.03.2001-13.03.2001. Stirling, Scotland: University of Stirling,Dept of Computing Science & Maths.
Conference Paper (published)
An Adequate Logic for Full LOTOS
Calder M, Maharaj S & Shankland C (2001) An Adequate Logic for Full LOTOS. In: Oliveira J & Zave P (eds.) FME 2001: Formal Methods for Increasing Software Productivity. Lecture Notes in Computer Science, 2021. International Symposium of Formal Methods Europe, Berlin, Germany, 12.03.2001-16.03.2001. Berlin Heidelberg: Springer, pp. 384-395. http://link.springer.com/chapter/10.1007/3-540-45251-6_21
Conference Paper (published)
A PVS Theory of Symbolic Transition Systems
Maharaj S (2001) A PVS Theory of Symbolic Transition Systems. In: Boulton R & Jackson P (eds.) Theorem Proving in Higher Order Logics, 2001, Supplemental Proceedings. Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, 03.09.2001-06.09.2001. Edinburgh, Scotland: Division of Informatics, University of Edinburgh, pp. 255-266. http://www.inf.ed.ac.uk/publications/online/0046/
Conference Paper (published)
A Survey of Formal Methods applied to IEEE 1394
Maharaj S & Shankland C (2000) A Survey of Formal Methods applied to IEEE 1394. In: Proceedings of the IEEE TC-ECBS + TF RE and IFIP WG10.1 Workshop - Joint Workshop on Formal Specifications of Computer-Based Systems. IEEE TC-ECBS + TF RE and IFIP WG10.1: Joint Workshop on Formal Specifications of Computer-Based Systems, Edinburgh, Scotland, 06.04.2000-07.04.2000. Stirling, Scotland: University of Stirling, pp. 25-26.
Article
A Survey of formal methods applied to leader election in IEEE 1394
Maharaj S & Shankland C (2000) A Survey of formal methods applied to leader election in IEEE 1394. Journal of Universal Computer Science, 6 (11), pp. 1145-1163. http://www.jucs.org/jucs_6_11/a_survey_of_formal
Conference Paper (published)
Towards a Method of Test Case Extraction from Correctness Proofs
Maharaj S (1999) Towards a Method of Test Case Extraction from Correctness Proofs. In: Proceedings of the 14th International Workshop on Algebraic Development Techniques. 14th International Workshop on Algebraic Development Techniques (WADT 1999), Chateau de Bonas, France, 15.09.1999-18.09.1999. Switzerland: Springer, pp. 45-46.
Book Chapter
On the Verification of VDM Specification and Refinement with PVS
Agerholm S, Bicarregui J & Maharaj S (1998) On the Verification of VDM Specification and Refinement with PVS. In: Bicarregui J (ed.) Proof in VDM: Case Studies. Formal Approaches to Computing and Information Technology (FACIT). London: Springer, pp. 157-189. http://link.springer.com/chapter/10.1007/978-1-4471-1532-8_6#
Conference Paper (published)
On the verification of VDM specification and refinement with PVS
Maharaj S & Bicarregui J (1997) On the verification of VDM specification and refinement with PVS. In: 12th IEEE International Conference Automated Software Engineering, 1997. Proceedings. 12th IEEE International Conference Automated Software Engineering, 1997, Incline Village, NV, USA, 01.11.1997-05.11.1997. Piscataway, NJ, USA: IEEE, pp. 280-289. http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=632849&abstractAccess=no&userType=inst; https://doi.org/10.1109/ASE.1997.632849
Thesis
A Type-theoretic Analysis of Modular Specifications
Maharaj S (1997) A Type-theoretic Analysis of Modular Specifications. Doctor of Philosophy. University of Edinburgh.
Article
Studying the ML module system in HOL
Gunter EL & Maharaj S (1995) Studying the ML module system in HOL. Computer Journal, 38 (2), pp. 142-151. https://doi.org/10.1093/comjnl/38.2.142
Conference Paper (published)
Studying the ML module system in HOL
Maharaj S & Gunter EL (1994) Studying the ML module system in HOL. In: Melham T & Camilleri J (eds.) Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop Valletta, Malta, September 19–22, 1994 Proceedings. Lecture Notes in Computer Science, 859. 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Valletta, Malta, 19.09.1994-22.09.1994. Berlin Heidelberg: Springer, pp. 346-361. http://link.springer.com/chapter/10.1007/3-540-58450-1_53#; https://doi.org/10.1007/3-540-58450-1_53
Conference Paper (published)
Encoding Z-style Schemas in Type Theory
Maharaj S (1994) Encoding Z-style Schemas in Type Theory. In: Barendregt H & Nipkow T (eds.) Types for Proofs and Programs: International Workshop TYPES'93 Nijmegen, The Netherlands, May 24–28, 1993 Selected Papers. Lecture Notes in Computer Science, 806. International Workshop TYPES'93, Nijmegen, The Netherlands, 24.05.1993-28.05.1993. Berlin Heidelberg: Springer, pp. 238-262. http://link.springer.com/chapter/10.1007/3-540-58085-9_79#; https://doi.org/10.1007/3-540-58085-9_79
Technical Report
Jones C & Maharaj S (1993) The LEGO library. University of Edinburgh. http://www.dcs.ed.ac.uk/home/lego/html/release-1.2/library/newlib.html
Technical Report
The Formal Development of an SML Program Using the LEGO Theorem-Prover
Maharaj S (1991) The Formal Development of an SML Program Using the LEGO Theorem-Prover. Bell Labs.
Thesis
Maharaj S (1990) Implementing Z in LEGO. Master of Science. University of Edinburgh.
Technical Report
A Computer Package for Studying Graph Polynomials
Maharaj S (1988) A Computer Package for Studying Graph Polynomials. Dept of Mathematics and Computer Science, University of the West Indies.
My teaching includes introductory programming in Java, software engineering and formal methods, relational database systems, and agent-based computational modelling.
