| |
Records |
Links |
|
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 |
Intrigila, Benedetto; Melatti, Igor; Tofani, Alberto; Macchiarelli, Guido |
|
| |
Title |
Computational models of myocardial endomysial collagen arrangement |
Type |
Journal Article |
| |
Year |
2007 |
Publication |
Computer Methods and Programs in Biomedicine |
Abbreviated Journal |
|
|
| |
Volume |
86 |
Issue |
3 |
Pages |
232-244 |
|
| |
Keywords |
|
|
| |
Abstract |
Collagen extracellular matrix is one of the factors related to high passive stiffness of cardiac muscle. However, the architecture and the mechanical aspects of the cardiac collagen matrix are not completely known. In particular, endomysial collagen contribution to the passive mechanics of cardiac muscle as well as its micro anatomical arrangement is still a matter of debate. In order to investigate mechanical and structural properties of endomysial collagen, we consider two alternative computational models of some specific aspects of the cardiac muscle. These two models represent two different views of endomysial collagen distribution: (1) the traditional view and (2) a new view suggested by the data obtained from scanning electron microscopy (SEM) in NaOH macerated samples (a method for isolating collagen from the other tissue). We model the myocardial tissue as a net of spring elements representing the cardiomyocytes together with the endomysial collagen distribution. Each element is a viscous elastic spring, characterized by an elastic and a viscous constant. We connect these springs to imitate the interconnections between collagen fibers. Then we apply to the net of springs some external forces of suitable magnitude and direction, obtaining an extension of the net itself. In our setting, the ratio forces magnitude /net extension is intended to model the stress /strain ratio of a microscopical portion of the myocardial tissue. To solve the problem of the correct identification of the values of the different parameters involved, we use an artificial neural network approach. In particular, we use this technique to learn, given a distribution of external forces, the elastic constants of the springs needed to obtain a desired extension as an equilibrium position. Our experimental findings show that, in the model of collagen distribution structured according to the new view, a given stress /strain ratio (of the net of springs, in the sense specified above) is obtained with much smaller (w.r.t. the other model, corresponding to the traditional view) elasticity constants of the springs. This seems to indicate that by an appropriate structure, a given stiffness of the myocardial tissue can be obtained with endomysial collagen fibers of much smaller size. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Elsevier North-Holland, Inc. |
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 |
0169-2607 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ Imtm07 |
Serial |
82 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Pugliese, Rosario; Tronci, Enrico |
|
| |
Title |
Automatic Verification of a Hydroelectric Power Plant |
Type |
Conference Article |
| |
Year |
1996 |
Publication |
Third International Symposium of Formal Methods Europe (FME), Co-Sponsored by IFIP WG 14.3 |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
425-444 |
|
| |
Keywords |
|
|
| |
Abstract |
We analyze the specification of a hydroelectric power plant by ENEL (the Italian Electric Company). Our goal is to show that for the specification of the plant (its control system in particular) some given properties hold. We were provided with an informal specification of the plant. From such informal specification we wrote a formal specification using the CCS/Meije process algebra formalism. We defined properties using μ-calculus. Automatic verification was carried out using model checking. This was done by translating our process algebra definitions (the model) and μ-calculus formulas into BDDs. In this paper we present the informal specification of the plant, its formal specification, some of the properties we verified and experimental results. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
Oxford, UK |
Editor |
Gaudel, M.-C.; Woodcock, J. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
1051 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-60973-3 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ fme96 |
Serial |
53 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Böhm, Corrado; Piperno, Adolfo; Tronci, Enrico |
|
| |
Title |
Solving Equations in λ-calculus |
Type |
Conference Article |
| |
Year |
1989 |
Publication |
Proc. of: Logic Colloquium 88 |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
|
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
|
Place of Publication |
Padova - Italy |
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 @ logic-colloquium-88 |
Serial |
62 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry |
|
| |
Title |
Model Checking Nash Equilibria in MAD Distributed Systems |
Type |
Conference Article |
| |
Year |
2008 |
Publication |
FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
1-8 |
|
| |
Keywords |
Model Checking, MAD Distributed System, Nash Equilibrium |
|
| |
Abstract |
We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Press |
Place of Publication |
Piscataway, NJ, USA |
Editor |
Cimatti, A.; Jones, R. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-1-4244-2735-2 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ MarMelSalTroAlvCle08 |
Serial |
93 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa |
|
| |
Title |
Exploiting Transition Locality in the Disk Based Mur$\varphi$ Verifier |
Type |
Conference Article |
| |
Year |
2002 |
Publication |
4th International Conference on Formal Methods in Computer-Aided Design (FMCAD) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
202-219 |
|
| |
Keywords |
|
|
| |
Abstract |
The main obstruction to automatic verification of Finite State Systems is the huge amount of memory required to complete the verification task (state explosion). This motivates research on distributed as well as disk based verification algorithms. In this paper we present a disk based Breadth First Explicit State Space Exploration algorithm as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm exploits transition locality (i.e. the statistical fact that most transitions lead to unvisited states or to recently visited states) to decrease disk read accesses thus reducing the time overhead due to disk usage. A disk based verification algorithm for Mur$\varphi$ has been already proposed in the literature. To measure the time speed up due to locality exploitation we compared our algorithm with such previously proposed algorithm. Our experimental results show that our disk based verification algorithm is typically more than 10 times faster than such previously proposed disk based verification algorithm. To measure the time overhead due to disk usage we compared our algorithm with RAM based verification using the (standard) Mur$\varphi$ verifier with enough memory to complete the verification task. Our experimental results show that even when using 1/10 of the RAM needed to complete verification, our disk based algorithm is only between 1.4 and 5.3 times (3 times on average) slower than (RAM) Mur$\varphi$ with enough RAM memory to complete the verification task at hand. Using our disk based Mur$\varphi$ we were able to complete verification of a protocol with about $10^9$ reachable states. This would require more than 5 gigabytes of RAM using RAM based Mur$\varphi$. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
Springer |
Place of Publication |
Portland, OR, USA |
Editor |
Aagaard, M.; O'Leary, J.W. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
| |
Series Volume |
2517 |
Series Issue |
|
Edition |
|
|
| |
ISSN |
3-540-00116-6 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ fmcad02 |
Serial |
41 |
|
| Permanent link to this record |
| |
|
| |
|
Author |
Tronci, Enrico |
|
| |
Title |
Hardware Verification, Boolean Logic Programming, Boolean Functional Programming |
Type |
Conference Article |
| |
Year |
1995 |
Publication |
Tenth Annual IEEE Symposium on Logic in Computer Science (LICS) |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
408-418 |
|
| |
Keywords |
|
|
| |
Abstract |
One of the main obstacles to automatic verification of finite state systems (FSSs) is state explosion. In this respect automatic verification of an FSS M using model checking and binary decision diagrams (BDDs) has an intrinsic limitation: no automatic global optimization of the verification task is possible until a BDD representation for M is generated. This is because systems and specifications are defined using different languages. To perform global optimization before generating a BDD representation for M we propose to use the same language to define systems and specifications. We show that first order logic on a Boolean domain yields an efficient functional programming language that can be used to represent, specify and automatically verify FSSs, e.g. on a SUN Sparc Station 2 we were able to automatically verify a 64 bit commercial multiplier. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Computer Society |
Place of Publication |
San Diego, California |
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 @ lics95 |
Serial |
56 |
|
| 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 |
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 |
| |
|
| |
|
Author |
Tronci, Enrico |
|
| |
Title |
Optimal Finite State Supervisory Control |
Type |
Conference Article |
| |
Year |
1996 |
Publication |
CDC '96: Proceedings of the 35th IEEE International Conference on Decision and Control |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
|
|
| |
Keywords |
|
|
| |
Abstract |
Supervisory Controllers are Discrete Event Dynamic Systems (DEDSs) forming the discrete core of a Hybrid Control System. We address the problem of automatic synthesis of Optimal Finite State Supervisory Controllers (OSCs). We show that Boolean First Order Logic (BFOL) and Binary Decision Diagrams (BDDs) are an effective methodological and practical framework for Optimal Finite State Supervisory Control. Using BFOL programs (i.e. systems of boolean functional equations) and BDDs we give a symbolic (i.e. BDD based) algorithm for automatic synthesis of OSCs. Our OSC synthesis algorithm can handle arbitrary sets of final states as well as plant transition relations containing loops and uncontrollable events (e.g. failures). We report on experimental results on the use of our OSC synthesis algorithm to synthesize a C program implementing a minimum fuel OSC for two autonomous vehicles moving on a 4 x 4 grid. |
|
| |
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 @ cdc96 |
Serial |
67 |
|
| Permanent link to this record |
