|   | 
Details
   web
Records
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 (down) Sapienza @ mari @ cdc12 Serial 96
Permanent link to this record
 

 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems Type Conference Article
Year 2010 Publication Computer Aided Verification Abbreviated Journal
Volume Issue Pages 180-195
Keywords
Abstract We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.
Address
Corporate Author Thesis
Publisher Springer Berlin / Heidelberg Place of Publication Editor Touili, T.; Cook, B.; Jackson, P.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 6174 Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number (down) Sapienza @ mari @ cav2010 Serial 16
Permanent link to this record
 

 
Author Bucciarelli, Antonio; Salvo, Ivano
Title Totality, Definability and Boolean Circuits Type Journal Article
Year 1998 Publication Abbreviated Journal
Volume 1443 Issue Pages 808-819
Keywords
Abstract In the type frame originating from the flat domain of boolean values, we single out elements which are hereditarily total. We show that these elements can be defined, up to total equivalence, by sequential programs. The elements of an equivalence class of the totality equivalence relation (totality class) can be seen as different algorithms for computing a given set-theoretic boolean function. We show that the bottom element of a totality class, which is sequential, corresponds to the most eager algorithm, and the top to the laziest one. Finally we suggest a link between size of totality classes and a well known measure of complexity of boolean functions, namely their sensitivity.
Address
Corporate Author Thesis
Publisher Springer 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 (down) Sapienza @ mari @ bucciarelli-salvo:98 Serial 70
Permanent link to this record
 

 
Author Bucciarelli, Antonio; Piperno, Adolfo; Salvo, Ivano
Title Intersection types and λ-definability Type Journal Article
Year 2003 Publication Mathematical Structures in Computer Science Abbreviated Journal
Volume 13 Issue 1 Pages 15-53
Keywords
Abstract This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.
Address
Corporate Author Thesis
Publisher Cambridge University Press Place of Publication New York, NY, USA Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0960-1295 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number (down) Sapienza @ mari @ Bucciarelli-Piperno-Salvo:MSCS-03 Serial 69
Permanent link to this record
 

 
Author Bucciarelli, Antonio; de Lorenzis, Silvia; Piperno, Adolfo; Salvo, Ivano
Title Some Computational Properties of Intersection Types (Extended Abstract) Type Journal Article
Year 1999 Publication Abbreviated Journal
Volume Issue Pages 109-118
Keywords lambda calculusCurry types, intersection types, lambda-definability, lambda-terms, strong normalization
Abstract This paper presents a new method for comparing computation-properties of λ-terms typeable with intersection types with respect to terms typeable with Curry types. In particular, strong normalization and λ-definability are investigated. A translation is introduced from intersection typing derivations to Curry typeable terms; the main feature of the proposed technique is that the translation is preserved by β-reduction. This allows to simulate a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach naturally leads to prove strong normalization in the intersection system by means of purely syntactical techniques. In addition, the presented method enables us to give a proof of a conjecture proposed by Leivant in 1990, namely that all functions uniformly definable using intersection types are already definable using Curry types.
Address
Corporate Author Thesis
Publisher IEEE Computer Society 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 (down) Sapienza @ mari @ bucciarelli-delorenzis-piperno-salvo:99 Serial 71
Permanent link to this record
 

 
Author Bartolini, Novella; Tronci, Enrico
Title On Optimizing Service Availability of an Internet Based Architecture for Infrastructure Protection Type Conference Article
Year 2006 Publication Cnip 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 yes
Call Number (down) Sapienza @ mari @ Bt06 Serial 28
Permanent link to this record
 

 
Author Bono, V.; Salvo, I.
Title A CuCh Interpretation of an Object-Oriented Language Type Journal Article
Year 2001 Publication Electronic Notes in Theoretical Computer Science Abbreviated Journal
Volume 50 Issue 2 Pages 159-177
Keywords
Abstract CuCh machine extends pure lambda–calculus with algebraic data types and provides a the possibility of defining functions over the disjoint sum of algebras. We exploit such natural form of overloading to define a functional interpretation of a simple, but significant fragment of a typical object-oriented language.
Address
Corporate Author 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 BOTH 2001, Bohm’s theorem: applications to Computer Science Theory (Satellite Workshop of ICALP 2001) Approved yes
Call Number (down) Sapienza @ mari @ Bono-Salvo:BOTH01 Serial 72
Permanent link to this record
 

 
Author Brizzolari, Francesco; Melatti, Igor; Tronci, Enrico; Della Penna, Giuseppe
Title Disk Based Software Verification via Bounded Model Checking Type Conference Article
Year 2007 Publication APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference Abbreviated Journal
Volume Issue Pages 358-365
Keywords
Abstract One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.
Address
Corporate Author Thesis
Publisher IEEE Computer Society Place of Publication Washington, DC, USA Editor
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 0-7695-3057-5 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number (down) Sapienza @ mari @ Bmtd07 Serial 76
Permanent link to this record
 

 
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 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 (down) Sapienza @ mari @ Barbanera-Dezani-Salvo-Sassone:01 Serial 73
Permanent link to this record
 

 
Author Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
Title Merging Planning, Scheduling & Verification – A Preliminary Analysis Type Conference Article
Year 2008 Publication In Proc. of 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA) 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 yes
Call Number (down) Sapienza @ mari @ Astra08 Serial 24
Permanent link to this record