var bibbase_data = {"data":"\"Loading..\"\n\n
\n\n \n\n \n\n \n \n\n \n\n \n \n\n \n\n \n
\n generated by\n \n \"bibbase.org\"\n\n \n
\n \n\n
\n\n \n\n\n
\n\n Excellent! Next you can\n create a new website with this list, or\n embed it in an existing web page by copying & pasting\n any of the following snippets.\n\n
\n JavaScript\n (easiest)\n
\n \n <script src=\"https://bibbase.org/show?bib=https://raw.githubusercontent.com/shaunazzopardi/shaunazzopardi.github.io/master/pubs.bib&jsonp=1&jsonp=1\"></script>\n \n
\n\n PHP\n
\n \n <?php\n $contents = file_get_contents(\"https://bibbase.org/show?bib=https://raw.githubusercontent.com/shaunazzopardi/shaunazzopardi.github.io/master/pubs.bib&jsonp=1\");\n print_r($contents);\n ?>\n \n
\n\n iFrame\n (not recommended)\n
\n \n <iframe src=\"https://bibbase.org/show?bib=https://raw.githubusercontent.com/shaunazzopardi/shaunazzopardi.github.io/master/pubs.bib&jsonp=1\"></iframe>\n \n
\n\n

\n For more details see the documention.\n

\n
\n
\n\n
\n\n This is a preview! To use this list on your own web site\n or create a new web site from it,\n create a free account. The file will be added\n and you will be able to edit it in the File Manager.\n We will show you instructions once you've created your account.\n
\n\n
\n\n

To the site owner:

\n\n

Action required! Mendeley is changing its\n API. In order to keep using Mendeley with BibBase past April\n 14th, you need to:\n

    \n
  1. renew the authorization for BibBase on Mendeley, and
  2. \n
  3. update the BibBase URL\n in your page the same way you did when you initially set up\n this page.\n
  4. \n
\n

\n\n

\n \n \n Fix it now\n

\n
\n\n
\n\n\n
\n \n \n
\n
\n  \n 2023\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Synchronous Agents, Verification, and Blame – A Deontic View.\n \n \n \n \n\n\n \n Kharraz, K.; Azzopardi, S.; Schneider, G.; and Leucker, M.\n\n\n \n\n\n\n 2023.\n \n\n\n\n
\n\n\n\n \n \n \"SynchronousPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@misc{kharraz2023synchronous,\n      title={Synchronous Agents, Verification, and Blame -- A Deontic View}, \n      author={Karam Kharraz and Shaun Azzopardi and Gerardo Schneider and Martin Leucker},\n      year={2023},\n      eprint={2309.14048},\n      archivePrefix={arXiv},\n      booktitle={arXiv},\n      primaryClass={cs.LO},\n      url={https://arxiv.org/abs/2309.14048}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Synchronous Agents, Verification, and Blame — A Deontic View.\n \n \n \n\n\n \n Kharraz, K.; Azzopardi, S.; Leucker, M.; and Schneider, G.\n\n\n \n\n\n\n In ICTAC 2023, 2023. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{azzopardi2023ictac,\n      title={Synchronous Agents, Verification, and Blame --- A Deontic View},\n      author={Kharraz, Karam and Azzopardi, Shaun and Leucker, Martin and Schneider, Gerardo},\n      year={2023},\n      booktitle={ICTAC 2023}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Language Support for Verifying Reconfigurable Interacting Systems.\n \n \n \n\n\n \n Abd Alrahman, Y.; Azzopardi, S.; Piterman, N.; and di Stefano, L.\n\n\n \n\n\n\n In International Journal on Software Tools for Technology Transfer (STTT), FoMaC, Special Issues, REoCAS 2022, 2023. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{azzopardi2023sttt,\n      title={Language Support for Verifying Reconfigurable Interacting Systems}, \n      author={Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir and di Stefano, Luca},\n      year={2023},\n      booktitle={International Journal on Software Tools for Technology Transfer (STTT), FoMaC, Special Issues, REoCAS 2022}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n LTL Synthesis on Infinite-State Arenas defined by Programs.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; Schneider, G.; and di Stefano, L.\n\n\n \n\n\n\n 2023.\n \n\n\n\n
\n\n\n\n \n \n \"LTLPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@misc{azzopardi2023ltl,\n      title={LTL Synthesis on Infinite-State Arenas defined by Programs}, \n      author={Azzopardi, Shaun and Piterman, Nir and Schneider, Gerardo and di Stefano, Luca},\n      year={2023},\n      eprint={2307.09776},\n      archivePrefix={arXiv},\n      primaryClass={cs.LO},\n      booktitle={arXiv},\n      url={https://arxiv.org/abs/2307.09776},\n      doi={10.48550/arXiv.2307.09776}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n ppLTLTT: Temporal testing for pure-past linear temporal logic formulae.\n \n \n \n\n\n \n Lidell, D.; Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n In Automated Technology for Verification and Analysis (ATVA), 2023. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{atva23,\ntitle={ppLTLTT: Temporal testing for pure-past linear temporal logic formulae}, \nauthor={Lidell, David and Azzopardi, Shaun and Piterman, Nir and Schneider, Gerardo},\nyear="2023",\nbooktitle="Automated Technology for Verification and Analysis (ATVA)"\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2022\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n R-CHECK: A Model Checker for Verifying Reconfigurable MAS.\n \n \n \n \n\n\n \n Alrahman, Y. A.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n 2022.\n \n\n\n\n
\n\n\n\n \n \n \"R-CHECK:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@misc{alrahman2022rcheck,\n      title={R-CHECK: A Model Checker for Verifying Reconfigurable MAS}, \n      author={Yehia Abd Alrahman and Shaun Azzopardi and Nir Piterman},\n      year={2022},\n      eprint={2201.06312},\n      archivePrefix={arXiv},\n      primaryClass={cs.LO},\n      booktitle={arXiv},\n      url={https://arxiv.org/abs/2201.06312}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Model Checking Reconfigurable Interacting Systems.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022. \n \n\n\n\n
\n\n\n\n \n \n \"ModelPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{isola-1,\ntitle={Model Checking Reconfigurable Interacting Systems}, \nauthor={Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir},\nyear="2022",\nbooktitle="International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74143/319774.pdf"\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Runtime Verification meets Controller Synthesis.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n In International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2022. \n \n\n\n\n
\n\n\n\n \n \n \"RuntimePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{isola-2,\ntitle={Runtime Verification meets Controller Synthesis}, \nauthor={Azzopardi, Shaun and Piterman, Nir, and Schneider, Gerardo},\nyear="2022",\nbooktitle="International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74142/319773.pdf?sequence=1&isAllowed=y"\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification.\n \n \n \n \n\n\n \n Shaun Azzopardi, J. E.; and Pace, G.\n\n\n \n\n\n\n In 22nd International Conference on Runtime Verification (RV), 2022. \n \n\n\n\n
\n\n\n\n \n \n \"AspectSol:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv22-1,\ntitle={AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification}, \nauthor={Shaun Azzopardi, Joshua Ellul, Ryan Falzon and Gordon Pace},\nyear="2022",\nbooktitle="22nd International Conference on Runtime Verification (RV)",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74146/319770.pdf?sequence=1&isAllowed=y"\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Tainting in Smart Contracts: Combining Static and Runtime Verification.\n \n \n \n \n\n\n \n Shaun Azzopardi, J. E.; and Pace, G.\n\n\n \n\n\n\n In 22nd International Conference on Runtime Verification (RV), 2022. \n \n\n\n\n
\n\n\n\n \n \n \"TaintingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv22-2,\ntitle={Tainting in Smart Contracts: Combining Static and Runtime Verification}, \nauthor={Shaun Azzopardi, Joshua Ellul, Ryan Falzon and Gordon Pace},\nyear="2022",\nbooktitle="22nd International Conference on Runtime Verification (RV)",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74145/319772.pdf?sequence=1"\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Runtime Verification of Kotlin Coroutines.\n \n \n \n \n\n\n \n Denis Furian, S. A.; and Schneider, G.\n\n\n \n\n\n\n In 22nd International Conference on Runtime Verification (RV), 2022. \n \n\n\n\n
\n\n\n\n \n \n \"RuntimePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv22-3,\ntitle={Runtime Verification of Kotlin Coroutines}, \nauthor={Denis Furian, Shaun Azzopardi, Yliès Falcone, and Gerardo Schneider},\nyear="2022",\nbooktitle="22nd International Conference on Runtime Verification (RV)",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74147/319771.pdf?sequence=1&isAllowed=y"\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n R-CHECK: A Model Checker for Verifying Reconfigurable MAS.\n \n \n \n \n\n\n \n Abd Alrahman, Y.; Azzopardi, S.; and Piterman, N.\n\n\n \n\n\n\n In Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, of AAMAS '22, pages 1518–1520, Richland, SC, 2022. International Foundation for Autonomous Agents and Multiagent Systems\n \n\n\n\n
\n\n\n\n \n \n \"R-CHECK:Paper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 5 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{10.5555/3535850.3536020,\nauthor = {Abd Alrahman, Yehia and Azzopardi, Shaun and Piterman, Nir},\ntitle = {R-CHECK: A Model Checker for Verifying Reconfigurable MAS},\nyear = {2022},\nisbn = {9781450392136},\npublisher = {International Foundation for Autonomous Agents and Multiagent Systems},\naddress = {Richland, SC},\nabstract = {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.},\nbooktitle = {Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems},\npages = {1518–1520},\nnumpages = {3},\nkeywords = {verification of multi-agent systems, logics for agent reasoning, agent theories and models},\nlocation = {Virtual Event, New Zealand},\nseries = {AAMAS '22},\nurl="https://www.ifaamas.org/Proceedings/aamas2022/pdfs/p1518.pdf"\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2021\n \n \n (5)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Incorporating Monitors in Reactive Synthesis without Paying the Price.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n 2021.\n \n\n\n\n
\n\n\n\n \n \n \"IncorporatingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@misc{azzopardi2021incorporating,\n      title={Incorporating Monitors in Reactive Synthesis without Paying the Price}, \n      author={Shaun Azzopardi and Nir Piterman and Gerardo Schneider},\n      year={2021},\n      eprint={2107.00929},\n      archivePrefix={arXiv},\n      primaryClass={cs.LO},\n      booktitle={arXiv},\n      url={https://arxiv.org/abs/2107.00929}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On the Specification and Monitoring of Timed Normative Systems.\n \n \n \n \n\n\n \n Azzopardi, S.; Pace, G.; Schapachnik, F.; and Schneider, G.\n\n\n \n\n\n\n In Feng, L.; and Fisman, D., editor(s), Runtime Verification (RV), pages 81–99, Cham, 2021. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rv21,\nauthor="Azzopardi, Shaun\nand Pace, Gordon\nand Schapachnik, Fernando\nand Schneider, Gerardo",\neditor="Feng, Lu\nand Fisman, Dana",\ntitle="On the Specification and Monitoring of Timed Normative Systems",\nbooktitle="Runtime Verification (RV)",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="81--99",\nabstract="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.",\nisbn="978-3-030-88494-9",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74148/309362.pdf?sequence=1"\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Incorporating Monitors in Reactive Synthesis Without Paying the Price.\n \n \n \n \n\n\n \n Azzopardi, S.; Piterman, N.; and Schneider, G.\n\n\n \n\n\n\n In Hou, Z.; and Ganesh, V., editor(s), Automated Technology for Verification and Analysis, pages 337–353, Cham, 2021. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n \n \"IncorporatingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{atva21,\nauthor="Azzopardi, Shaun\nand Piterman, Nir\nand Schneider, Gerardo",\neditor="Hou, Zhe\nand Ganesh, Vijay",\ntitle="Incorporating Monitors in Reactive Synthesis Without Paying the Price",\nbooktitle="Automated Technology for Verification and Analysis",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="337--353",\nabstract="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.",\nisbn="978-3-030-88885-5",\nurl="https://gupea.ub.gu.se/bitstream/handle/2077/74140/305933.pdf"\n}\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Model-Based Static and Runtime Verification for Ethereum Smart Contracts.\n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G.\n\n\n \n\n\n\n In Hammoudi, S.; Pires, L.; and Selić, B., editor(s), Model-Driven Engineering and Software Development, pages 323–348, Cham, 2021. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{10.1007/978-3-030-67445-8_14,\n\tauthor="Azzopardi, Shaun\n\tand Colombo, Christian\n\tand Pace, Gordon",\n\teditor="Hammoudi, Slimane\n\tand Pires, Lu{\\'i}s Ferreira\n\tand Seli{\\'{c}}, Bran",\n\ttitle="Model-Based Static and Runtime Verification for Ethereum Smart Contracts",\n\tbooktitle="Model-Driven Engineering and Software Development",\n\tyear="2021",\n\tpublisher="Springer International Publishing",\n\taddress="Cham",\n\tpages="323--348",\n\tabstract="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.",\n\tisbn="978-3-030-67445-8"\n}\n\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Runtime Monitoring Processes Across Blockchains.\n \n \n \n \n\n\n \n Azzopardi, S.; Ellul, J.; and Pace, G. J.\n\n\n \n\n\n\n In Hojjat, H.; and Massink, M., editor(s), Fundamentals of Software Engineering, pages 142–156, Cham, 2021. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n \n \"RuntimePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{rvblockchains,\nauthor="Azzopardi, Shaun\nand Ellul, Joshua\nand Pace, Gordon J.",\neditor="Hojjat, Hossein\nand Massink, Mieke",\ntitle="Runtime Monitoring Processes Across Blockchains",\nbooktitle="Fundamentals of Software Engineering",\nyear="2021",\npublisher="Springer International Publishing",\naddress="Cham",\npages="142--156",\nabstract="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.",\nisbn="978-3-030-89247-0",\nurl = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/fsen2021.pdf}\n}\n\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2020\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n A Technique for Automata-Based Verification with Residual Reasoning.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G.\n\n\n \n\n\n\n In Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020, Valletta, Malta, February 25-27, 2020, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{clarvatheory,\n  author    = {Shaun Azzopardi and\n                Christian Colombo and\n                Gordon Pace},\n  title     = {A Technique for Automata-Based Verification with Residual Reasoning},\n  booktitle = {Proceedings of the 8th International Conference on Model-Driven Engineering\n               and Software Development, {MODELSWARD} 2020, Valletta, Malta,\n               February 25-27, 2020},\n  year      = {2020},\n  url  = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/modelsward2020a.pdf},\n  doi = {10.5220/0008981902370248}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n CLARVA: Model-Based Residual Verification of Java Programs.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G.\n\n\n \n\n\n\n In Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020, Valletta, Malta, February 25-27, 2020, 2020. \n \n\n\n\n
\n\n\n\n \n \n \"CLARVA:Paper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{clarvatool,\n  author    = {Shaun Azzopardi and\n                Christian Colombo and\n                Gordon Pace},\n  title     = {CLARVA: Model-Based Residual Verification of Java Programs},\n  booktitle = {Proceedings of the 8th International Conference on Model-Driven Engineering\n               and Software Development, {MODELSWARD} 2020, Valletta, Malta,\n               February 25-27, 2020},\n  year      = {2020},\n  url = {http://www.cs.um.edu.mt/gordon.pace/Research/Papers/modelsward2020b.pdf},\n  doi = {10.5220/0008966603520359}\n}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2018\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond.\n \n \n \n \n\n\n \n Azzopardi, S.; Ellul, J.; and Pace, G. J.\n\n\n \n\n\n\n In Colombo, C.; and Leucker, M., editor(s), Runtime Verification, pages 113–137, Cham, 2018. Springer International Publishing\n \n\n\n\n
\n\n\n\n \n \n \"MonitoringPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n  \n \n abstract \n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{Shaun_Azzopardi48593129,\nauthor="Azzopardi, Shaun\nand Ellul, Joshua\nand Pace, Gordon J.",\neditor="Colombo, Christian\nand Leucker, Martin",\ntitle="Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond",\nbooktitle="Runtime Verification",\nyear="2018",\npublisher="Springer International Publishing",\naddress="Cham",\npages="113--137",\nabstract="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.",\nisbn="978-3-030-03769-7",\nurl="https://doi.org/10.1007/978-3-030-03769-7_8"\n}\n\n\n\n
\n
\n\n\n
\n 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.\n
\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n On Observing Contracts: Deontic Contracts Meet Smart Contracts.\n \n \n \n \n\n\n \n Azzopardi, S.; Pace, G. J.; and Schapachnik, F.\n\n\n \n\n\n\n In Legal Knowledge and Information Systems - JURIX 2018: The Thirty-first Annual Conference, Groningen, The Netherlands, 12-14 December 2018., pages 21–30, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"OnPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 11 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/jurix/AzzopardiPS18,\n  author    = {Shaun Azzopardi and\n               Gordon J. Pace and\n               Fernando Schapachnik},\n  title     = {On Observing Contracts: Deontic Contracts Meet Smart Contracts},\n  booktitle = {Legal Knowledge and Information Systems - {JURIX} 2018: The Thirty-first\n               Annual Conference, Groningen, The Netherlands, 12-14 December 2018.},\n  pages     = {21--30},\n  year      = {2018},\n  crossref  = {DBLP:conf/jurix/2018},\n  url       = {https://doi.org/10.3233/978-1-61499-935-5-21},\n  doi       = {10.3233/978-1-61499-935-5-21},\n  timestamp = {Sun, 16 Dec 2018 18:16:27 +0100},\n  biburl    = {https://dblp.org/rec/bib/conf/jurix/AzzopardiPS18},\n  bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Controlled Natural Language for Financial Services Compliance Checking.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G. J.\n\n\n \n\n\n\n In Controlled Natural Language - Proceedings of the Sixth International Workshop, CNL 2018, Maynooth, Co. Kildare, Ireland, August 27-28, 2018, pages 11–20, 2018. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/cnl/AzzopardiCP18, author= {Shaun Azzopardi and\n               Christian Colombo and\n               Gordon J. Pace}, title= {A Controlled Natural Language for Financial Services Compliance Checking}, booktitle= {Controlled Natural Language - Proceedings of the Sixth International\n               Workshop, {CNL} 2018, Maynooth, Co. Kildare, Ireland, August 27-28,\n               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}}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2017\n \n \n (3)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Control-Flow Residual Analysis for Symbolic Automata.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G. J.\n\n\n \n\n\n\n . 2017.\n \n\n\n\n
\n\n\n\n \n \n \"Control-FlowPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{Azzopardi_2017,\n\tyear = 2017,\n\n      eprint={1708.06889},\n      archivePrefix={arXiv},\n      primaryClass={cs.LO},\n      booktitle={arXiv},\n      url={https://arxiv.org/abs/1708.07230},\n      author = {Shaun Azzopardi and Christian Colombo and Gordon J. Pace},\n      title = {Control-Flow Residual Analysis for Symbolic Automata}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Runtime Verification using VALOUR.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; Ebejer, J.; Mallia, E.; and Pace, G. J.\n\n\n \n\n\n\n In 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, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"RuntimePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/rv/AzzopardiCEMP17, \n            author= {Shaun Azzopardi and\n               Christian Colombo and\n               Jean{-}Paul Ebejer and\n               Edward Mallia and\n               Gordon J. Pace}, \n            title= {Runtime Verification using {VALOUR}}, booktitle= {RV-CuBES 2017. An International Workshop on Competitions, Usability,\n               Benchmarks, Evaluation, and Standardisation for Runtime Verification\n               Tools, September 15, 2017, Seattle, WA, {USA}}, pages= {10--18}, year= {2017}, crossref= {DBLP:conf/rv/2017cubes}, url= {\thttps://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}}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Control-Flow Residual Analysis for Symbolic Automata.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G. J.\n\n\n \n\n\n\n In Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, PrePost@iFM 2017, Torino, Italy, 19 September 2017., pages 29–43, 2017. \n \n\n\n\n
\n\n\n\n \n \n \"Control-FlowPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:journals/corr/abs-1708-07230, author= {Shaun Azzopardi and\n               Christian Colombo and\n               Gordon J. Pace}, title= {Control-Flow Residual Analysis for Symbolic Automata}, booktitle= {Proceedings Second International Workshop on Pre- and Post-Deployment\n               Verification Techniques, PrePost@iFM 2017, Torino, Italy, 19 September\n               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}}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2016\n \n \n (7)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Residual Control-Flow Static Analysis with Symbolic Automata.\n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G. J.\n\n\n \n\n\n\n In CSAW 2016: Computer Science Annual Workshop 2016, University of Malta, Malta, 2016. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{clarva-csaw,\n\ttitle={Residual Control-Flow Static Analysis with Symbolic Automata},\n\tyear={2016},\n\tbooktitle={CSAW 2016: Computer Science Annual Workshop 2016, University of Malta, Malta},\n\tauthor={Shaun Azzopardi and\n\tChristian Colombo and\n\tGordon J. Pace}\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n Regulation specification and automatic static and dynamic checks generation in the OPE.\n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G. J.\n\n\n \n\n\n\n In CSAW 2016: Computer Science Annual Workshop 2016, University of Malta, Malta, 2016. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{ope-csaw,\n\ttitle={Regulation specification and automatic static and dynamic checks generation in the OPE},\n\tyear={2016},\n\tbooktitle={CSAW 2016: Computer Science Annual Workshop 2016, University of Malta, Malta},\n\tauthor={Shaun Azzopardi and\n\tChristian Colombo and\n\tGordon J. Pace}\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Reasoning About Partial Contracts.\n \n \n \n \n\n\n \n Azzopardi, S.; Gatt, A.; and Pace, G. J.\n\n\n \n\n\n\n In Legal Knowledge and Information Systems - JURIX 2016: The Twenty-Ninth Annual Conference, pages 23–32, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"ReasoningPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 7 downloads\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/jurix/AzzopardiGP16, author= {Shaun Azzopardi and\n               Albert Gatt and\n               Gordon J. Pace}, title= {Reasoning About Partial Contracts}, booktitle= {Legal Knowledge and Information Systems - {JURIX} 2016: The Twenty-Ninth\n               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}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n A Model-Based Approach to Combining Static and Dynamic Verification Techniques.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; and Pace, G. J.\n\n\n \n\n\n\n In 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, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"APaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/isola/AzzopardiCP16, author= {Shaun Azzopardi and\n               Christian Colombo and\n               Gordon J. Pace}, title= {A Model-Based Approach to Combining Static and Dynamic Verification\n               Techniques}, booktitle= {Leveraging Applications of Formal Methods, Verification and Validation:\n               Foundational Techniques - 7th International Symposium, ISoLA 2016,\n               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}}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Integrating Natural Language and Formal Analysis for Legal Documents.\n \n \n \n \n\n\n \n Azzopardi, S.; Gatt, A.; and Pace, G.\n\n\n \n\n\n\n 2016.\n \n\n\n\n
\n\n\n\n \n \n \"IntegratingPaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@conference{Shaun_Azzopardi48593036,\ntitle={Integrating Natural Language and Formal Analysis for Legal Documents},\nbooktitle={10th Conference on Language Technologies and Digital Humanities 2016, Ljubljana, Slovenia},\nauthor={Shaun Azzopardi and Albert Gatt and  Gordon Pace},\nyear={2016},\nurl="https://www.um.edu.mt/library/oar/handle/123456789/22605"\n}\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Compliance Checking in the Open Payments Ecosystem.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; Pace, G. J.; and Vella, B.\n\n\n \n\n\n\n In 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, 2016. \n \n\n\n\n
\n\n\n\n \n \n \"CompliancePaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/sefm/AzzopardiCPV16, author= {Shaun Azzopardi and\n               Christian Colombo and\n               Gordon J. Pace and\n               Brian Vella}, title= {Compliance Checking in the Open Payments Ecosystem}, booktitle= {Software Engineering and Formal Methods - 14th International Conference,\n               {SEFM} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 4-8,\n               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}}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Contract automata - An operational view of contracts between interactive parties.\n \n \n \n \n\n\n \n Azzopardi, S.; Pace, G. J.; Schapachnik, F.; and Schneider, G.\n\n\n \n\n\n\n Artificial Intelligence and Law, 24(3): 203–243. 2016.\n \n\n\n\n
\n\n\n\n \n \n \"ContractPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@article{DBLP:journals/ail/AzzopardiPSS16, author= {Shaun Azzopardi and\n               Gordon J. Pace and\n               Fernando Schapachnik and\n               Gerardo Schneider}, title= {Contract automata - An operational view of contracts between interactive\n               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}}\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2015\n \n \n (2)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n Formally Analysing Natural Language Contracts.\n \n \n \n\n\n \n Azzopardi, S.; Gatt, A.; and Pace, G. J.\n\n\n \n\n\n\n In CSAW 2015: Computer Science Annual Workshop 2015, University of Malta, Malta, 2015. \n \n\n\n\n
\n\n\n\n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{csaw-masters,\n\ttitle={Formally Analysing Natural Language Contracts},\n\tyear={2015},\n\tbooktitle={CSAW 2015: Computer Science Annual Workshop 2015, University of Malta, Malta},\n\tauthor={Shaun Azzopardi and\n\tAlbert Gatt and\n\tGordon J. Pace}\n}\n\n\n
\n
\n\n\n\n
\n\n\n
\n \n\n \n \n \n \n \n \n Compliance Checking in the Open Payments Ecosystem.\n \n \n \n \n\n\n \n Azzopardi, S.; Colombo, C.; Pace, G. J.; and Vella, B.\n\n\n \n\n\n\n In CSAW 2015: Computer Science Annual Workshop 2015, University of Malta, Malta, 2015. \n \n\n\n\n
\n\n\n\n \n \n \"CompliancePaper\n  \n \n\n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@InProceedings{ope-csaw-1,\n\ttitle={Compliance Checking in the Open Payments Ecosystem},\n\tyear={2015},\n\tbooktitle={CSAW 2015: Computer Science Annual Workshop 2015, University of Malta, Malta},\n\tauthor={Shaun Azzopardi and\n\tChristian Colombo and\n\tGordon J. Pace and\n\tBrian Vella},\n  url="https://www.um.edu.mt/library/oar/bitstream/123456789/23982/1/Compliance%20Checking%20in%20the%20Open%20Payments%20Ecosystem.pdf"\n}\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n  \n 2014\n \n \n (1)\n \n \n
\n
\n \n \n
\n \n\n \n \n \n \n \n \n Contract Automata with Reparations.\n \n \n \n \n\n\n \n Azzopardi, S.; Pace, G. J.; and Schapachnik, F.\n\n\n \n\n\n\n In Legal Knowledge and Information Systems - JURIX 2014: The Twenty-Seventh Annual Conference, Jagiellonian University, Krakow, Poland, 10-12 December 2014, pages 49–54, 2014. \n \n\n\n\n
\n\n\n\n \n \n \"ContractPaper\n  \n \n\n \n \n doi\n  \n \n\n \n link\n  \n \n\n bibtex\n \n\n \n\n \n  \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n  \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/jurix/AzzopardiPS14, author= {Shaun Azzopardi and\n               Gordon J. Pace and\n               Fernando Schapachnik}, title= {Contract Automata with Reparations}, booktitle= {Legal Knowledge and Information Systems - {JURIX} 2014: The Twenty-Seventh\n               Annual Conference, Jagiellonian University, Krakow, Poland, 10-12\n               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}}\n\n\n
\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n\n\n\n
\n\n\n \n\n \n \n \n \n\n
\n"}; document.write(bibbase_data.data);