
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. "Linear Constraints and Guarded Predicates as a Modeling Language for Discrete Time Hybrid Systems." International Journal on Advances in Software vol. 6, nr 1&2 (2013): 155–169. IARIA. ISSN: 19422628.
Abstract: Model based design is particularly appealing in
software based control systems (e.g., embedded
software) design, since in such a case system
level specifications are much easier to define
than the control software behavior itself. In
turn, model based design of embedded systems
requires modeling both continuous subsystems
(typically, the plant) as well as discrete
subsystems (the controller). This is typically
done using hybrid systems. Mixed Integer Linear
Programming (MILP) based abstraction techniques
have been successfully applied to automatically
synthesize correctbyconstruction control
software for discrete time linear hybrid systems,
where plant dynamics is modeled as a linear
predicate over state, input, and next state
variables. Unfortunately, MILP solvers require
such linear predicates to be conjunctions of
linear constraints, which is not a natural way of
modeling hybrid systems. In this paper we show
that, under the hypothesis that each variable
ranges over a bounded interval, any linear
predicate built upon conjunction and disjunction
of linear constraints can be automatically
translated into an equivalent conjunctive
predicate. Since variable bounds play a key role
in this translation, our algorithm includes a
procedure to compute all implicit variable bounds
of the given linear predicate. Furthermore, we
show that a particular form of linear predicates,
namely guarded predicates, are a natural and
powerful language to succinctly model discrete
time linear hybrid systems dynamics. Finally, we
experimentally show the feasibility of our
approach on an important and challenging case
study taken from the literature, namely the
multiinput Buck DCDC Converter. As an example,
the guarded predicate that models (with 57
constraints) a 6inputs Buck DCDC Converter is
translated in a conjunctive predicate (with 102
linear constraints) in about 40 minutes.
Keywords: Modelbased software design; Linear predicates; Hybrid systems



Enrico Tronci. "Formally Modeling a Metal Processing Plant and its Closed Loop Specifications." In 4th IEEE International Symposium on HighAssurance Systems Engineering (HASE), 151. Washington, D.C, USA: IEEE Computer Society, 1999. ISSN: 0769504183. DOI: 10.1109/HASE.1999.809490.
Abstract: We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design followed by automatic verification. The system to be controlled (plant) models a metal processing facility near Karlsruhe. We succeeded in automatically generating C code implementing a (correct by construction) embedded controller for such a plant from closed loop formal specifications. Our experimental results show that for industrial automation control systems automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design followed by automatic verification.



Enrico Tronci. "Equational Programming in LambdaCalculus via SLSystems. Part 1." Theoretical Computer Science 160, no. 1&2 (1996): 145–184. DOI: 10.1016/03043975(95)001050.



Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Michele Minichino, Ester Ciancamerla, Andrea Parisse, Enrico Tronci, and Marisa Venturini Zilli. "Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier." In Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 35, 2003, Proceedings, edited by O. Maler and A. Pnueli, 141–155. Lecture Notes in Computer Science 2623. Springer, 2003. ISSN: 3540009132. DOI: 10.1007/354036580X.
Abstract: Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Cogenerative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas.



Benedetto Intrigila, Ivano Salvo, and Stefano Sorgi. "A characterization of weakly ChurchRosser abstract reduction systems that are not ChurchRosser." Information and Computation 171, no. 2 (2001): 137–155. Academic Press, Inc.. ISSN: 08905401. DOI: 10.1006/inco.2001.2945.
Abstract: Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or ChurchRosser, CR) and weak confluence (or weak ChurchRosser, WCR) and their relationships can be studied in this setting: as a matter of fact, wellknown counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graphtheoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the NewmanÃ¢â‚¬â„¢s lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graphrewriting rules, with specific combinatorial properties.



