MCLab Group List of Papers -- Query Results

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

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	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	Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe
	Title	Disk Based Software Verification via Bounded Model Checking			Type	Conference Article
	Year	2007	Publication	APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference	Abbreviated Journal
	Volume		Issue		Pages	358-365
	Keywords
	Abstract	One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, DC, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-3057-5	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Bmtd07			Serial	76
Permanent link to this record



	Author	Della Penna, Giuseppe; Magazzeni, Daniele; Tofani, Alberto; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
	Title	Automatic Synthesis of Robust Numerical Controllers			Type	Conference Article
	Year	2007	Publication	Icas '07	Abbreviated Journal
	Volume		Issue		Pages	4
	Keywords
	Abstract	A major problem of numerical controllers is their robustness, i.e. the state read from the plant may not be in the controller table, although it may be close to some states in the table. For continuous systems, this problem is typically handled by interpolation techniques. Unfortunately, when the plant contains both continuous and discrete variables, the interpolation approach does not work well. To cope with this kind of systems, we propose a general methodology that exploits explicit model checking in an innovative way to automatically synthesize a (time-) optimal numerical controller from a plant specification and apply an optimized strengthening algorithm only on the most significant states, in order to reach an acceptable robustness degree. We implemented all the algorithms within our CGMurphi tool, an extension of the well-known CMurphi verifier, and tested the effectiveness of our approach by applying it to the well-known truck and trailer obstacles avoidance problem.
	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	0-7695-2859-5	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Dmtimt07			Serial	89
Permanent link to this record



	Author	Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico
	Title	A Model Checking Technique for the Verification of Fuzzy Control Systems			Type	Conference Article
	Year	2005	Publication	CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06)	Abbreviated Journal
	Volume		Issue		Pages	536-542
	Keywords
	Abstract	Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, DC, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-2504-0-01	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Immt05			Serial	75
Permanent link to this record



	Author	Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa
	Title	A Probabilistic Approach to Automatic Verification of Concurrent Systems			Type	Conference Article
	Year	2001	Publication	8th Asia-Pacific Software Engineering Conference (APSEC)	Abbreviated Journal
	Volume		Issue		Pages	317-324
	Keywords
	Abstract	The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead it just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that by using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Macau, China	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-1408-1	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ apsec01			Serial	43
Permanent link to this record



	Author	Dipoppa, G.; D'Alessandro, G.; Semprini, R.; Tronci, E.
	Title	Integrating Automatic Verification of Safety Requirements in Railway Interlocking System Design			Type	Conference Article
	Year	2001	Publication	High Assurance Systems Engineering, 2001. Sixth IEEE International Symposium on	Abbreviated Journal
	Volume		Issue		Pages	209-219
	Keywords
	Abstract	A railway interlocking system (RIS) is an embedded system (namely a supervisory control system) that ensures the safe, operation of the devices in a railway station. RIS is a safety critical system. We explore the possibility of integrating automatic formal verification methods in a given industry RIS design flow. The main obstructions to be overcome in our work are: selecting a formal verification tool that is efficient enough to solve the verification problems at hand; and devising a cost effective integration strategy for such tool. We were able to devise a successful integration strategy meeting the above constraints without requiring major modification in the pre-existent design flow nor retraining of personnel. We run verification experiments for a RIS designed for the Singapore Subway. The experiments show that the RIS design flow obtained from our integration strategy is able to automatically verify real life RIS designs.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Albuquerque, NM, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-1275-5	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ hase01			Serial	45
Permanent link to this record



	Author	Cecconi, Michele; Tronci, Enrico
	Title	Requirements Formalization and Validation for a Telecommunication Equipment Protection Switcher			Type	Conference Article
	Year	2000	Publication	Hase	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract
	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	0-7695-0927-4	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ CeTro00			Serial	29
Permanent link to this record



	Author	Tronci, Enrico
	Title	Formally Modeling a Metal Processing Plant and its Closed Loop Specifications			Type	Conference Article
	Year	1999	Publication	4th IEEE International Symposium on High-Assurance Systems Engineering (HASE)	Abbreviated Journal
	Volume		Issue		Pages	151
	Keywords
	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.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, D.C, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-0418-3	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ hase99			Serial	50
Permanent link to this record



	Author	Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri
	Title	Model Checking Satellite Operational Procedures			Type	Conference Article
	Year	2011	Publication	DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace.	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract	We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.
	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 @ Dasia11			Serial	13
Permanent link to this record



	Author	Cesta, Amedeo; Fratini, Simone; Orlandini, Andrea; Finzi, Alberto; Tronci, Enrico
	Title	Flexible Plan Verification: Feasibility Results			Type	Journal Article
	Year	2011	Publication	Fundamenta Informaticae	Abbreviated Journal
	Volume	107	Issue	2	Pages	111-137
	Keywords
	Abstract
	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 @ fi11			Serial	15
Permanent link to this record