MCLab Group List of Papers -- Query Results

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

Search & Display Options

Select All Deselect All

[1–10] << 11 12 13 14 15 >>

List View

Citations

Details

	Records
	Author	Intrigila, Benedetto; Salvo, Ivano; Sorgi, Stefano
	Title	A characterization of weakly Church-Rosser abstract reduction systems that are not Church-Rosser			Type	Journal Article
	Year	2001	Publication	Information and Computation	Abbreviated Journal
	Volume	171	Issue	2	Pages	137-155
	Keywords
	Abstract	Basic properties of rewriting systems can be stated in the framework of abstract reduction systems (ARS). Properties like confluence (or Church-Rosser, CR) and weak confluence (or weak Church-Rosser, WCR) and their relationships can be studied in this setting: as a matter of fact, well-known counterexamples to the implication WCR CR have been formulated as ARS. In this paper, starting from the observation that such counterexamples are structurally similar, we set out a graph-theoretic characterization of WCR ARS that is not CR in terms of a suitable class of reduction graphs, such that in every WCR not CR ARS, we can embed at least one element of this class. Moreover, we give a tighter characterization for a restricted class of ARS enjoying a suitable regularity condition. Finally, as a consequence of our approach, we prove some interesting results about ARS using the mathematical tools developed. In particular, we prove an extension of the NewmanÃ¢â‚¬â„¢s lemma and we find out conditions that, once assumed together with WCR property, ensure the unique normal form property. The Appendix treats two interesting examples, both generated by graph-rewriting rules, with specific combinatorial properties.
	Address
	Corporate Author				Thesis
	Publisher	Academic Press, Inc.	Place of Publication	Duluth, MN, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0890-5401	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ Intrigila-Salvo-Sorgi:01			Serial	68
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	Cecconi, Michele; Tronci, Enrico
	Title	Requirements Formalization and Validation for a Telecommunication Equipment Protection Switcher			Type	Conference Article
	Year	2000	Publication	Hase	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract
	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	0-7695-0927-4	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ CeTro00			Serial	29
Permanent link to this record



	Author	Tronci, Enrico
	Title	Automatic Synthesis of Control Software for an Industrial Automation Control System			Type	Conference Article
	Year	1999	Publication	Proc.of: 14th IEEE International Conference on: Automated Software Engineering (ASE)	Abbreviated Journal
	Volume		Issue		Pages	247-250
	Keywords
	Abstract	We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design, followed by automatic verification. Our experimental results show that for industrial automation control systems, automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design, followed by automatic verification.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication	Cocoa Beach, Florida, USA	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 @ ase99			Serial	49
Permanent link to this record



	Author	Tronci, Enrico
	Title	Formally Modeling a Metal Processing Plant and its Closed Loop Specifications			Type	Conference Article
	Year	1999	Publication	4th IEEE International Symposium on High-Assurance Systems Engineering (HASE)	Abbreviated Journal
	Volume		Issue		Pages	151
	Keywords
	Abstract	We present a case study on automatic synthesis of control software from formal specifications for an industrial automation control system. Our aim is to compare the effectiveness (i.e. design effort and controller quality) of automatic controller synthesis from closed loop formal specifications with that of manual controller design followed by automatic verification. The system to be controlled (plant) models a metal processing facility near Karlsruhe. We succeeded in automatically generating C code implementing a (correct by construction) embedded controller for such a plant from closed loop formal specifications. Our experimental results show that for industrial automation control systems automatic synthesis is a viable and profitable (especially as far as design effort is concerned) alternative to manual design followed by automatic verification.
	Address
	Corporate Author				Thesis
	Publisher	IEEE Computer Society	Place of Publication	Washington, D.C, USA	Editor
	Language		Summary Language		Original Title
	Series Editor		Series Title		Abbreviated Series Title
	Series Volume		Series Issue		Edition
	ISSN	0-7695-0418-3	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ hase99			Serial	50
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	Fantechi, Alessandro; Gnesi, Stefania; Mazzanti, Franco; Pugliese, Rosario; Tronci, Enrico
	Title	A Symbolic Model Checker for ACTL			Type	Conference Article
	Year	1998	Publication	International Workshop on Current Trends in Applied Formal Method (FM-Trends)	Abbreviated Journal
	Volume		Issue		Pages	228-242
	Keywords
	Abstract	We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Boppard, Germany	Editor	Hutter, D.; Stephan, W.; Traverso, P.; Ullmann, M.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	1641	Series Issue		Edition
	ISSN	3-540-66462-9	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ fm-trends98			Serial	51
Permanent link to this record



	Author	Tronci, Enrico
	Title	Automatic Synthesis of Controllers from Formal Specifications			Type	Conference Article
	Year	1998	Publication	Proc of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM)	Abbreviated Journal
	Volume		Issue		Pages	134-143
	Keywords
	Abstract	Many safety critical reactive systems are indeed embedded control systems. Usually a control system can be partitioned into two main subsystems: a controller and a plant. Roughly speaking: the controller observes the state of the plant and sends commands (stimulus) to the plant to achieve predefined goals. We show that when the plant can be modeled as a deterministic finite state system (FSS) it is possible to effectively use formal methods to automatically synthesize the program implementing the controller from the plant model and the given formal specifications for the closed loop system (plant+controller). This guarantees that the controller program is correct by construction. To the best of our knowledge there is no previously published effective algorithm to extract executable code for the controller from closed loop formal specifications. We show practical usefulness of our techniques by giving experimental results on their use to synthesize C programs implementing optimal controllers (OCs) for plants with more than 109 states.
	Address
	Corporate Author				Thesis
	Publisher		Place of Publication	Brisbane, Queensland, Australia	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 @ icfem98			Serial	52
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	Tronci, Enrico
	Title	On Computing Optimal Controllers for Finite State Systems			Type	Conference Article
	Year	1997	Publication	CDC '97: Proceedings of the 36th IEEE International Conference on Decision and Control	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract
	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		ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ cdc97			Serial	66
Permanent link to this record