Shaun Azzopardi


About

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

I am interested in the application of formal methods for the modelling, analysis, verification, and synthesis of programs, smart contracts, and legal contracts.


Current projects:

  • Synthesising controllers meant to act against infinite-state programs
  • Compositional reactive synthesis for LTL extended to ω-regularity
  • Reactive synthesis for Past LTL
  • Comparison of row- and column-oriented data stores for financial quantitative analysis workloads
  • Verification and analysis of reconfigurable interacting systems
  • Who's to blame for a violation in a multi-agent setting?

News

  • [Aug22] Accepted for publication in International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) 2022:
    1. "Model Checking Reconfigurable Interacting Systems", with Yehia Abd Alrahman and Nir Piterman;
    2. "Runtime Verification meets Controller Synthesis", with Nir Piterman and Gerardo Schneider; and
  • [Jun22] Accepted for publication in Runtime Verification (RV) 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.
  • [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.

Publications