News

• [Jun22] Accepted for publication in Runtime Verification 2022:
  1. "AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification", with Joshua Ellul, Ryan Falzon and Gordon Pace;
  2. "Tainting in Smart Contracts: Combining Static and Runtime Verification", with Joshua Ellul, Ryan Falzon and Gordon Pace; and
  3. "Runtime Verification of Kotlin Coroutines", with Denis Furian, Yliès Falcone and Gerardo Schneider.
• [Jun22] Participating in Highlights 2022, presenting: "How to synthesise when your Environment is a Program", ongoing work about applying reactive synthesis in the context of rich environments through the use of abstraction and a counter-example guided abstraction refinement loop, with Nir Piterman and Gerardo Schneider.
• [Jan22] Accepted for publication: "R-CHECK: A Model Checker for Verifying Reconfigurable MAS" by Yehia Abd Alrahman, Shaun Azzopardi, and Nir Piterman, to appear in AAMAS (International Conference on Autonomous Agents and Multiagent Systems) 2022.
  • Preprint here.
• [Jul21] Accepted for publication: "On the Specification and Monitoring of Timed Normative Systems" by Shaun Azzopardi, Gordon Pace, Fernando Schapachnik, and Gerardo Schneider, to appear in RV (Runtime Verification) 2021.
  • Online presentation here.
• [Jun21] Accepted for publication: "Incorporating Monitors in Reactive Synthesis without Paying the Price" by Shaun Azzopardi, Nir Piterman, and Gerardo Schneider, to appear in ATVA (Automated Technology for Verification and Analysis) 2021 (full version with proofs).
  • This work will also be presented at Highlights 2021 (extended abstract).
  • Online presentation here.
• [Apr21] Published a prototype of the syMTri tool.
• [Jan-May21] I'm visiting at the Simons Institute's Theoretical Foundations of Computer Systems program.
• [Dec20] Runtime Monitoring Processes Across Blockchains was accepted at FSEN 2021.
• [Oct20] Model-based Static and Runtime Verification for Ethereum Smart Contracts will be published in Springer's CCIS 1361, as part of a collection of selected revised papers from MODELSWARD 2020.

Research Interests

I am interested in the application of formal methods for the modelling, analysis, and verification of programs, smart contracts, and legal contracts. I am also interested in the application of blockchain to real-world problems.

Service

• VMCAI 21 - Artifact Committee Member
• CONCUR 20 - Reviewer
• RV 17, 20, 21 - Reviewer
• SEFM 21 - Reviewer
• FMSD, STTT - Reviewer

Teaching

• University of Gothenburg / Chalmers University:
  • TDA567/DIT082 (2020) - Testing, Debugging, and Verification
• University of Malta (Teaching Assistant):
  • CPS1002/5200 (2016-2020) - Mathematics of Discrete Structures
  • CPS1005 (2016-2020) - Mathematics of Discrete Structures
  • ICT3009 (2019-2020) - Blockchain and Smart Contracts

Tools

• syMTri: A tool utilising synthesis to concretise parts of a system --- currently considers systems specified as sequential combinations of (concrete/imperative) rich symbolic automata and (declarative) LTL specifications, and applies reactive synthesis to the LTL parts to complete the system.
• CLarva: Performs partial static analysis of symbolic Java monitors (used mainly as a pre-processing step for the Larva monitoring tool).
• solidCLarva: A counterpart to CLarva for the Solidity smart contract language (used mainly as a pre-processing step for the contractLarva monitoring tool).
• Solidity CFG Builder: Builds control-flow graphs (as data structures and visualisations) of Solidity smart contracts.
• bpmn_to_solidity: Compiles BPMN process models into Solidity smart contracts.
• Partial DL Conflict Finder: Performs best-attempt conflict checking of partial deontic logic formulas.
• contractLarva: Interleaves Solidity smart contracts with symbolic monitoring or enforcing logic.

Education

Ph.D. in Computer Science (University of Malta 2016-2020)