MCLab Group List of Papers -- Query Results

	MCLab Group List of Papers Home \| Show All \| Simple Search \| Advanced Search	Login Quick Search: Field: contains: ...
	21–30 of 143 records found matching your query (RSS \| history):

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 8 9 10 >> [11–15]

List View

Citations

Details

	Records
	Author	Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano
	Title	Intersection types and λ-definability			Type	Journal Article
	Year	2003	Publication	Mathematical Structures in Computer Science	Abbreviated Journal
	Volume	13	Issue	1	Pages	15-53
	Keywords
	Abstract	This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
	Address
	Corporate Author				Thesis
	Publisher	Cambridge University Press	Place of Publication	New York, NY, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0960-1295	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03			Serial	69
Permanent link to this record



	Author	Bucciarelli, Antonio; de Lorenzis, Silvia; Piperno, Adolfo; Salvo, Ivano
	Title	Some Computational Properties of Intersection Types (Extended Abstract)			Type	Journal Article
	Year	1999	Publication		Abbreviated Journal
	Volume		Issue		Pages	109-118
	Keywords	lambda calculusCurry types, intersection types, lambda-definability, lambda-terms, strong normalization
	Abstract	This paper presents a new method for comparing computation-properties of λ-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and λ-definability are investigated. A translation is introduced from intersection typing derivations to Curry typeable terms; the main feature of the proposed technique is that the translation is preserved by β-reduction. This allows to simulate a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach naturally leads to prove strong normalization in the intersection system by means of purely syntactical techniques. In addition, the presented method enables us to give a proof of a conjecture proposed by Leivant in 1990, namely that all functions uniformly definable using intersection types are already definable using Curry types.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ bucciarelli-delorenzis-piperno-salvo:99			Serial	71
Permanent link to this record



	Author	Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico
	Title	Automated analysis of timed security: a case study on web privacy			Type	Journal Article
	Year	2004	Publication	International Journal of Information Security	Abbreviated Journal
	Volume	2	Issue	3-4	Pages	168-186
	Keywords
	Abstract	This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ ijis04			Serial	33
Permanent link to this record



	Author	Ciancamerla, Ester; Minichino, Michele; Serro, Stefano; Tronci, Enrico
	Title	Automatic Timeliness Verification of a Public Mobile Network			Type	Conference Article
	Year	2003	Publication	22nd International Conference on Computer Safety, Reliability, and Security (SAFECOMP)	Abbreviated Journal
	Volume		Issue		Pages	35-48
	Keywords
	Abstract	This paper deals with the automatic verification of the timeliness of Public Mobile Network (PMN), consisting of Mobile Nodes (MNs) and Base Stations (BSs). We use the Mur$\varphi$ Model Checker to verify that the waiting access time of each MN, under different PMN configurations and loads, and different inter arrival times of MNs in a BS cell, is always below a preassigned threshold. Our experimental results show that Model Checking can be successfully used to generate worst case scenarios and nicely complements probabilistic methods and simulation which are typically used for performance evaluation.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Edinburgh, UK	Editor	Anderson, S.; Felici, M.; Littlewood, B.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	2788	Series Issue		Edition
	ISSN	978-3-540-20126-7	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ safecomp03			Serial	38
Permanent link to this record



	Author	Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
	Title	Verifying Flexible Timeline-based Plans			Type	Conference Article
	Year	2009	Publication	E-Proc. of ICAPS Workshop on Validation and Verification of Planning and Scheduling Systems	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract	The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verification method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Vvps09			Serial	23
Permanent link to this record



	Author	Leeners, B.; Krueger, T.; Geraedts, K.; Tronci, E.; Mancini, T.; Ille, F.; Egli, M.; Roeblitz, S.; Wunder, D.; Saleh, L.; Schippert, C.; Hengartner, M.P.
	Title	Cognitive function in association with high estradiol levels resulting from fertility treatment			Type	Journal Article
	Year	2021	Publication	Hormones and Behavior	Abbreviated Journal
	Volume	130	Issue		Pages	104951
	Keywords	Cognition, Estrogen, Estradiol, Fertility treatment, Attention, Cognitive bias
	Abstract	The putative association between hormones and cognitive performance is controversial. While there is evidence that estradiol plays a neuroprotective role, hormone treatment has not been shown to improve cognitive performance. Current research is flawed by the evaluation of combined hormonal effects throughout the menstrual cycle or in the menopausal transition. The stimulation phase of a fertility treatment offers a unique model to study the effect of estradiol on cognitive function. This quasi-experimental observational study is based on data from 44 women receiving IVF in Zurich, Switzerland. We assessed visuospatial working memory, attention, cognitive bias, and hormone levels at the beginning and at the end of the stimulation phase of ovarian superstimulation as part of a fertility treatment. In addition to inter-individual differences, we examined intra-individual change over time (within-subject effects). The substantial increases in estradiol levels resulting from fertility treatment did not relate to any considerable change in cognitive functioning. As the tests applied represent a broad variety of cognitive functions on different levels of complexity and with various brain regions involved, we can conclude that estradiol does not show a significant short-term effect on cognitive function.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0018-506x	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	no
	Call Number	MCLab @ davi @ Leeners2021104951			Serial	185
