toggle visibility Search & Display Options

Select All    Deselect All
 |   | 
Details
   print
  Records Links
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa pdf  doi
openurl 
  Title Finite Horizon Analysis of Stochastic Systems with the Mur$\varphi$ Verifier Type Conference Article
  Year 2003 Publication Theoretical Computer Science, 8th Italian Conference, ICTCS 2003, Bertinoro, Italy, October 13-15, 2003, Proceedings Abbreviated Journal  
  Volume Issue (down) Pages 58-71  
  Keywords  
  Abstract Many reactive systems are actually Stochastic Processes. Automatic analysis of such systems is usually very difficult thus typically one simplifies the analysis task by using simulation or by working on a simplified model (e.g. a Markov Chain). We present a Finite Horizon Probabilistic Model Checking approach which essentially can handle the same class of stochastic processes of a typical simulator. This yields easy modeling of the system to be analyzed together with formal verification capabilities. Our approach is based on a suitable disk based extension of the Mur$\varphi$ verifier. Moreover we present experimental results showing effectiveness of our approach.  
  Address  
  Corporate Author Thesis  
  Publisher Springer Place of Publication Editor Blundo, C.; Laneve, C.  
  Language Summary Language Original Title  
  Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title  
  Series Volume 2841 Series Issue Edition  
  ISSN 3-540-20216-1 ISBN Medium  
  Area Expedition Conference  
  Notes Approved yes  
  Call Number Sapienza @ mari @ DIMTZ03c Serial 90  
Permanent link to this record
 

 
Author 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 (down) 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 Chierichetti, Flavio; Lattanzi, Silvio; Mari, Federico; Panconesi, Alessandro pdf  doi
openurl 
  Title On Placing Skips Optimally in Expectation Type Conference Article
  Year 2008 Publication Web Search and Web Data Mining (WSDM 2008) Abbreviated Journal  
  Volume Issue (down) Pages 15-24  
  Keywords Information Retrieval  
  Abstract We study the problem of optimal skip placement in an inverted list. Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O(n log n), n being the length of the list. The placement is optimal in the sense that it minimizes the expected time to process a query. Our theoretical results are matched by experiments with a real corpus, showing that substantial savings can be obtained with respect to the tra- ditional skip placement strategy, that of placing consecutive skips, each spanning sqrt(n) many locations.  
  Address  
  Corporate Author Thesis  
  Publisher Acm Place of Publication Editor Najork, M.; Broder, A.Z.; Chakrabarti, S.  
  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 @ ChiLatMar08 Serial 94  
Permanent link to this record
Select All    Deselect All
 |   | 
Details
   print

Save Citations:
Export Records: