
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, and Marisa Venturini Zilli. "Synchronized Regular Expressions." Electr. Notes Theor. Comput. Sci. 62 (2002): 195–210. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types.
Abstract: Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday stresses the need of more powerful tools to interact with texts. Indeed, much work has been done to provide nonprogramming tools that can be useful for the most common text manipulation issues. Regular Expressions (RE), introduced by Kleene, are wellÃ‚â€“known in the formal language theory. RE received several extensions, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [A] UNIX command, or the Perl [17] language pattern matching constructs) we find backreferences (as defind in [1]), i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all the kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. Therefore, we introduce the Synchronized Regular Expressions (SRE) as a derivation of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are talking about formalisms that should have a practical utility and can be used in the real world, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a userÃ‚â€“friendly syntax for SRE to be used in implementations of SREÃ‚â€“powered search algorithms.



Riccardo Focardi, Roberto Gorrieri, Ruggero Lanotte, Andrea MaggioloSchettini, Fabio Martinelli, Simone Tini, and Enrico Tronci. "Formal Models of Timing Attacks on Web Privacy." Electronic Notes in Theoretical Computer Science 62 (2002): 229–243. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types. DOI: 10.1016/S15710661(04)003299.
Abstract: We model a timing attack on web privacy proposed by Felten and Schneider by using three different approaches: HLTimed Automata, SMV model checker, and tSPA Process Algebra. Some comparative analysis on the three approaches is derived.



Franco Barbanera, Mariangiola DezaniCiancaglini, Ivano Salvo, and Vladimiro Sassone. "A Type Inference Algorithm for Secure Ambients." Electronic Notes in Theoretical Computer Science 62 (2002): 83–101. Elsevier. Notes: TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types. DOI: 10.1016/S15710661(04)003214.
Abstract: We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottomup algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario.



I. Melatti, F. Mari, T. Mancini, M. Prodanovic, and E. Tronci. "A TwoLayer NearOptimal Strategy for Substation Constraint Management via Home Batteries." IEEE Transactions on Industrial Electronics (2021): 1. Notes: To appear. DOI: 10.1109/TIE.2021.3102431.
Abstract: Within electrical distribution networks, substation constraints management requires that aggregated power demand from residential users is kept within suitable bounds. Efficiency of substation constraints management can be measured as the reduction of constraints violations w.r.t. unmanaged demand. Home batteries hold the promise of enabling efficient and useroblivious substation constraints management. Centralized control of home batteries would achieve optimal efficiency. However, it is hardly acceptable by users, since service providers (e.g., utilities or aggregators) would directly control batteries at user premises. Unfortunately, devising efficient hierarchical control strategies, thus overcoming the above problem, is far from easy. We present a novel twolayer control strategy for home batteries that avoids direct control of home devices by the service provider and at the same time yields nearoptimal substation constraints management efficiency. Our simulation results on field data from 62 households in Denmark show that the substation constraints management efficiency achieved with our approach is at least 82% of the one obtained with a theoretical optimal centralized strategy.



T. Mancini, I. Melatti, and E. Tronci. "Anyhorizon uniform random sampling and enumeration of constrained scenarios for simulationbased formal verification." IEEE Transactions on Software Engineering (2021): 1. ISSN: 19393520. Notes: To appear. DOI: 10.1109/TSE.2021.3109842.
Abstract: Modelbased approaches to the verification of nonterminating CyberPhysical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently enumerate (possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulationbased statistical model checking. Unfortunately, in case of nontrivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in general fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be very inefficient to produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which anyhorizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables seamless support to virtually all simulationbased approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.



Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems." In Proceedings of the 51th IEEE Conference on Decision and Control, CDC 2012, December 1013, 2012, Maui, HI, USA, 6120–6125. IEEE, 2012. ISBN: 9781467320658. Notes: Techreport version can be found at http://arxiv.org/abs/1207.4098. DOI: 10.1109/CDC.2012.6426260.



Vadim Alimguzhin, Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "On Model Based Synthesis of Embedded Control Software." In Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2012, part of the Eighth Embedded Systems Week, ESWeek 2012, Tampere, Finland, October 712, 2012, edited by Ahmed Jerraya and Luca P. Carloni and Florence Maraninchi and John Regehr, 227–236. ACM, 2012. ISBN: 9781450314251. Notes: Techreport version can be found at arxiv.org. DOI: 10.1145/2380356.2380398.



V. Bono, and I. Salvo. "A CuCh Interpretation of an ObjectOriented Language." Electronic Notes in Theoretical Computer Science 50, no. 2 (2001): 159–177. Elsevier. Notes: BOTH 2001, BohmÃ¢â‚¬â„¢s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001). DOI: 10.1016/S15710661(04)001719.
Abstract: CuCh machine extends pure lambdaÃ‚â€“calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of overloading to define a functional interpretation of a simple, but significant fragment of a typical objectoriented language.



Federico Mari, Igor Melatti, Ivano Salvo, and Enrico Tronci. "From Boolean Relations to Control Software." In Proceedings of ICSEA 2011, The Sixth International Conference on Software Engineering Advances, 528–533. ThinkMind, 2011. ISSN: 9781612081656. Notes: Best Paper Award.
Abstract: Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) linear in nr, being n = x the number of input arguments for functions in F and r the number of functions in F.



T. Mancini, F. Mari, I. Melatti, I. Salvo, and E. Tronci. "An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks." In Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 2931, 2018, Proceedings, 302–312., 2018. Notes: Best Paper. DOI: 10.1007/9783030018511_29.