Permanent link to this record



	Author	Bobbio, Andrea; Bologna, Sandro; Minichino, Michele; Ciancamerla, Ester; Incalcaterra, Piero; Kropp, Corrado; Tronci, Enrico
	Title	Advanced techniques for safety analysis applied to the gas turbine control system of Icaro co generative plant			Type	Conference Article
	Year	2001	Publication	X Convegno Tecnologie e Sistemi Energetici Complessi	Abbreviated Journal
	Volume		Issue		Pages	339-350
	Keywords
	Abstract	The paper describes two complementary and integrable approaches, a probabilistic one and a deterministic one, based on classic and advanced modelling techniques for safety analysis of complex computer based systems. The probabilistic approach is based on classical and innovative probabilistic analysis methods. The deterministic approach is based on formal verification methods. Such approaches are applied to the gas turbine control system of ICARO co generative plant, in operation at ENEA CR Casaccia. The main difference between the two approaches, behind the underlining different theories, is that the probabilistic one addresses the control system by itself, as the set of sensors, processing units and actuators, while the deterministic one also includes the behaviour of the equipment under control which interacts with the control system. The final aim of the research, documented in this paper, is to explore an innovative method which put the probabilistic and deterministic approaches in a strong relation to overcome the drawbacks of their isolated, selective and fragmented use which can lead to inconsistencies in the evaluation results.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication	Genova, Italy	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ tesec01			Serial	65
Permanent link to this record



	Author	Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Tini, Simone; Troina, Angelo; Tronci, Enrico
	Title	Automatic Covert Channel Analysis of a Multilevel Secure Component			Type	Conference Article
	Year	2004	Publication	Information and Communications Security, 6th International Conference, ICICS 2004, Malaga, Spain, October 27-29, 2004, Proceedings	Abbreviated Journal
	Volume		Issue		Pages	249-261
	Keywords
	Abstract	The NRL Pump protocol defines a multilevel secure component whose goal is to minimize leaks of information from high level systems to lower level systems, without degrading average time performances. We define a probabilistic model for the NRL Pump and show how a probabilistic model checker (FHP-mur$\varphi$) can be used to estimate the capacity of a probabilistic covert channel in the NRL Pump. We are able to compute the probability of a security violation as a function of time for various configurations of the system parameters (e.g. buffer sizes, moving average size, etc). Because of the model complexity, our results cannot be obtained using an analytical approach and, because of the low probabilities involved, it can be hard to obtain them using a simulator.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Lopez, J.; Qing, S.; Okamoto, E.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3269	Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ icics04			Serial	34
Permanent link to this record



	Author	Gribaudo, Marco; HorvÃ¡th, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele
	Title	Model-Checking Based on Fluid Petri Nets for the Temperature Control System of the ICARO Co-generative Plant			Type	Conference Article
	Year	2002	Publication	21st International Conference on Computer Safety, Reliability and Security (SAFECOMP)	Abbreviated Journal
	Volume		Issue		Pages	273-283
	Keywords
	Abstract	The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain for conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPN). It is shown that the same FPN model can be fed to a functional analyser for model checking as well as to a stochastic analyser for performance evaluation. We illustrate our approach and show its usefulness by applying it to a Ã¢â‚¬Å“real worldÃ¢â‚¬Â hybrid system: the temperature control system of a co-generative plant.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Catania, Italy	Editor	Anderson, S.; Bologna, S.; Felici, M.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	2434	Series Issue		Edition
	ISSN	3-540-44157-3	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ safecomp02			Serial	42
Permanent link to this record



	Author	Gribaudo, Marco; HorvÃ¡th, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele
	Title	Fluid Petri Nets and hybrid model checking: a comparative case study			Type	Journal Article
	Year	2003	Publication	Int. Journal on: Reliability Engineering & System Safety	Abbreviated Journal
	Volume	81	Issue	3	Pages	239-257
	Keywords
	Abstract	The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a Ã¢â‚¬â„¢real worldÃ¢â‚¬â„¢ hybrid system: the temperature control system of a co-generative plant.
	Address
	Corporate Author				Thesis
	Publisher	Elsevier	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ ress03			Serial	40
Permanent link to this record