Shaun Azzopardi

@misc{kharraz2023synchronous,
      title={Synchronous Agents, Verification, and Blame -- A Deontic View}, 
      author={Karam Kharraz and Shaun Azzopardi and Gerardo Schneider and Martin Leucker},
      year={2023},
      eprint={2309.14048},
      archivePrefix={arXiv},
      booktitle={arXiv},
      primaryClass={cs.LO},
      url={https://arxiv.org/abs/2309.14048}
}

@inproceedings{azzopardi2023ictac,
      title={Synchronous Agents, Verification, and Blame --- A Deontic View},
      author={Kharraz, Karam and Azzopardi, Shaun and Leucker, Martin and Schneider, Gerardo},
      year={2023},
      booktitle={ICTAC 2023}
}

@inproceedings{azzopardi2023sttt,
      title={Language Support for Verifying Reconfigurable Interacting Systems}, 
      author={Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir and di Stefano, Luca},
      year={2023},
      booktitle={International Journal on Software Tools for Technology Transfer (STTT), FoMaC, Special Issues, REoCAS 2022}
}

@misc{azzopardi2023ltl,
      title={LTL Synthesis on Infinite-State Arenas defined by Programs}, 
      author={Azzopardi, Shaun and Piterman, Nir and Schneider, Gerardo and di Stefano, Luca},
      year={2023},
      eprint={2307.09776},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      booktitle={arXiv},
      url={https://arxiv.org/abs/2307.09776},
      doi={10.48550/arXiv.2307.09776}
}

@inproceedings{atva23,
title={ppLTLTT: Temporal testing for pure-past linear temporal logic formulae}, 
author={Lidell, David and Azzopardi, Shaun and Piterman, Nir and Schneider, Gerardo},
year="2023",
booktitle="Automated Technology for Verification and Analysis (ATVA)"
}

@misc{alrahman2022rcheck,
      title={R-CHECK: A Model Checker for Verifying Reconfigurable MAS}, 
      author={Yehia Abd Alrahman and Shaun Azzopardi and Nir Piterman},
      year={2022},
      eprint={2201.06312},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      booktitle={arXiv},
      url={https://arxiv.org/abs/2201.06312}
}

@inproceedings{isola-1,
title={Model Checking Reconfigurable Interacting Systems}, 
author={Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir},
year="2022",
booktitle="International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74143/319774.pdf"
}

@inproceedings{isola-2,
title={Runtime Verification meets Controller Synthesis}, 
author={Azzopardi, Shaun and Piterman, Nir, and Schneider, Gerardo},
year="2022",
booktitle="International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74142/319773.pdf?sequence=1&isAllowed=y"
}

@inproceedings{rv22-1,
title={AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification}, 
author={Shaun Azzopardi, Joshua Ellul, Ryan Falzon and Gordon Pace},
year="2022",
booktitle="22nd International Conference on Runtime Verification (RV)",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74146/319770.pdf?sequence=1&isAllowed=y"
}

@inproceedings{rv22-2,
title={Tainting in Smart Contracts: Combining Static and Runtime Verification}, 
author={Shaun Azzopardi, Joshua Ellul, Ryan Falzon and Gordon Pace},
year="2022",
booktitle="22nd International Conference on Runtime Verification (RV)",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74145/319772.pdf?sequence=1"
}

@inproceedings{rv22-3,
title={Runtime Verification of Kotlin Coroutines}, 
author={Denis Furian, Shaun Azzopardi, Yliès Falcone, and Gerardo Schneider},
year="2022",
booktitle="22nd International Conference on Runtime Verification (RV)",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74147/319771.pdf?sequence=1&isAllowed=y"
}

@inproceedings{10.5555/3535850.3536020,
author = {Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir},
title = {R-CHECK: A Model Checker for Verifying Reconfigurable MAS},
year = {2022},
isbn = {9781450392136},
publisher = {International Foundation for Autonomous Agents and Multiagent Systems},
address = {Richland, SC},
abstract = {Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system-level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.},
booktitle = {Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems},
pages = {1518–1520},
numpages = {3},
keywords = {verification of multi-agent systems, logics for agent reasoning, agent theories and models},
location = {Virtual Event, New Zealand},
series = {AAMAS '22},
url="https://www.ifaamas.org/Proceedings/aamas2022/pdfs/p1518.pdf"
}

Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system-level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.

@misc{azzopardi2021incorporating,
      title={Incorporating Monitors in Reactive Synthesis without Paying the Price}, 
      author={Shaun Azzopardi and Nir Piterman and Gerardo Schneider},
      year={2021},
      eprint={2107.00929},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      booktitle={arXiv},
      url={https://arxiv.org/abs/2107.00929}
}

@inproceedings{rv21,
author="Azzopardi, Shaun
and Pace, Gordon
and Schapachnik, Fernando
and Schneider, Gerardo",
editor="Feng, Lu
and Fisman, Dana",
title="On the Specification and Monitoring of Timed Normative Systems",
booktitle="Runtime Verification (RV)",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="81--99",
abstract="In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.",
isbn="978-3-030-88494-9",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74148/309362.pdf?sequence=1"
}

In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.

@inproceedings{atva21,
author="Azzopardi, Shaun
and Piterman, Nir
and Schneider, Gerardo",
editor="Hou, Zhe
and Ganesh, Vijay",
title="Incorporating Monitors in Reactive Synthesis Without Paying the Price",
booktitle="Automated Technology for Verification and Analysis",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="337--353",
abstract="Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.",
isbn="978-3-030-88885-5",
url="https://gupea.ub.gu.se/bitstream/handle/2077/74140/305933.pdf"
}

Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language.

@InProceedings{10.1007/978-3-030-67445-8_14,
	author="Azzopardi, Shaun
	and Colombo, Christian
	and Pace, Gordon",
	editor="Hammoudi, Slimane
	and Pires, Lu{\'i}s Ferreira
	and Seli{\'{c}}, Bran",
	title="Model-Based Static and Runtime Verification for Ethereum Smart Contracts",
	booktitle="Model-Driven Engineering and Software Development",
	year="2021",
	publisher="Springer International Publishing",
	address="Cham",
	pages="323--348",
	abstract="Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context -- blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.",
	isbn="978-3-030-67445-8"
}

Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context – blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.

@inproceedings{rvblockchains,
author="Azzopardi, Shaun
and Ellul, Joshua
and Pace, Gordon J.",
editor="Hojjat, Hossein
and Massink, Mieke",
title="Runtime Monitoring Processes Across Blockchains",
booktitle="Fundamentals of Software Engineering",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="142--156",
abstract="Business processes have been long researched, with many tools, languages, and diagrammatic notations having been developed for automation. Recently, distributed ledger technology (of which Blockchain is one type) has been proposed for use in the monitoring of business process compliance. Such a set-up is attractive since it allows for immutability and thus a perfect record of the history of the business process regulated.",
isbn="978-3-030-89247-0",
url = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/fsen2021.pdf}
}

Business processes have been long researched, with many tools, languages, and diagrammatic notations having been developed for automation. Recently, distributed ledger technology (of which Blockchain is one type) has been proposed for use in the monitoring of business process compliance. Such a set-up is attractive since it allows for immutability and thus a perfect record of the history of the business process regulated.

@inproceedings{clarvatheory,
  author    = {Shaun Azzopardi and
                Christian Colombo and
                Gordon Pace},
  title     = {A Technique for Automata-Based Verification with Residual Reasoning},
  booktitle = {Proceedings of the 8th International Conference on Model-Driven Engineering
               and Software Development, {MODELSWARD} 2020, Valletta, Malta,
               February 25-27, 2020},
  year      = {2020},
  url  = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/modelsward2020a.pdf},
  doi = {10.5220/0008981902370248}
}

@inproceedings{clarvatool,
  author    = {Shaun Azzopardi and
                Christian Colombo and
                Gordon Pace},
  title     = {CLARVA: Model-Based Residual Verification of Java Programs},
  booktitle = {Proceedings of the 8th International Conference on Model-Driven Engineering
               and Software Development, {MODELSWARD} 2020, Valletta, Malta,
               February 25-27, 2020},
  year      = {2020},
  url = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/modelsward2020b.pdf},
  doi = {10.5220/0008966603520359}
}

@InProceedings{Shaun_Azzopardi48593129,
author="Azzopardi, Shaun
and Ellul, Joshua
and Pace, Gordon J.",
editor="Colombo, Christian
and Leucker, Martin",
title="Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond",
booktitle="Runtime Verification",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="113--137",
abstract="Smart contracts present new challenges for runtime verification techniques, due to features such as immutability of the code and the notion of gas that must be paid for the execution of code. In this paper we present the runtime verification tool ContractLarva and outline its use in instrumenting monitors in smart contracts written in Solidity, for the Ethereum blockchain-based distributed computing platform. We discuss the challenges faced in doing so, and how some of these can be addressed, using the ERC-20 token standard to illustrate the techniques. We conclude by proposing a list of open challenges in smart contract and blockchain monitoring.",
isbn="978-3-030-03769-7",
url="https://doi.org/10.1007/978-3-030-03769-7_8"
}

Smart contracts present new challenges for runtime verification techniques, due to features such as immutability of the code and the notion of gas that must be paid for the execution of code. In this paper we present the runtime verification tool ContractLarva and outline its use in instrumenting monitors in smart contracts written in Solidity, for the Ethereum blockchain-based distributed computing platform. We discuss the challenges faced in doing so, and how some of these can be addressed, using the ERC-20 token standard to illustrate the techniques. We conclude by proposing a list of open challenges in smart contract and blockchain monitoring.

@inproceedings{DBLP:conf/jurix/AzzopardiPS18,
  author    = {Shaun Azzopardi and
               Gordon J. Pace and
               Fernando Schapachnik},
  title     = {On Observing Contracts: Deontic Contracts Meet Smart Contracts},
  booktitle = {Legal Knowledge and Information Systems - {JURIX} 2018: The Thirty-first
               Annual Conference, Groningen, The Netherlands, 12-14 December 2018.},
  pages     = {21--30},
  year      = {2018},
  crossref  = {DBLP:conf/jurix/2018},
  url       = {https://doi.org/10.3233/978-1-61499-935-5-21},
  doi       = {10.3233/978-1-61499-935-5-21},
  timestamp = {Sun, 16 Dec 2018 18:16:27 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/jurix/AzzopardiPS18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cnl/AzzopardiCP18, author= {Shaun Azzopardi and
               Christian Colombo and
               Gordon J. Pace}, title= {A Controlled Natural Language for Financial Services Compliance Checking}, booktitle= {Controlled Natural Language - Proceedings of the Sixth International
               Workshop, {CNL} 2018, Maynooth, Co. Kildare, Ireland, August 27-28,
               2018}, pages= {11--20}, year= {2018}, crossref= {DBLP:conf/cnl/2018}, url= {https://doi.org/10.3233/978-1-61499-904-1-11}, doi= {10.3233/978-1-61499-904-1-11}, timestamp= {Thu, 23 Aug 2018 17:14:17 +0200}, biburl= {https://dblp.org/rec/bib/conf/cnl/AzzopardiCP18}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@article{Azzopardi_2017,
	year = 2017,

      eprint={1708.06889},
      archivePrefix={arXiv},
      primaryClass={cs.LO},
      booktitle={arXiv},
      url={https://arxiv.org/abs/1708.07230},
      author = {Shaun Azzopardi and Christian Colombo and Gordon J. Pace},
      title = {Control-Flow Residual Analysis for Symbolic Automata}
}

@inproceedings{DBLP:conf/rv/AzzopardiCEMP17, 
            author= {Shaun Azzopardi and
               Christian Colombo and
               Jean{-}Paul Ebejer and
               Edward Mallia and
               Gordon J. Pace}, 
            title= {Runtime Verification using {VALOUR}}, booktitle= {RV-CuBES 2017. An International Workshop on Competitions, Usability,
               Benchmarks, Evaluation, and Standardisation for Runtime Verification
               Tools, September 15, 2017, Seattle, WA, {USA}}, pages= {10--18}, year= {2017}, crossref= {DBLP:conf/rv/2017cubes}, url= {	https://doi.org/10.29007/bwd4}, timestamp= {Tue, 16 Jan 2018 18:09:01 +0100}, biburl= {https://dblp.org/rec/bib/conf/rv/AzzopardiCEMP17}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@inproceedings{DBLP:journals/corr/abs-1708-07230, author= {Shaun Azzopardi and
               Christian Colombo and
               Gordon J. Pace}, title= {Control-Flow Residual Analysis for Symbolic Automata}, booktitle= {Proceedings Second International Workshop on Pre- and Post-Deployment
               Verification Techniques, PrePost@iFM 2017, Torino, Italy, 19 September
               2017.}, pages= {29--43}, year= {2017}, crossref= {DBLP:journals/corr/abs-1708-06889}, url= {https://doi.org/10.4204/EPTCS.254.3}, doi= {10.4204/EPTCS.254.3}, timestamp= {Wed, 12 Sep 2018 01:00:00 +0200}, biburl= {https://dblp.org/rec/bib/journals/corr/abs-1708-07230}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@inproceedings{clarva-csaw,
	title={Residual Control-Flow Static Analysis with Symbolic Automata},
	year={2016},
	booktitle={CSAW 2016: Computer Science Annual Workshop 2016, University of Malta, Malta},
	author={Shaun Azzopardi and
	Christian Colombo and
	Gordon J. Pace}
}

@inproceedings{ope-csaw,
	title={Regulation specification and automatic static and dynamic checks generation in the OPE},
	year={2016},
	booktitle={CSAW 2016: Computer Science Annual Workshop 2016, University of Malta, Malta},
	author={Shaun Azzopardi and
	Christian Colombo and
	Gordon J. Pace}
}

@inproceedings{DBLP:conf/jurix/AzzopardiGP16, author= {Shaun Azzopardi and
               Albert Gatt and
               Gordon J. Pace}, title= {Reasoning About Partial Contracts}, booktitle= {Legal Knowledge and Information Systems - {JURIX} 2016: The Twenty-Ninth
               Annual Conference}, pages= {23--32}, year= {2016}, crossref= {DBLP:conf/jurix/2016}, url= {https://doi.org/10.3233/978-1-61499-726-9-23}, doi= {10.3233/978-1-61499-726-9-23}, timestamp= {Thu, 25 May 2017 01:00:00 +0200}, biburl= {https://dblp.org/rec/bib/conf/jurix/AzzopardiGP16}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@inproceedings{DBLP:conf/isola/AzzopardiCP16, author= {Shaun Azzopardi and
               Christian Colombo and
               Gordon J. Pace}, title= {A Model-Based Approach to Combining Static and Dynamic Verification
               Techniques}, booktitle= {Leveraging Applications of Formal Methods, Verification and Validation:
               Foundational Techniques - 7th International Symposium, ISoLA 2016,
               Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part {I}}, pages= {416--430}, year= {2016}, crossref= {DBLP:conf/isola/2016-1}, url= {https://doi.org/10.1007/978-3-319-47166-2\_29}, doi= {10.1007/978-3-319-47166-2\_29}, timestamp= {Tue, 23 May 2017 01:12:13 +0200}, biburl= {https://dblp.org/rec/bib/conf/isola/AzzopardiCP16}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@conference{Shaun_Azzopardi48593036,
title={Integrating Natural Language and Formal Analysis for Legal Documents},
booktitle={10th Conference on Language Technologies and Digital Humanities 2016, Ljubljana, Slovenia},
author={Shaun Azzopardi and Albert Gatt and  Gordon Pace},
year={2016},
url="https://www.um.edu.mt/library/oar/handle/123456789/22605"
}

@inproceedings{DBLP:conf/sefm/AzzopardiCPV16, author= {Shaun Azzopardi and
               Christian Colombo and
               Gordon J. Pace and
               Brian Vella}, title= {Compliance Checking in the Open Payments Ecosystem}, booktitle= {Software Engineering and Formal Methods - 14th International Conference,
               {SEFM} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 4-8,
               2016, Proceedings}, pages= {337--343}, year= {2016}, crossref= {DBLP:conf/sefm/2016}, url= {https://doi.org/10.1007/978-3-319-41591-8\_23}, doi= {10.1007/978-3-319-41591-8\_23}, timestamp= {Sun, 21 May 2017 01:00:00 +0200}, biburl= {https://dblp.org/rec/bib/conf/sefm/AzzopardiCPV16}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@article{DBLP:journals/ail/AzzopardiPSS16, author= {Shaun Azzopardi and
               Gordon J. Pace and
               Fernando Schapachnik and
               Gerardo Schneider}, title= {Contract automata - An operational view of contracts between interactive
               parties}, journal= {Artificial Intelligence and Law}, volume= {24}, number= {3}, pages= {203--243}, year= {2016}, url= {https://doi.org/10.1007/s10506-016-9185-2}, doi= {10.1007/s10506-016-9185-2}, timestamp= {Sat, 16 Sep 2017 01:00:00 +0200}, biburl= {https://dblp.org/rec/bib/journals/ail/AzzopardiPSS16}, bibsource= {dblp computer science bibliography, https://dblp.org}}

@InProceedings{csaw-masters,
	title={Formally Analysing Natural Language Contracts},
	year={2015},
	booktitle={CSAW 2015: Computer Science Annual Workshop 2015, University of Malta, Malta},
	author={Shaun Azzopardi and
	Albert Gatt and
	Gordon J. Pace}
}

@InProceedings{ope-csaw-1,
	title={Compliance Checking in the Open Payments Ecosystem},
	year={2015},
	booktitle={CSAW 2015: Computer Science Annual Workshop 2015, University of Malta, Malta},
	author={Shaun Azzopardi and
	Christian Colombo and
	Gordon J. Pace and
	Brian Vella},
  url="https://www.um.edu.mt/library/oar/bitstream/123456789/23982/1/Compliance%20Checking%20in%20the%20Open%20Payments%20Ecosystem.pdf"
}

@inproceedings{DBLP:conf/jurix/AzzopardiPS14, author= {Shaun Azzopardi and
               Gordon J. Pace and
               Fernando Schapachnik}, title= {Contract Automata with Reparations}, booktitle= {Legal Knowledge and Information Systems - {JURIX} 2014: The Twenty-Seventh
               Annual Conference, Jagiellonian University, Krakow, Poland, 10-12
               December 2014}, pages= {49--54}, year= {2014}, crossref= {DBLP:conf/jurix/2014}, url= {https://doi.org/10.3233/978-1-61499-468-8-49}, doi= {10.3233/978-1-61499-468-8-49}, timestamp= {Thu, 25 May 2017 01:00:00 +0200}, biburl= {https://dblp.org/rec/bib/conf/jurix/AzzopardiPS14}, bibsource= {dblp computer science bibliography, https://dblp.org}}