|   | 
Details
   web
Records
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 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 (down) Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ DIMTZ04j Serial 91
Permanent link to this record
 

 
Author Mari, Federico; Tronci, Enrico
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 (down) 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
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 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 (down) Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ ChiLatMar08 Serial 94
Permanent link to this record