文章
使用 Sentinel-2 时间序列检测并绘制安扎利国际湿地水葫芦生长周期
Pirbasti MA、Akbari V、Bhowmik D、Maharaj S 和 Marino A (2024) 使用 Sentinel-2 时间序列检测和绘制安扎利国际湿地水葫芦生长周期。IEEE 应用地球观测和遥感专题杂志，17，第 13346 - 13357 页。https://doi.org/10.1109/jstars.2024.3427002
关于我
我在特立尼达和多巴哥长大，毕业于西印度群岛大学，获得数学和计算机科学学士学位。在短暂（但足够！）担任 COBOL 程序员之后，我来到苏格兰，在爱丁堡大学获得计算机科学硕士和博士学位。我的博士学位部分是通过在当时称为 AT&T 贝尔实验室的暑期工作获得的，在那里我在一个令人兴奋的研究部门工作，遗憾的是，该部门已不复存在。获得博士学位后（哇！），我获得了一年的 ERCIM 奖学金，这使我能够访问法国 INRIA 的 CROAP 小组和英国 RAL 的计算和信息系。然后我回到苏格兰，成为milan米兰体育的讲师。我和尼尔结婚了，我们有两个孩子，莎达和杰米。
我对使用模拟技术（包括基于代理的模拟和虚拟世界）来了解现实世界的社会经济现象感兴趣。我还致力于将交互式模拟和游戏用于科学传播、教育，以及为不同用户开发决策支持工具。我目前的项目重点关注英国和印度的树木和植物健康以及农业领域的应用。 在之前的工作中，我研究了使用形式数学技术来开发关键系统。一些特定的兴趣领域包括：使用定理证明工具，特别是基于高阶逻辑和类型论的工具，对规范、编程语言和程序进行形式推理；形式规范语言的设计和语义。我与 Thomas Wilson 和 Robert Clark 合作开展了 Omnibus 项目。我还与 Carron Shankland 和 Muffy Calder 合作研究了 LOTOS 规范语言的符号语义；与 Juan Biccaregui 一起在 PVS 定理证明中形式化 VDM；与 Elsa Gunter 一起在 HOL 定理证明器中形式化标准 ML 的语义；与爱丁堡大学的乐高小组合作；以及西印度群岛大学的爱德华·法雷尔。
活动/演示
综合验证策略：一种灵活、可配置的基于断言的软件验证方法。第三届 IEEE 软件工程和形式化方法国际会议
研究向过程代数模型添加空间性的效果。第八届过程代数和随机定时活动研讨会 (PASTA 2009)：英国爱丁堡处理代数和随机定时活动 (PASTA)http://www.dcs.ed.ac.uk/pepa/group/pastaworkshop/
用于研究感染风险态度的参与式模拟模型。 2011 年夏季计算机模拟会议 (SCSC 2011)国际建模与仿真协会
呆在家里，勤洗手：流行病动态与感染意识。夏季模拟多人会议
研究项目(4)
用于监测印度入侵水草的多模式数据分析 PI：萨维·马哈拉吉博士资助单位：英国皇家工程院 –
通过开发针对杂草入侵的预警和准备响应系统来保护东南亚国家的粮食安全 PI：萨维·马哈拉吉博士资助单位：医学科学院 –
利用严肃的游戏促进植物健康领域的公众参与和公民科学 PI：萨维·马哈拉吉博士资助方：苏格兰信息学与计算机科学联盟 –
游戏化：确定游戏的使用范围以吸引和学习 PI：萨维·马哈拉吉博士资助单位：环境食品和农村事务部 –
输出 (49)
会议论文（未发表）
Akbari V、Datta A、Bhowmik D、Marino A、Kumar S、Rupavatharam S、Prabhu GN、Kleczkowski A、R. P. Sujeetha JA 和 Maharaj S (2022) 海得拉巴 Patancheru 湖水葫芦测绘的多时相多光谱无人机图像， 印度。 Bostater CR（编辑）和 Neyt X（编辑）海洋、海冰、沿海水域和大水域遥感 2022 年，德国柏林，2022 年 9 月 5 日至 2022 年 9 月 8 日。 https://doi.org/10.1117/12.2639004
文章
使用 Dual-Pol Sentinel-1 SAR 图像检测印度库塔纳德的水葫芦侵扰
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) 使用 Dual-Pol Sentinel-1 SAR 图像检测印度库塔纳德的水葫芦侵扰。遥感，14（12），艺术。编号：2845。https://doi.org/10.3390/rs14122845
会议论文（已发布）
使用 Sentinel-1 SAR 数据监测印度库塔纳德的水葫芦
Simpson M、Marino A、Prabhu GN、Bhowmik D、Rupavatharam S、Datta A、Kleczkowski A、Sujeetha JARP 和 Maharaj S (2021) 使用 Sentinel-1 SAR 数据监测印度库塔纳德的水葫芦。在：2020 IEEE 印度地球科学与遥感研讨会 (InGARSS)。 2020 年 IEEE 国际印度地球科学与遥感研讨会 (InGARSS)，在线，2020 年 12 月 2 日至 2020 年 12 月 5 日。美国新泽西州皮斯卡塔韦：IEEE。 https://doi.org/10.1109/InGARSS48198.2020.9358977
会议论文（已发布）
Docherty C、Rutherford A、Jones G 和 Maharaj S (2021) 比较植物来源公共教育的游戏与非游戏方法。见：Gabron S（编辑）GSGS '21 - 游戏化和严肃游戏进程国际会议。游戏化和严肃游戏研讨会。 GSGS '21 - 游戏化和严肃游戏国际会议，瑞士洛桑，2021 年 6 月 28 日至 2021 年 7 月 9 日。都柏林：数字王国。 https://gsgs.ch/wp-content/uploads/2021/07/gsgs21.pdf
会议论文（已发布）
Akbari V、Simpson M、Maharaj S、Marino A、Bhowmik D、Prabhu GN、Rupavatharam S、Datta A、Kleczkowski A 和 Sujeetha JARP (2021) 利用多时相遥感数据和机器学习技术监测印度湿地的水生杂草。在：2021 IEEE 国际地球科学与遥感研讨会 IGARSS。国际地球科学与遥感研讨会 (IGARSS)，比利时，2021 年 7 月 12 日至 2021 年 7 月 16 日。美国新泽西州皮斯卡塔韦：IEEE。 https://doi.org/10.1109/IGARSS47720.2021.9553207
评论
监测水葫芦 (Pontederia crassipes) 的传播：挑战和未来发展
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) 监测水葫芦的传播 (Pontederia) crassipes）：挑战和未来发展。生态学和进化的前沿，9，艺术。编号：631338。https://doi.org/10.3389/fevo.2021.631338
文章
Ameerbakhsh O、Maharaj S、Hussain A 和 McAdam B (2019) 在大学环境中使用严肃游戏教授海洋生态学的两种方法的比较。国际人机研究杂志，127，第 181-189 页。 https://doi.org/10.1016/j.ijhcs.2018.07.004
会议论文（已发布）
Ameerbakhsh O、Maharaj S、Hussain A、Paine CET 和 Taiksi S (2016) 生态学教学交互式模拟的探索性案例研究。在：2016 第十五届国际信息技术高等教育与培训会议 (ITHET)。 ITHET 2016：第十五届基于信息技术的高等教育和培训国际会议，土耳其伊斯坦布尔，2016 年 9 月 8 日至 2016 年 9 月 10 日。美国新泽西州皮斯卡塔韦：IEEE。 https://doi.org/10.1109/ITHET.2016.7760725
演示/演讲
Maharaj S、Jones G、Greene P 和 Docherty C (2016) 游戏化促进公众参与入侵树木病虫害。2016 年第一届国际欧洲公民科学协会 (ESCA) 会议：公民科学 - 开放科学、社会和政策方面的创新，柏林，2016 年 5 月 19 日至 2016 年 5 月 21 日。
文章
生物经济“战争游戏”模型，用于模拟植物病害入侵并测试景观规模的响应策略
Cook D、Aurambout J、Villalta O、Liu S、Edwards J 和 Maharaj S (2016) 一种生物经济“战争游戏”模型，用于模拟植物病害入侵并在景观尺度上测试响应策略。粮食安全，8 (1)，第 37-48 页。 https://doi.org/10.1007/s12571-015-0524-z
文章
Williams L、Rasmussen S、Kleczkowski A、Maharaj S 和 Cairns N (2015) 针对模拟传染病流行的保护动机理论和社交疏远行为。心理学、健康和医学，20 (7)，第 832-837 页。 https://doi.org/10.1080/13548506.2015.1028946
会议论文（未发表）
Maharaj S (2015) 游戏化促进公众参与入侵树木病虫害。欧洲公民科学协会会议，柏林。
文章
Kleczkowski A、Maharaj S、Rasmussen S、Williams L 和 Cairns N (2015) 针对模拟流行病的自发社交距离：虚拟实验。BMC 公共卫生，15，艺术。编号：973。https://doi.org/10.1186/s12889-015-2336-7
研究报告
Maharaj S 和 Greene P (2015)林业委员会植物健康领域的游戏化。苏格兰林业委员会。milan米兰体育。 http://www.forestry.gov.uk/pdf/Gamification_in_the_FC.pdf/$FILE/Gamification_in_the_FC.pdf
会议论文（已发布）
网络上的战略互动和信息交换：基于代理的保护激励计划中土地所有者行为的模拟模型
Banerjee S 和 Maharaj S (2015) 网络上的战略互动和信息交换：保护激励计划中基于代理的土地所有者行为模拟模型。见：Miguel F、Amblad F、Barcelo J 和 Madella M（编辑）计算社会科学和社会模拟的进展：2014 年社会模拟会议论文集，巴塞罗那，加泰罗尼亚（西班牙），9 月 15 日。社会模拟会议，巴塞罗那自治大学，2014 年 9 月 1 日至 2014 年 9 月 5 日。巴塞罗那：巴塞罗那自治大学出版社，第 42-46 页。 http://ddd.uab.cat/pub/poncom/2014/125597/advcomsocsci_a2014.pdf
会议论文（已发布）
Delaney L、Kleczkowski A、Maharaj S、Rasmussen S 和 Williams L (2013) 对解决流行病期间人类行为的虚拟实验的思考。在：SummerSim '13 2013 夏季模拟多会议加拿大多伦多 — 2013 年 7 月 7 日至 10 日。模拟系列，45.11。 2013 年夏季计算机模拟会议，加拿大多伦多，2013 年 7 月 7 日至 2013 年 7 月 10 日。加利福尼亚州维斯塔：国际建模与仿真协会。 http://dl.acm.org/itation.cfm?id=2557732&CFID=279840820&CFTOKEN=77799498
文章
Maharaj S 和 Kleczkowski A (2012) 通过保持社交距离控制流行病传播：要么做得好，要么根本不做。BMC 公共卫生，12（679）。 https://doi.org/10.1186/1471-2458-12-679
会议论文（已发布）
Maharaj S、Kleczkowski A 和 McCaldin T (2011) 用于研究感染风险态度的参与式模拟模型。在：2011 年夏季计算机模拟会议 (SCSC 2011) 论文集。 2011 年夏季计算机模拟会议 (SCSC 2011)，荷兰海牙，2011 年 6 月 27 日至 2011 年 6 月 30 日。加利福尼亚州：国际建模与仿真学会 Vista / ACM 数字图书馆，第 8-13 页。
会议论文（已发布）
Kleczkowski A 和 Maharaj S (2010) 呆在家里，洗手：流行病动态与感染意识。在：SummerSim '10 2010 夏季模拟多会议。夏季模拟多方会议，加拿大渥太华，2010 年 7 月 1 日。圣地亚哥：国际计算机模拟协会，第 141-146 页。 http://dl.acm.org/itation.cfm?id=1999432
会议论文（已发布）
Maharaj S、McCaig C 和 Shankland C (2009) 研究向过程代数模型添加空间性的影响。见：Clark A 和 Guerriero M（编辑）第八届过程代数和随机定时活动研讨会：PASTA 2009。第八届过程代数和随机定时活动研讨会 (PASTA 2009)：英国爱丁堡，爱丁堡，2009 年 8 月 26 日至 2009 年 8 月 26 日。英国爱丁堡：爱丁堡大学，第 153-158 页。 http://www.dcs.ed.ac.uk/pepa/group/pastaworkshop/PASTA09/proceedings.pdf
技术报告
威尔逊 T、马哈拉吉 S 和克拉克 R (2009)基于断言的集成验证与 Omnibus 的案例研究。技术报告 CSM，176。milan米兰体育计算科学与数学系。
文章
Wilson T、Maharaj S 和 Clark R (2008) 使用 Omnibus 实现灵活且可配置的验证策略。软件和系统建模，7 (3)，第 257-272 页。 http://www.springerlink.com/content/9543347t1h403181/fulltext.pdf； https://doi.org/10.1007/s10270-007-0060-1
技术报告
适用于应用程序开发人员的按钮工具，适用于组件供应商的完整形式验证
威尔逊 T、马哈拉吉 S 和克拉克 R (2007)适用于应用程序开发人员的按钮工具，适用于组件供应商的完整形式验证。技术报告 CSM，167。milan米兰体育计算科学与数学系。
其他
Maharaj S（编辑）、Shankland C（编辑）和 Rattray C（编辑）（2006 年）理论计算机科学。理论计算机科学，351（2）。 http://www.sciencedirect.com/science/journal/03043975/351/2
会议论文（已发布）
Omnibus：一种干净的语言和支持工具，用于集成不同的基于断言的验证技术
Wilson T、Maharaj S 和 Clark R (2005) Omnibus：一种干净的语言和支持工具，用于集成不同的基于断言的验证技术。见：Butler M、Jones C、Romanovsky A 和 Troubisyna E（编辑）容错系统严格工程研讨会论文集 (REFT 2005)。技术报告系列，CS-TR-915。容错系统严格工程研讨会 (REFT 2005)，纽卡斯尔，2005 年 7 月 19 日至 2005 年 7 月 19 日。泰恩河畔纽卡斯尔：泰恩河畔纽卡斯尔大学，第 43-52 页。 http://rodin.cs.ncl.ac.uk/REFT.htm
会议论文（已发布）
Bujorianu ML、Bujorianu MC 和 Maharaj S (2005) 分布式随机混合系统。见：Zitek P（编辑）第 16 届 IFAC 世界大会论文集，2005 年。 IFAC 会议记录卷，16。国际自动化与控制联合会第 16 届世界大会 (IFAC 2005)，捷克共和国，2005 年 7 月 4 日至 2005 年 7 月 8 日。阿姆斯特丹：Elsevier 国际自动控制联合会，第 158-163 页。 http://www.ifac-papersonline.net/Detailed/27660.html
会议论文（已发布）
Wilson T、Maharaj S 和 Clark R (2005) 综合验证策略：一种灵活、可配置的基于断言的软件验证方法。载于：Aichernig B 和 Beckert B（编辑）SEFM 2005：第三届 IEEE 软件工程和形式化方法国际会议，论文集。第三届 IEEE 软件工程和形式方法国际会议，德国科布伦茨，2005 年 9 月 7 日至 2005 年 9 月 9 日。加利福尼亚州洛斯阿拉米托斯：电气和电子工程师协会，第 150-159 页。 http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=10529
编辑过的会议记录
代数方法论和软件技术：第 10 届国际会议，AMAST 2004，英国苏格兰milan米兰体育官网，2004 年 7 月 12 日至 16 日。会议记录
Rattray C、Maharaj S 和 Shankland C（编辑）(2004)代数方法论和软件技术：第 10 届国际会议，AMAST 2004，英国苏格兰milan米兰体育官网，2004 年 7 月 12 日至 16 日。会议记录。计算机科学讲义，3116。AMAST'2004 - 第十届代数方法和软件技术国际会议。柏林海德堡：施普林格。
文章
Maharaj S、Romijn J 和 Shankland C (2003) IEEE 1394 树识别协议：案例研究简介。计算的形式方面，14 (3)，第 200-214 页。 https://doi.org/10.1007/s001650300001
其他
应用于 IEEE 1394 的形式方法：比较案例研究。计算的形式方面特刊
Cooke J（编辑）、Maharaj S（编辑）、Romijn J（编辑）和 Shankland C（编辑）(2003) 应用于 IEEE 1394 的形式方法：比较案例研究。计算的形式方面特刊。计算的形式方面，14（3）。 http://link.springer.com/journal/165/14/3
会议论文（已发布）
Bujorianu MC、Maharaj S 和 Bujorianu ML (2002) 迈向观点测试的形式化。见：Hierons R 和 Thierry J（编辑）软件测试的正式方法：FATES’02 CONCUR’02 卫星研讨会，捷克共和国布尔诺，2002 年 8 月 24 日会议记录。 FATES’02：CONCUR’02 卫星研讨会，捷克共和国布尔诺，2002 年 8 月 24 日至 2002 年 8 月 24 日。瑞士：Springer，第 137-151 页。 http://kar.kent.ac.uk/13752/1/FormalRob.pdf
文章
Calder M、Maharaj S 和 Shankland C (2002) 基于符号转换系统的完整 LOTOS 模态逻辑。计算机杂志，45 (1)，第 55-61 页。 https://doi.org/10.1093/comjnl/45.1.55
编辑过的会议记录
IEEE 1394（火线）研讨会：形式化方法在 IEEE 1394 标准中的应用国际研讨会
Shankland C、Romijn J 和 Maharaj S（编辑）(2001)IEEE 1394（火线）研讨会：形式化方法在 IEEE 1394 标准中的应用国际研讨会。 IEEE 1394 (FireWire) 研讨会：IEEE 1394 标准形式化方法应用国际研讨会，苏格兰milan米兰体育官网，2001 年 3 月 13 日至 2001 年 3 月 13 日。苏格兰milan米兰体育官网：milan米兰体育计算科学与数学系。
会议论文（已发布）
Calder M、Maharaj S 和 Shankland C (2001) 完整 LOTOS 的充分逻辑。见：Oliveira J 和 Zave P（编辑）FME 2001：提高软件生产力的形式化方法。计算机科学讲义，2021 年。欧洲形式方法国际研讨会，德国柏林，2001 年 3 月 12 日至 2001 年 3 月 16 日。柏林海德堡：Springer，第 384-395 页。 http://link.springer.com/chapter/10.1007/3-540-45251-6_21
会议论文（已发布）
Maharaj S (2001) 符号转换系统的 PVS 理论。见：Boulton R 和 Jackson P（编辑）高阶逻辑中的定理证明，2001 年，补充论文集。高阶逻辑定理证明：第 14 届国际会议，TPHOLs 2001，苏格兰爱丁堡，2001 年 9 月 3 日至 2001 年 9 月 6 日。苏格兰爱丁堡：爱丁堡大学信息学部，第 255-266 页。 http://www.inf.ed.ac.uk/publications/online/0046/
会议论文（已发布）
Maharaj S 和 Shankland C (2000) 适用于 IEEE 1394 的形式方法调查。见：IEEE TC-ECBS + TF RE 和 IFIP WG10.1 研讨会论文集 - 基于计算机的系统正式规范联合研讨会。 IEEE TC-ECBS + TF RE 和 IFIP WG10.1：基于计算机的系统正式规范联合研讨会，苏格兰爱丁堡，2000 年 4 月 6 日至 2000 年 4 月 7 日。苏格兰milan米兰体育官网：milan米兰体育，第 25-26 页。
文章
Maharaj S 和 Shankland C (2000) IEEE 1394 中应用于领导者选举的正式方法的调查。通用计算机科学杂志，6 (11)，第 1145-1163 页。 http://www.jucs.org/jucs_6_11/a_survey_of_formal
会议论文（已发布）
Maharaj S (1999) 走向从正确性证明中提取测试用例的方法。在：第十四届国际代数展开技术研讨会论文集。第 14 届国际代数展开技术研讨会 (WADT 1999)，法国博纳斯城堡，1999 年 9 月 15 日至 1999 年 9 月 18 日。瑞士：Springer，第 45-46 页。
书籍章节
Agerholm S、Bicarregui J 和 Maharaj S (1998) 关于 VDM 规范的验证和使用 PVS 的细化。见：Bicarregui J（编辑）VDM 中的证明：案例研究。计算和信息技术的正式方法（FACIT）。伦敦：Springer，第 157-189 页。 http://link.springer.com/chapter/10.1007/978-1-4471-1532-8_6#
会议论文（已发布）
Maharaj S 和 Bicarregui J (1997) 关于使用 PVS 验证 VDM 规范和细化。在：第十二届 IEEE 国际会议自动化软件工程，1997 年。论文集。第 12 届 IEEE 国际会议自动化软件工程，1997 年，美国内华达州 Incline Village，1997 年 11 月 1 日至 1997 年 11 月 5 日。美国新泽西州皮斯卡塔韦：IEEE，第 280-289 页。 http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=632849&abstractAccess=no&userType=inst; https://doi.org/10.1109/ASE.1997.632849
论文
马哈拉吉 S (1997)模块化规范的类型理论分析。哲学博士。爱丁堡大学。
文章
Gunter EL 和 Maharaj S (1995) 研究 HOL 中的 ML 模块系统。计算机杂志，38 (2)，第 142-151 页。 https://doi.org/10.1093/comjnl/38.2.142
会议论文（已发布）
Maharaj S (1994) 在类型理论中编码 Z 样式模式。见：Barendregt H 和 Nipkow T（编辑）证明和程序的类型：国际研讨会 TYPES'93，荷兰奈梅亨，1993 年 5 月 24 日至 28 日 论文选集。计算机科学讲义，806。国际研讨会 TYPES'93，荷兰奈梅亨，1993 年 5 月 24 日至 1993 年 5 月 28 日。柏林海德堡：Springer，第 238-262 页。 http://link.springer.com/chapter/10.1007/3-540-58085-9_79#； https://doi.org/10.1007/3-540-58085-9_79
会议论文（已发布）
Maharaj S 和 Gunter EL (1994) 研究 HOL 中的 ML 模块系统。见：Melham T 和 Camilleri J（编辑）高阶逻辑定理证明及其应用：第七届国际研讨会，马耳他瓦莱塔，1994 年 9 月 19 日至 22 日会议记录。计算机科学讲义，859。第七届高阶逻辑定理证明及其应用国际研讨会，马耳他瓦莱塔，1994 年 9 月 19 日至 1994 年 9 月 22 日。柏林海德堡：Springer，第 346-361 页。 http://link.springer.com/chapter/10.1007/3-540-58450-1_53#； https://doi.org/10.1007/3-540-58450-1_53
技术报告
琼斯 C 和马哈拉吉 S (1993)乐高图书馆。爱丁堡大学。 http://www.dcs.ed.ac.uk/home/lego/html/release-1.2/library/newlib.html
技术报告
马哈拉吉 S (1991)使用乐高定理证明器正式开发 SML 程序。贝尔实验室。
论文
马哈拉吉 S (1990)在乐高中实现 Z。理学硕士。爱丁堡大学。
技术报告
马哈拉吉 S (1988)用于研究图多项式的计算机软件包。西印度群岛大学数学与计算机科学系。
教学
我的教学包括 Java 编程入门、软件工程和形式化方法、关系数据库系统以及基于代理的计算建模。