MCLab Group List of Papers -- Query Results

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

Search & Display Options

Select All Deselect All

<< 1 2 3 4 5 6 7 8 9 10 >> [11–15]

List View

Citations

Details

	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	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	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	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	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	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	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	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	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	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	Sapienza @ mari @ Astra08			Serial	24
Permanent link to this record