21 citations · 78 across the 18 of their papers we have counts for
21 papers
Synchronous Agents, Verification, and Blame -- A Deontic View
Karam Kharraz, Shaun Azzopardi, Gerardo Schneider +1
A question we can ask of multi-agent systems is whether the agents' collective interaction satisfies particular goals or specifications, which can be either individual or collectiv…
Full LTL Synthesis over Infinite-state Arenas
Shaun Azzopardi, Luca Di Stefano, Nir Piterman +1
Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating…
Correct-by-Construction Design of Contextual Robotic Missions Using Contracts
Piergiuseppe Mallozzi, Pierluigi Nuzzo, Nir Piterman +2
Effectively specifying and implementing robotic missions poses a set of challenges to software engineering for robotic systems. These challenges stem from the need to formalize and…
Capturing Smart Contract Design with DCR Graphs
Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho +2
Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, ac…
Incorporating Monitors in Reactive Synthesis without Paying the Price
Shaun Azzopardi, Nir Piterman, Gerardo Schneider
Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarat…
A Multidisciplinary Definition of Privacy Labels: The Story of Princess Privacy and the Seven Helpers
Johanna Johansen, Tore Pedersen, Simone Fischer-Hübner +6
Privacy is currently in distress and in need of rescue, much like princesses in the all-familiar fairytales. We employ storytelling and metaphors from fairytales to make reader-fri…
Transforming Data Flow Diagrams for Privacy Compliance (Long Version)
Hanaa Alshareef, Sandro Stucki, Gerardo Schneider
Recent regulations, such as the European General Data Protection Regulation (GDPR), put stringent constraints on the handling of personal data. Privacy, like security, is a non-fun…
Security Wrappers for Information-Flow Control in Active Object Languages with Futures
Farzane Karami, Olaf Owe, Gerardo Schneider
This paper introduces a run-time mechanism for preventing leakage of secure information in distributed systems. We consider a general concurrency language model, where concurrent o…
Gray-box Monitoring of Hyperproperties (Extended Version)
Sandro Stucki, César Sánchez, Gerardo Schneider +1
Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyper…
COST Action IC 1402 ArVI: Runtime Verification Beyond Monitoring -- Activity Report of Working Group 1
Wolfgang Ahrendt, Cyrille Artho, Christian Colombo +9
This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of th…
A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)
César Sánchez, Gerardo Schneider, Wolfgang Ahrendt +13
Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime…
Monitoring Data Minimisation
Srinivas Pinisetty, Thibaud Antignac, David Sands +1
Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking t…
Model Checking Social Network Models
Raúl Pardo, Gerardo Schneider
A social network service is a platform to build social relations among people sharing similar interests and activities. The underlying structure of a social networks service is the…
Timed Epistemic Knowledge Bases for Social Networks (Extended Version)
Raúl Pardo, César Sánchez, Gerardo Schneider
We present an epistemic logic equipped with time-stamps in the atoms and epistemic operators, which allows to reason not only about information available to the different agents, b…
A Web-Based Tool for Analysing Normative Documents in English
John J. Camilleri, Mohammad Reza Haghshenas, Gerardo Schneider
Our goal is to use formal methods to analyse normative documents written in English, such as privacy policies and service-level agreements. This requires the combination of a numbe…
Extracting Formal Models from Normative Texts
John J. Camilleri, Normunds Grūz\=ıtis, Gerardo Schneider
We are concerned with the analysis of normative texts - documents based on the deontic notions of obligation, permission, and prohibition. Our goal is to make queries about these n…
Data Minimisation: a Language-Based Approach (Long Version)
Thibaud Antignac, David Sands, Gerardo Schneider
Data minimisation is a privacy-enhancing principle considered as one of the pillars of personal data regulations. This principle dictates that personal data collected should be no…
Extracting Formal Models from Normative Texts
John J. Camilleri, Normunds Gruzitis, Gerardo Schneider
Normative texts are documents based on the deontic notions of obligation, permission, and prohibition. Our goal is to model such texts using the C-O Diagram formalism, making them…
A CNL for Contract-Oriented Diagrams
John J. Camilleri, Gabriele Paganelli, Gerardo Schneider
We present a first step towards a framework for defining and manipulating normative documents or contracts described as Contract-Oriented (C-O) Diagrams. These diagrams provide a v…
From Contracts in Structured English to CL Specifications
Seyed M. Montazeri, Nivir K. S. Roy, Gerardo Schneider
In this paper we present a framework to analyze conflicts of contracts written in structured English. A contract that has manually been rewritten in a structured English is automat…
Timed Automata Semantics for Visual e-Contracts
Enrique Martínez, M. Emilia Cambronero, Gregorio Díaz +1
C-O Diagrams have been introduced as a means to have a more visual representation of electronic contracts, where it is possible to represent the obligations, permissions and prohib…