Shaun Azzopardi


I am a postdoctoral researcher at the Formal Methods unit of the Department of Computer Science and Engineering, University of Gothenburg/Chalmers, working on the ERC Consolidator Project dSynMA (Distributed Synthesis from Single to Multiple Agents), led by Nir Piterman.

News

  • [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).
  • [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)

Publications