MCLab Group List of Papers -- Query Results

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

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 >>

List View

Citations

Details

	Records
	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		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ ChiLatMar08			Serial	94
Permanent link to this record



	Author	Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
	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		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; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
	Title	Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems			Type	Book Chapter
	Year	2012	Publication	Theoretical Aspects of Computing – ICTAC 2012	Abbreviated Journal
	Volume		Issue		Pages	243-258
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	Springer Berlin Heidelberg	Place of Publication		Editor	Roychoudhury, A.; D'Souza, M.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	7521	Series Issue		Edition
	ISSN		ISBN	978-3-642-32942-5	Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Mari2012			Serial	99
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	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	Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry
	Title	Model Checking Coalition Nash Equilibria in MAD Distributed Systems			Type	Conference Article
	Year	2009	Publication	Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings	Abbreviated Journal
	Volume		Issue		Pages	531-546
	Keywords
	Abstract	We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an ε-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than ε in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^21$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication		Editor	Guerraoui, R.; Petit, F.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	5873	Series Issue		Edition
	ISSN		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ sss09			Serial	19
Permanent link to this record



	Author	Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
	Title	Simulator Semantics for System Level Formal Verification			Type	Conference Article
	Year	2015	Publication	Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015),	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	MCLab @ davi @			Serial	125
Permanent link to this record



	Author	Tronci, E.; Mancini, T.; Mari, F.; Melatti, I.; Jacobsen, R. H.; Ebeid, E.; Mikkelsen, S. A.; Prodanovic, M.; Gruber, J. K.; Hayes, B.
	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	Alimguzhin, Vadim; Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
	Title	Automatic Control Software Synthesis for Quantized Discrete Time Hybrid Systems			Type	Conference Article
	Year	2012	Publication	Proceedings of the 51th IEEE Conference on Decision and Control, CDC 2012, December 10-13, 2012, Maui, HI, USA	Abbreviated Journal
	Volume		Issue		Pages	6120-6125
	Keywords
	Abstract
	Address
	Corporate Author				Thesis
	Publisher	IEEE	Place of Publication		Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN		ISBN	978-1-4673-2065-8	Medium
	Area		Expedition		Conference
	Notes	Techreport version can be found at http://arxiv.org/abs/1207.4098			Approved	yes
	Call Number	Sapienza @ mari @ cdc12			Serial	96
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	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	Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
	Title	SyLVaaS: System Level Formal Verification as a Service			Type	Conference Article
	Year	2015	Publication	Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD)	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	MCLab @ davi @			Serial	123
Permanent link to this record