|   | 
Details
   web
Records
Author Barbanera, Franco; Dezani-Ciancaglini, Mariangiola; Salvo, Ivano; Sassone, Vladimiro
Title A Type Inference Algorithm for Secure Ambients Type Journal Article
Year 2002 Publication Electronic Notes in Theoretical Computer Science Abbreviated Journal
Volume 62 Issue Pages 83-101
Keywords
Abstract We consider a type discipline for the Ambient Calculus that associates ambients with security levels and constrains them to be traversed by or opened in ambients of higher security clearance only. We present a bottom-up algorithm that, given an untyped process P, computes a minimal set of constraints on security levels such that all actions during runs of P are performed without violating the security level priorities. Such an algorithm appears to be a prerequisite to use type systems to ensure security properties in the web scenario.
Address
Corporate Author (up) Thesis
Publisher Elsevier 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 TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types Approved yes
Call Number Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01 Serial 73
Permanent link to this record
 

 
Author Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Giovannetti, Elio; Salvo, Ivano
Title Mobility Types for Mobile Processes in Mobile Ambients Type Journal Article
Year 2003 Publication Electr. Notes Theor. Comput. Sci. Abbreviated Journal
Volume 78 Issue Pages
Keywords
Abstract We present an ambient-like calculus in which the open capability is dropped, and a new form of “lightweight  process mobility is introduced. The calculus comes equipped with a type system that allows the kind of values exchanged in communications and the access and mobility properties of processes to be controlled. A type inference procedure determines the “minimal  requirements to accept a system or a component as well typed. This gives a kind of principal typing. As an expressiveness test, we show that some well known calculi of concurrency and mobility can be encoded in our calculus in a natural way.
Address
Corporate Author (up) 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 @ Coppo-Dezani-Giovannetti-Salvo:03 Serial 74
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Finite horizon analysis of Markov Chains with the Mur$\varphi$ verifier Type Journal Article
Year 2006 Publication Int. J. Softw. Tools Technol. Transf. Abbreviated Journal
Volume 8 Issue 4 Pages 397-409
Keywords
Abstract In this paper we present an explicit disk-based verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. Given a Markov Chain and an integer k (horizon), our algorithm checks whether the probability of reaching an error state in at most k steps is below a given threshold. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call the resulting probabilistic model checker FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$). We present experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can handle systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
Address
Corporate Author (up) Thesis
Publisher Springer-Verlag Place of Publication Berlin, Heidelberg Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1433-2779 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimtz06 Serial 78
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico; Venturini Zilli, Marisa
Title Bounded Probabilistic Model Checking with the Mur$\varphi$ Verifier Type Conference Article
Year 2004 Publication Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings Abbreviated Journal
Volume Issue Pages 214-229
Keywords
Abstract In this paper we present an explicit verification algorithm for Probabilistic Systems defining discrete time/finite state Markov Chains. We restrict ourselves to verification of Bounded PCTL formulas (BPCTL), that is, PCTL formulas in which all Until operators are bounded, possibly with different bounds. This means that we consider only paths (system runs) of bounded length. Given a Markov Chain $\cal M$ and a BPCTL formula Φ, our algorithm checks if Φ is satisfied in $\cal M$. This allows to verify important properties, such as reliability in Discrete Time Hybrid Systems. We present an implementation of our algorithm within a suitable extension of the Mur$\varphi$ verifier. We call FHP-Mur$\varphi$ (Finite Horizon Probabilistic Mur$\varphi$) such extension of the Mur$\varphi$ verifier. We give experimental results comparing FHP-Mur$\varphi$ with (a finite horizon subset of) PRISM, a state-of-the-art symbolic model checker for Markov Chains. Our experimental results show that FHP-Mur$\varphi$ can effectively handle verification of BPCTL formulas for systems that are out of reach for PRISM, namely those involving arithmetic operations on the state variables (e.g. hybrid systems).
Address
Corporate Author (up) Thesis
Publisher Springer Place of Publication Editor Hu, A.J.; Martin, A.K.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 3312 Series Issue Edition
ISSN 3-540-23738-0 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimtz04 Serial 87
Permanent link to this record
 

 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Melatti, Igor; Minichino, Michele; Ciancamerla, Ester; Parisse, Andrea; Tronci, Enrico; Venturini Zilli, Marisa
Title Automatic Verification of a Turbogas Control System with the Mur$\varphi$ Verifier Type Conference Article
Year 2003 Publication Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings Abbreviated Journal
Volume Issue Pages 141-155
Keywords
Abstract Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur$\varphi$ verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Mur$\varphi$ verifier by importing the C language long double type (finite precision real numbers) into it. We give experimental results on running our extended Mur$\varphi$ on our TCS model. For example using Mur$\varphi$ we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas.
Address
Corporate Author (up) Thesis
Publisher Springer Place of Publication Editor Maler, O.; Pnueli, A.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 2623 Series Issue Edition
ISSN 3-540-00913-2 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dimmcptz03 Serial 88
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 (up) 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 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 (up) 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; 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 (up) 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
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 (up) 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; Tofani, Alberto; Pecorari, Marcello; Raparelli, Orazio; Intrigila, Benedetto; Melatti, Igor; Tronci, Enrico
Title A Case Study on Automated Generation of Integration Tests Type Conference Article
Year 2006 Publication Fdl Abbreviated Journal
Volume Issue Pages 278-284
Keywords
Abstract
Address
Corporate Author (up) Thesis
Publisher Ecsi Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 978-3-00-019710-9 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Dtprimt06 Serial 27
Permanent link to this record