MCLab Group List of Papers -- Query Results

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

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	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	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	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; 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	Campagnano, Edoardo; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico
	Title	Automatic Analysis of a Safety Critical Tele Control System			Type	Conference Article
	Year	2005	Publication	24th International Conference on: Computer Safety, Reliability, and Security (SAFECOMP)	Abbreviated Journal
	Volume		Issue		Pages	94-107
	Keywords
	Abstract	We show how the Mur$\varphi$ model checker can be used to automatically carry out safety analysis of a quite complex hybrid system tele-controlling vehicles traffic inside a safety critical transport infrastructure such as a long bridge or a tunnel. We present the Mur$\varphi$ model we developed towards this end as well as the experimental results we obtained by running the Mur$\varphi$ verifier on our model. Our experimental results show that the approach presented here can be used to verify safety of critical dimensioning parameters (e.g. bandwidth) of the telecommunication network embedded in a safety critical system.
	Address
	Corporate Author				Thesis
	Publisher	Springer	Place of Publication	Fredrikstad, Norway	Editor	Winther, R.; Gran, B. A.; Dahll, G.
	Language		Summary Language		Original Title
	Series Editor		Series Title	Lecture Notes in Computer Science	Abbreviated Series Title
	Series Volume	3688	Series Issue		Edition
	ISSN	3-540-29200-4	ISBN		Medium
	Area		Expedition		Conference
	Notes				Approved	yes
	Call Number	Sapienza @ mari @ safecomp05			Serial	32
Permanent link to this record



	Author	Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Tronci, Enrico; Verzino, Giovanni; Yushtein, Yuri
	Title	Model Checking Satellite Operational Procedures			Type	Conference Article
	Year	2011	Publication	DAta Systems In Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT. San Anton, Malta, EuroSpace.	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract	We present a model checking approach for the automatic verification of satellite operational procedures (OPs). Building a model for a complex system as a satellite is a hard task. We overcome this obstruction by using a suitable simulator (SIMSAT) for the satellite. Our approach aims at improving OP quality assurance by automatic exhaustive exploration of all possible simulation scenarios. Moreover, our solution decreases OP verification costs by using a model checker (CMurphi) to automatically drive the simulator. We model OPs as user-executed programs observing the simulator telemetries and sending telecommands to the simulator. In order to assess feasibility of our approach we present experimental results on a simple meaningful scenario. Our results show that we can save up to 90% of verification time.
	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 @ Dasia11			Serial	13
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	Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
	Title	Validation and verification issues in a timeline-based planning system			Type	Journal Article
	Year	2010	Publication	The Knowledge Engineering Review	Abbreviated Journal
	Volume	25	Issue	03	Pages	299-318
	Keywords
	Abstract	One of the key points to take into account to foster effective introduction of AI planning and scheduling systems in real world is to develop end user trust in the related technologies. Automated planning and scheduling systems often brings solutions to the users which are neither Ã¢â‚¬Å“obviousÃ¢â‚¬Â nor immediately acceptable for them. This is due to the ability of these tools to take into account quite an amount of temporal and causal constraints and to employ resolution processes often designed to optimize the solution with respect to non trivial evaluation functions. To increase technology trust, the study of tools for verifying and validating plans and schedules produced by AI systems might be instrumental. In general, validation and verification techniques represent a needed complementary technology in developing domain independent architectures for automated problem solving. This paper presents a preliminary report of the issues concerned with the use of two software tools for formal verification of finite state systems to the validation of the solutions produced by MrSPOCK, a recent effort for building a timeline based planning tool in an ESA project.
	Address
	Corporate Author				Thesis
	Publisher	Cambridge University Press	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 @ Cffot10			Serial	18
Permanent link to this record



	Author	Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
	Title	Flexible Plan Verification: Feasibility Results			Type	Conference Article
	Year	2009	Publication	16th RCRA International Workshop on “Experimental evaluation of algorithms for solving problems with combinatorial explosion” (RCRA). Proceedings	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 @ Rcra09			Serial	22
Permanent link to this record



	Author	Cesta, Amedeo; Finzi, Alberto; Fratini, Simone; Orlandini, Andrea; Tronci, Enrico
	Title	Verifying Flexible Timeline-based Plans			Type	Conference Article
	Year	2009	Publication	E-Proc. of ICAPS Workshop on Validation and Verification of Planning and Scheduling Systems	Abbreviated Journal
	Volume		Issue		Pages
	Keywords
	Abstract	The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verification method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study.
	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 @ Vvps09			Serial	23
Permanent link to this record