toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author (down) Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico pdf  doi
openurl 
  Title Model checking driven simulation of sat procedures Type Conference Article
  Year 2012 Publication Proceedings of 12th International Conference on Space Operations (SpaceOps 2012) Abbreviated Journal International Conference on Space Operations  
  Volume Issue Pages  
  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 no  
  Call Number Sapienza @ melatti @ Serial 117  
Permanent link to this record
 

 
Author (down) Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa pdf  doi
openurl 
  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 (down) Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa pdf  doi
openurl 
  Title Exploiting Transition Locality in Automatic Verification Type Conference Article
  Year 2001 Publication 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) Abbreviated Journal  
  Volume Issue Pages 259-274  
  Keywords  
  Abstract In this paper we present an algorithm to contrast state explosion when using Explicit State Space Exploration to verify protocols. We show experimentally that protocols exhibit transition locality. We present a verification algorithm that exploits transition locality as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm is compatible with all Breadth First (BF) optimization techniques present in the Mur$\varphi$ verifier and it is by no means a substitute for any of them. In fact, since our algorithm trades space with time, it is typically most useful when one runs out of memory and has already used all other state reduction techniques present in the Mur$\varphi$ verifier. Our experimental results show that using our approach we can typically save more than 40% of RAM with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Livingston, Scotland, UK Editor Margaria, T.; Melham, T.F.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 2144 Series Issue Edition  
  ISSN 3-540-42541-1 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ charme01 Serial 44  
Permanent link to this record
 

 
Author (down) Tronci, E.; Mancini, T.; Salvo, I.; Mari, F.; Melatti, I.; Massini, A.; Sinisi, S.; Davì, F.; Dierkes, T.; Ehrig, R.; Röblitz, S.; Leeners, B.; Krüger, T.; Egli, M.; Ille, F. pdf  doi
openurl 
  Title Patient-Specific Models from Inter-Patient Biological Models and Clinical Records Type Conference Article
  Year 2014 Publication Formal Methods in Computer-Aided Design (FMCAD) Abbreviated Journal  
  Volume Issue Pages  
  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 no  
  Call Number Sapienza @ mari @ Serial 120  
Permanent link to this record
 

 
Author (down) Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Prodanovic, M.; Gruber, J. K.; Hayes, B.; Elmegaard, L. pdf  doi
openurl 
  Title Demand-Aware Price Policy Synthesis and Verification Services for Smart Grids Type Conference Article
  Year 2014 Publication Proceedings of Smart Grid Communications (SmartGridComm), 2014 IEEE International Conference On Abbreviated Journal  
  Volume Issue Pages  
  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 no  
  Call Number Sapienza @ melatti @ Serial 121  
Permanent link to this record
 

 
Author (down) Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Jacobsen, R. H.; Ebeid, E.; Mikkelsen, S. A.; Prodanovic, M.; Gruber, J. K.; Hayes, B. pdf  isbn
openurl 
  Title SmartHG: Energy Demand Aware Open Services for Smart Grid Intelligent Automation Type Conference Article
  Year 2014 Publication Proceedings of the Work in Progress Session of SEAA/DSD 2014 Abbreviated Journal  
  Volume Issue Pages  
  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 978-3-902457-40-0 Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ mari @ Serial 119  
Permanent link to this record
 

 
Author (down) Toni Mancini; Enrico Tronci; Ivano Salvo; Federico Mari; Annalisa Massini; Igor Melatti pdf  doi
openurl 
  Title Computing Biological Model Parameters by Parallel Statistical Model Checking Type Journal Article
  Year 2015 Publication International Work Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015) Abbreviated Journal  
  Volume 9044 Issue Pages 542-554  
  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 no  
  Call Number MCLab @ davi @ Serial 124  
Permanent link to this record
 

 
Author (down) Mazzini, Silvia; Puri, Stefano; Mari, Federico; Melatti, Igor; Tronci, Enrico pdf  openurl
  Title Formal Verification at System Level Type Conference Article
  Year 2009 Publication In: DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. Instanbul, Turkey, EuroSpace Abbreviated Journal  
  Volume Issue Pages  
  Keywords  
  Abstract System Level Analysis calls for a language comprehensible to experts with different background and yet precise enough to support meaningful analyses. SysML is emerging as an effective balance between such conflicting goals. In this paper we outline some the results obtained as for SysML based system level functional formal verification by an ESA/ESTEC study, with a collaboration among INTECS and La Sapienza University of Roma. The study focuses on SysML based system level functional requirements techniques.  
  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 @ Dasia09 Serial 20  
Permanent link to this record
 

 
Author (down) Mari, Federico; Tronci, Enrico pdf  doi
openurl 
  Title CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems Type Conference Article
  Year 2007 Publication Hybrid Systems: Computation and Control (HSCC 2007) Abbreviated Journal  
  Volume Issue Pages 399-412  
  Keywords Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS  
  Abstract Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem. We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems. Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Bemporad, A.; Bicchi, A.; Buttazzo, G.C.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 4416 Series Issue Edition  
  ISSN ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ MarTro07 Serial 92  
Permanent link to this record
 

 
Author (down) Mari, Federico; Melatti, Igor; Tronci, Enrico; Finzi, Alberto pdf  url
doi  openurl
  Title A multi-hop advertising discovery and delivering protocol for multi administrative domain MANET Type Journal Article
  Year 2013 Publication Mobile Information Systems Abbreviated Journal Mobile Information Systems  
  Volume 3 Issue 9 Pages 261-280  
  Keywords  
  Abstract  
  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 1574-017x (Print) 1875-905X (Online) ISBN Medium  
  Area Expedition Conference  
  Notes Approved no  
  Call Number Sapienza @ melatti @ Serial 109  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: