Volume
OASIcs, Volume 86
Recent Developments in the Design and Implementation of Programming Languages
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Festschrift Maurizio Gabbrielli
Publication Details
- published at: 2020-11-27
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-171-9
- DBLP: db/conf/birthday/gabbrielli2020
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 86, Gabbrielli's Festschrift, Complete Volume
Abstract
OASIcs, Volume 86, Gabbrielli's Festschrift, Complete Volume
Cite as
Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@Proceedings{deboer_et_al:OASIcs.Gabbrielli,
title = {{OASIcs, Volume 86, Gabbrielli's Festschrift, Complete Volume}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {1--256},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli},
URN = {urn:nbn:de:0030-drops-132219},
doi = {10.4230/OASIcs.Gabbrielli},
annote = {Keywords: OASIcs, Volume 86, Gabbrielli's Festschrift, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{deboer_et_al:OASIcs.Gabbrielli.0,
author = {de Boer, Frank S. and Mauro, Jacopo},
title = {{Front Matter, Table of Contents, Preface}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {0:i--0:xiv},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.0},
URN = {urn:nbn:de:0030-drops-132227},
doi = {10.4230/OASIcs.Gabbrielli.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Locally Static, Globally Dynamic Session Types for Active Objects
Abstract
Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.
Cite as
Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{hahnle_et_al:OASIcs.Gabbrielli.1,
author = {H\"{a}hnle, Reiner and Haubner, Anton W. and Kamburjan, Eduard},
title = {{Locally Static, Globally Dynamic Session Types for Active Objects}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {1:1--1:24},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.1},
URN = {urn:nbn:de:0030-drops-132237},
doi = {10.4230/OASIcs.Gabbrielli.1},
annote = {Keywords: Session Types, Active Objects, Runtime Verification, Static Verification}
}
Document
A Formal Analysis of the Bitcoin Protocol
Abstract
We study Nakamoto’s Bitcoin protocol that implements a distributed ledger on peer-to-peer asynchronous networks. In particular, we define a principled formal model of key participants - the miners - as stochastic processes and describe the whole system as a parallel composition of miners. We therefore compute the probability that ledgers turn into a state with more severe inconsistencies, e.g. with longer forks, under the assumptions that messages are not lost and nodes are not hostile. We also study how the presence of hostile nodes mining blocks in wrong positions impacts on the consistency of the ledgers. Our theoretical results agree with the simulations performed on a probabilistic model checker that we extended with dynamic datatypes in order to have a faithful description of miners' behaviour.
Cite as
Cosimo Laneve and Adele Veschetti. A Formal Analysis of the Bitcoin Protocol. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{laneve_et_al:OASIcs.Gabbrielli.2,
author = {Laneve, Cosimo and Veschetti, Adele},
title = {{A Formal Analysis of the Bitcoin Protocol}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {2:1--2:17},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.2},
URN = {urn:nbn:de:0030-drops-132242},
doi = {10.4230/OASIcs.Gabbrielli.2},
annote = {Keywords: Bitcoin, Distributed consensus, Distributed ledgers, Blockchain, PRISM, forks}
}
Document
Deconfined Intersection Types in Java
Abstract
We show how Java intersection types can be freed from their confinement in type casts, in such a way that the proposed Java extension is safe and fully compatible with the current language. To this aim, we exploit two calculi which formalise the simple Java core and the extended language, respectively. Namely, the second calculus extends the first one by allowing an intersection type to be used anywhere in place of a nominal type. We define a translation algorithm, compiling programs of the extended language into programs of the former calculus. The key point is the interaction between λ-expressions and intersection types, that adds safe expressiveness while being the crucial matter in the translation. We prove that the translation preserves typing and semantics. Thus, typed programs in the proposed extension are translated to typed Java programs. Moreover, semantics of translated programs coincides with the one of the source programs.
Cite as
Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Deconfined Intersection Types in Java. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dezaniciancaglini_et_al:OASIcs.Gabbrielli.3,
author = {Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Venneri, Betti},
title = {{Deconfined Intersection Types in Java}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {3:1--3:25},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.3},
URN = {urn:nbn:de:0030-drops-132256},
doi = {10.4230/OASIcs.Gabbrielli.3},
annote = {Keywords: Intersection Types, Featherweight Java, Lambda Expressions}
}
Document
Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation
Abstract
Static and dynamic program analyses attempt to extract useful information on program’s behaviours. Static analysis uses an abstract model of programs to reason on their runtime behaviour without actually running them, while dynamic analysis reasons on a test set of real program executions. For this reason, the precision of static analysis is limited by the presence of false positives (executions allowed by the abstract model that cannot happen at runtime), while the precision of dynamic analysis is limited by the presence of false negatives (real executions that are not in the test set). Researchers have developed many analysis techniques and tools in the attempt to increase the precision of program verification. Software protection is an interesting scenario where programs need to be protected from adversaries that use program analysis to understand their inner working and then exploit this knowledge to perform some illicit actions. Program analysis plays a dual role in program verification and software protection: in program verification we want the analysis to be as precise as possible, while in software protection we want to degrade the results of the analysis as much as possible. Indeed, in software protection researchers usually recur to a special class of program transformations, called code obfuscation, to modify a program in order to make it more difficult to analyse while preserving its intended functionality. In this setting, it is interesting to study how program transformations that preserve the intended behaviour of programs can affect the precision of both static and dynamic analysis. While some works have been done in order to formalise the efficiency of code obfuscation in degrading static analysis and in the possibility of transforming programs in order to avoid or increase false positives, less attention has been posed to formalise the relation between program transformations and false negatives in dynamic analysis. In this work we are setting the scene for a formal investigation of the syntactic and semantic program features that affect the presence of false negatives in dynamic analysis. We believe that this understanding would be useful for improving the precision of the existing dynamic analysis tools and in the design of program transformations that complicate the dynamic analysis.
To Maurizio on his 60th birthday!
Cite as
Mila Dalla Preda. Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{dallapreda:OASIcs.Gabbrielli.4,
author = {Dalla Preda, Mila},
title = {{Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {4:1--4:22},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.4},
URN = {urn:nbn:de:0030-drops-132263},
doi = {10.4230/OASIcs.Gabbrielli.4},
annote = {Keywords: Program analysis, analysis precision, program transformation, software protection, code obfuscation}
}
Document
The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service
Abstract
Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the λ- and the π-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous π-calculus and prove it correct in terms of an operational correspondence.
Dedicated to Maurizio Gabbrielli, on his 60th birthday (... rob da mët ! )
Cite as
Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro. The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{giallorenzo_et_al:OASIcs.Gabbrielli.5,
author = {Giallorenzo, Saverio and Lanese, Ivan and Montesi, Fabrizio and Sangiorgi, Davide and Zingaro, Stefano Pio},
title = {{The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {5:1--5:21},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.5},
URN = {urn:nbn:de:0030-drops-132271},
doi = {10.4230/OASIcs.Gabbrielli.5},
annote = {Keywords: Serverless computing, Process calculi, Pi-calculus}
}
Document
A Logic Programming Approach to Reaction Systems
Abstract
Reaction systems (RS) are a computational framework inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RS have shown to be useful also for computer science applications, e.g. to model circuits or transition systems. Since their introduction about 10 years ago, RS matured into a fruitful and dynamically evolving research area. They have become a popular novel model of interactive computation. RS can be seen as a rewriting system interacting with the environment represented by the context. RS pose some problems of implementation, as it is a relatively recent computation model, and several extensions of the basic model have been designed. In this paper we present some preliminary work on how to implement this formalism in a logic programming language (Prolog). To the best of our knowledge this is the first approach to RS in logic programming. Our prototypical implementation does not aim to be highly performing, but has the advantage of being high level and easily modifiable. So it is suitable as a rapid prototyping tool for implementing several extensions of reaction systems in the literature as well as new ones. We also make a preliminary implementation of a kind of memoization mechanism for stopping potentially infinite and repetitive computations. Then we show how to implement in our interpreter an extension of RS for modeling a nondeterministic context and interaction between components of a (biological) system. We then present an extension of the interpreter for implementing the recently introduced networks of RS.
Cite as
Moreno Falaschi and Giulia Palma. A Logic Programming Approach to Reaction Systems. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{falaschi_et_al:OASIcs.Gabbrielli.6,
author = {Falaschi, Moreno and Palma, Giulia},
title = {{A Logic Programming Approach to Reaction Systems}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {6:1--6:15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.6},
URN = {urn:nbn:de:0030-drops-132282},
doi = {10.4230/OASIcs.Gabbrielli.6},
annote = {Keywords: reaction systems, logic programming, non deterministic context}
}
Document
Abstract Interpretation, Symbolic Execution and Constraints
Abstract
Abstract interpretation is a static analysis framework for sound over-approximation of all possible runtime states of a program. Symbolic execution is a framework for reachability analysis which tries to explore all possible execution paths of a program. A shared feature between abstract interpretation and symbolic execution is that each - implicitly or explicitly - maintains constraints during execution, in the form of invariants or path conditions. We investigate the relations between the worlds of abstract interpretation, symbolic execution and constraint solving, to expose potential synergies.
Cite as
Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. Abstract Interpretation, Symbolic Execution and Constraints. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{amadini_et_al:OASIcs.Gabbrielli.7,
author = {Amadini, Roberto and Gange, Graeme and Schachte, Peter and S{\o}ndergaard, Harald and Stuckey, Peter J.},
title = {{Abstract Interpretation, Symbolic Execution and Constraints}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {7:1--7:19},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.7},
URN = {urn:nbn:de:0030-drops-132294},
doi = {10.4230/OASIcs.Gabbrielli.7},
annote = {Keywords: Abstract interpretation, symbolic execution, constraint solving, dynamic analysis, static analysis}
}
Document
The Standard Model for Programming Languages: The Birth of a Mathematical Theory of Computation
Abstract
Despite the insight of some of the pioneers (Turing, von Neumann, Curry, Böhm), programming the early computers was a matter of fiddling with small architecture-dependent details. Only in the sixties some form of "mathematical program development" will be in the agenda of some of the most influential players of that time. A "Mathematical Theory of Computation" is the name chosen by John McCarthy for his approach, which uses a class of recursively computable functions as an (extensional) model of a class of programs. It is the beginning of that grand endeavour to present programming as a mathematical activity, and reasoning on programs as a form of mathematical logic. An important part of this process is the standard model of programming languages - the informal assumption that the meaning of programs should be understood on an abstract machine with unbounded resources, and with true arithmetic. We present some crucial moments of this story, concluding with the emergence, in the seventies, of the need of more "intensional" semantics, like the sequential algorithms on concrete data structures. The paper is a small step of a larger project - reflecting and tracing the interaction between mathematical logic and programming (languages), identifying some of the driving forces of this process.
to Maurizio Gabbrielli, on his 60th birthday
Cite as
Simone Martini. The Standard Model for Programming Languages: The Birth of a Mathematical Theory of Computation. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{martini:OASIcs.Gabbrielli.8,
author = {Martini, Simone},
title = {{The Standard Model for Programming Languages: The Birth of a Mathematical Theory of Computation}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {8:1--8:13},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.8},
URN = {urn:nbn:de:0030-drops-132307},
doi = {10.4230/OASIcs.Gabbrielli.8},
annote = {Keywords: Semantics of programming languages, history of programming languages, mathematical theory of computation}
}
Document
A Concurrent Language for Argumentation: Preliminary Notes
Abstract
While agent-based modelling languages naturally implement concurrency, the currently available languages for argumentation do not allow to explicitly model this type of interaction. In this paper we introduce a concurrent language for handling process arguing and communicating using a shared argumentation framework (reminding shared constraint store as in concurrent constraint). We introduce also basic expansions, contraction and revision procedures as main bricks for enforcement, debate, negotiation and persuasion.
Cite as
Stefano Bistarelli and Carlo Taticchi. A Concurrent Language for Argumentation: Preliminary Notes. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bistarelli_et_al:OASIcs.Gabbrielli.9,
author = {Bistarelli, Stefano and Taticchi, Carlo},
title = {{A Concurrent Language for Argumentation: Preliminary Notes}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {9:1--9:22},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.9},
URN = {urn:nbn:de:0030-drops-132311},
doi = {10.4230/OASIcs.Gabbrielli.9},
annote = {Keywords: Argumentation, Concurrent Language, Debating, Negotiation, Belief Revision}
}
Document
Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages
Abstract
This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.
Cite as
Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito. Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{deboer_et_al:OASIcs.Gabbrielli.10,
author = {de Boer, Frank S. and Johnsen, Einar Broch and Schlatte, Rudolf and Tapia Tarifa, Silvia Lizeth and Tveito, Lars},
title = {{Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {10:1--10:18},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.10},
URN = {urn:nbn:de:0030-drops-132322},
doi = {10.4230/OASIcs.Gabbrielli.10},
annote = {Keywords: Testing, Symbolic Traces, Guarded Commands, Partial Order Reduction}
}
Document
Derivation of Constraints from Machine Learning Models and Applications to Security and Privacy
Abstract
This paper shows how we can combine the power of machine learning with the flexibility of constraints. More specifically, we show how machine learning models can be represented by first-order logic theories, and how to derive these theories. The advantage of this representation is that it can be augmented with additional formulae, representing constraints of some kind on the data domain. For instance, new knowledge, or potential attackers, or fairness desiderata. We consider various kinds of learning algorithms (neural networks, k-nearest-neighbours, decision trees, support vector machines) and for each of them we show how to infer the FOL formulae. Then we focus on one particular application domain, namely the field of security and privacy. The idea is to represent the potentialities and goals of the attacker as a set of constraints, then use a constraint solver (more precisely, a solver modulo theories) to verify the satisfiability. If a solution exists, then it means that an attack is possible, otherwise, the system is safe. We show various examples from different areas of security and privacy; specifically, we consider a side-channel attack on a password checker, a malware attack on smart health systems, and a model-inversion attack on a neural network.
Cite as
Moreno Falaschi, Catuscia Palamidessi, and Marco Romanelli. Derivation of Constraints from Machine Learning Models and Applications to Security and Privacy. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{falaschi_et_al:OASIcs.Gabbrielli.11,
author = {Falaschi, Moreno and Palamidessi, Catuscia and Romanelli, Marco},
title = {{Derivation of Constraints from Machine Learning Models and Applications to Security and Privacy}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {11:1--11:20},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.11},
URN = {urn:nbn:de:0030-drops-132338},
doi = {10.4230/OASIcs.Gabbrielli.11},
annote = {Keywords: Constraints, machine learning, privacy, security}
}
Document
Adaptive Real Time IoT Stream Processing in Microservices Architecture
Abstract
The Internet of Things (IoT) has created new and challenging opportunities for Data Analytics. IoT represents an infinitive source of massive and heterogeneous data, whose real-time processing is an increasingly important issue. Real-time Data Stream Processing is a natural answer for the majority of the goals of IoT platforms, but it has to deal with the highly variable and dynamic IoT environment. IoT applications usually consist of multiple technological layers connecting ‘things’ to a remote cloud core. These layers are generally grouped in two macro-levels: the edge-level (consisting of the devices at the boundary of the network near the devices that produce the data) and the core-level (consisting of the remote cloud components of the application). Real-time Data Stream Processing has to cope with a wide variety of technologies, devices and requirements that vary depending on the two IoT application levels. The aim of this work is to propose an adaptive microservices architecture for an IoT platform able to integrate real-time stream processing functionalities in a dynamic and flexible way, with the goal of covering the different real-time processing requirements that exist among the different levels of an IoT application. The proposal has been formulated for extending Senseioty, a proprietary IoT platform developed by FlairBit S.r.l., but it can easily be integrated in any other IoT platform. A preliminary prototype has been implemented as proof of concept of the feasibility and benefits of the proposed architecture.
Cite as
Luca Bixio, Giorgio Delzanno, Stefano Rebora, and Matteo Rulli. Adaptive Real Time IoT Stream Processing in Microservices Architecture. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
Copy BibTex To Clipboard
@InProceedings{bixio_et_al:OASIcs.Gabbrielli.12,
author = {Bixio, Luca and Delzanno, Giorgio and Rebora, Stefano and Rulli, Matteo},
title = {{Adaptive Real Time IoT Stream Processing in Microservices Architecture}},
booktitle = {Recent Developments in the Design and Implementation of Programming Languages},
pages = {12:1--12:20},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-95977-171-9},
ISSN = {2190-6807},
year = {2020},
volume = {86},
editor = {de Boer, Frank S. and Mauro, Jacopo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.12},
URN = {urn:nbn:de:0030-drops-132341},
doi = {10.4230/OASIcs.Gabbrielli.12},
annote = {Keywords: Cloud Computing, Service Oriented Computing, Internet of Things, Real-time Stream Processing, Query Languages}
}