|   | 
Details
   web
Records
Author Sinisi, S.; Alimguzhin, V.; Mancini, T.; Tronci, E.; Mari, F.; Leeners, B.
Title Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins Type Journal Article
Year 2020 Publication Abbreviated Journal Fundamenta Informaticae
Volume 174 Issue Pages (up) 283-310
Keywords Artificial Intelligence; Virtual Physiological Human; In Silico Clinical Trials; Simulation; Personalised Medicine; In Silico Treatment Optimisation
Abstract In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine ). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.
Address
Corporate Author Thesis
Publisher IOS Press Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1875-8681 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number MCLab @ davi @ Serial 187
Permanent link to this record
 

 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico
Title System Level Formal Verification via Model Checking Driven Simulation Type Conference Article
Year 2013 Publication Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia Abbreviated Journal CAV 2013
Volume Issue Pages (up) 296-312
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer - Verlag Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 8044 Series Issue Edition
ISSN 0302-9743 ISBN 978-3-642-39798-1 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 113
Permanent link to this record
 

 
Author Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
Title Validation and verification issues in a timeline-based planning system Type Journal Article
Year 2010 Publication The Knowledge Engineering Review Abbreviated Journal
Volume 25 Issue 03 Pages (up) 299-318
Keywords
Abstract One of the key points to take into account to foster effective introduction of AI planning and scheduling systems in real world is to develop end user trust in the related technologies. Automated planning and scheduling systems often brings solutions to the users which are neither “obvious†nor immediately acceptable for them. This is due to the ability of these tools to take into account quite an amount of temporal and causal constraints and to employ resolution processes often designed to optimize the solution with respect to non trivial evaluation functions. To increase technology trust, the study of tools for verifying and validating plans and schedules produced by AI systems might be instrumental. In general, validation and verification techniques represent a needed complementary technology in developing domain independent architectures for automated problem solving. This paper presents a preliminary report of the issues concerned with the use of two software tools for formal verification of finite state systems to the validation of the solutions produced by MrSPOCK, a recent effort for building a timeline based planning tool in an ESA project.
Address
Corporate Author Thesis
Publisher Cambridge University Press 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 @ Cffot10 Serial 18
Permanent link to this record
 

 
Author Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.
Title An Efficient Algorithm for Network Vulnerability Analysis Under Malicious Attacks Type Conference Article
Year 2018 Publication Foundations of Intelligent Systems – 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings Abbreviated Journal
Volume Issue Pages (up) 302-312
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 Best Paper Approved no
Call Number MCLab @ davi @ DBLP:conf/ismis/ManciniMMST18 Serial 176
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 (up) 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 Böhm, Corrado; Tronci, Enrico
Title X-Separability and Left-Invertibility in lambda-calculus Type Conference Article
Year 1987 Publication Symposium on Logic in Computer Science (LICS) Abbreviated Journal
Volume Issue Pages (up) 320-328
Keywords
Abstract
Address
Corporate Author Thesis
Publisher IEEE Computer Society Place of Publication Ithaca, New York, USA 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 @ lics87 Serial 63
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems Type Journal Article
Year 2004 Publication Sttt Abbreviated Journal
Volume 6 Issue 4 Pages (up) 320-341
Keywords
Abstract In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms. We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Mur$\varphi$ verifier distribution. We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Mur$\varphi$ verifier. Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Mur$\varphi$ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Mur$\varphi$ was able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 GB of memory using standard Mur$\varphi$.
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 @ DIMTZ04j Serial 91
Permanent link to this record
 

 
Author Piperno, Adolfo; Tronci, Enrico
Title Regular Systems of Equations in λ-calculus Type Journal Article
Year 1990 Publication Int. J. Found. Comput. Sci. Abbreviated Journal
Volume 1 Issue 3 Pages (up) 325-340
Keywords
Abstract Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.
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 @ ijfcs90 Serial 60
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 (up) 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 Tronci, Enrico
Title Introductory Paper Type Journal Article
Year 2006 Publication Sttt Abbreviated Journal
Volume 8 Issue 4-5 Pages (up) 355-358
Keywords
Abstract In today’s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21–24 October 2003 in L’Aquila, Italy. Authors of well regarded papers from CHARME’03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.
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 @ sttt06 Serial 30
Permanent link to this record