Enrico Tronci. "Automatic Synthesis of Controllers from Formal Specifications." In Proc of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM), 134–143. Brisbane, Queensland, Australia, 1998. DOI: 10.1109/ICFEM.1998.730577.
Abstract: Many safety critical reactive systems are indeed embedded control systems. Usually a control system can be partitioned into two main subsystems: a controller and a plant. Roughly speaking: the controller observes the state of the plant and sends commands (stimulus) to the plant to achieve predefined goals. We show that when the plant can be modeled as a deterministic finite state system (FSS) it is possible to effectively use formal methods to automatically synthesize the program implementing the controller from the plant model and the given formal specifications for the closed loop system (plant+controller). This guarantees that the controller program is correct by construction. To the best of our knowledge there is no previously published effective algorithm to extract executable code for the controller from closed loop formal specifications. We show practical usefulness of our techniques by giving experimental results on their use to synthesize C programs implementing optimal controllers (OCs) for plants with more than 109 states.



B. Leeners, T. H. C. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. RÃ¶blitz, L. Saleh, K. Spanaus et al. "Lack of Associations between Female Hormone Levels and Visuospatial Working Memory, Divided Attention and Cognitive Bias across Two Consecutive Menstrual Cycles." Frontiers in Behavioral Neuroscience 11 (2017): 120. ISSN: 16625153. DOI: 10.3389/fnbeh.2017.00120.
Abstract: Background: Interpretation of observational studies on associations between prefrontal cognitive functioning and hormone levels across the female menstrual cycle is complicated due to small sample sizes and poor replicability. Methods: This observational multisite study comprised data of n=88 menstruating women from Hannover, Germany, and Zurich, Switzerland, assessed during a first cycle and n=68 reassessed during a second cycle to rule out practice effects and falsepositive chance findings. We assessed visuospatial working memory, attention, cognitive bias and hormone levels at four consecutive timepoints across both cycles. In addition to interindividual differences we examined intraindividual change over time (i.e., withinsubject effects). Results: Oestrogen, progesterone and testosterone did not relate to interindividual differences in cognitive functioning. There was a significant negative association between intraindividual change in progesterone and change in working memory from preovulatory to midluteal phase during the first cycle, but that association did not replicate in the second cycle. Intraindividual change in testosterone related negatively to change in cognitive bias from menstrual to preovulatory as well as from preovulatory to midluteal phase in the first cycle, but these associations did not replicate in the second cycle. Conclusions: There is no consistent association between women's hormone levels, in particular oestrogen and progesterone, and attention, working memory and cognitive bias. That is, anecdotal findings observed during the first cycle did not replicate in the second cycle, suggesting that these are falsepositives attributable to random variation and systematic biases such as practice effects. Due to methodological limitations, positive findings in the published literature must be interpreted with reservation.



S. Fischer, R. Ehrig, S. Schaefer, E. Tronci, T. Mancini, M. Egli, F. Ille, T. H. C. Krueger, B. Leeners, and S. Roeblitz. "Mathematical Modeling and Simulation Provides Evidence for New Strategies of Ovarian Stimulation." Frontiers in Endocrinology 12 (2021): 117. ISSN: 16642392. DOI: 10.3389/fendo.2021.613048.
Abstract: New approaches to ovarian stimulation protocols, such as luteal start, random start or double stimulation, allow for flexibility in ovarian stimulation at different phases of the menstrual cycle. It has been proposed that the success of these methods is based on the continuous growth of multiple cohorts (“waves”) of follicles throughout the menstrual cycle which leads to the availability of ovarian follicles for ovarian controlled stimulation at several time points. Though several preliminary studies have been published, their scientific evidence has not been considered as being strong enough to integrate these results into routine clinical practice. This work aims at adding further scientific evidence about the efficiency of variablestart protocols and underpinning the theory of follicular waves by using mathematical modeling and numerical simulations. For this purpose, we have modified and coupled two previously published models, one describing the time course of hormones and one describing competitive follicular growth in a normal menstrual cycle. The coupled model is used to test ovarian stimulation protocols in silico. Simulation results show the occurrence of follicles in a wavelike manner during a normal menstrual cycle and qualitatively predict the outcome of ovarian stimulation initiated at different time points of the menstrual cycle.



Amedeo Cesta, Simone Fratini, Andrea Orlandini, Alberto Finzi, and Enrico Tronci. "Flexible Plan Verification: Feasibility Results." Fundamenta Informaticae 107, no. 2 (2011): 111–137. DOI: 10.3233/FI2011397.

