| Records |
| Author |
Tronci, Enrico |
| Title |
Equational Programming in Lambda-Calculus via SL-Systems. Part 1 |
Type |
Journal Article |
| Year |
1996 |
Publication |
Theoretical Computer Science |
Abbreviated Journal |
|
| Volume |
160 |
Issue  |
1&2 |
Pages |
145-184 |
| 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 @ tcs96 |
Serial |
54 |
| Permanent link to this record |
| |
|
| |
| Author |
Tronci, Enrico |
| Title |
Equational Programming in Lambda-Calculus via SL-Systems. Part 2 |
Type |
Journal Article |
| Year |
1996 |
Publication |
Theoretical Computer Science |
Abbreviated Journal |
|
| Volume |
160 |
Issue |
1&2 |
Pages |
185-216 |
| 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 @ tcs96a |
Serial |
55 |
| Permanent link to this record |
| |
|
| |
| Author |
Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E. |
| Title |
SyLVaaS: System Level Formal Verification as a Service |
Type |
Journal Article |
| Year |
2016 |
Publication |
Fundamenta Informaticae |
Abbreviated Journal |
|
| Volume |
149 |
Issue |
1-2 |
Pages |
101-132 |
| 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 |
no |
| Call Number |
MCLab @ davi @ DBLP:journals/fuin/ManciniMMMT16 |
Serial |
160 |
| Permanent link to this record |
| |
|
| |
| Author |
Alimguzhin, V.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E. |
| Title |
Linearising Discrete Time Hybrid Systems |
Type |
Journal Article |
| Year |
2017 |
Publication |
IEEE Transactions on Automatic Control |
Abbreviated Journal |
|
| Volume |
62 |
Issue |
10 |
Pages |
5357-5364 |
| Keywords |
|
| Abstract |
Model Based Design approaches for embedded systems aim at generating correct-by-construction control software, guaranteeing that the closed loop system (controller and plant) meets given system level formal specifications. This technical note addresses control synthesis for safety and reachability properties of possibly non-linear discrete time hybrid systems. By means of syntactical transformations that require non-linear terms to be Lipschitz continuous functions, we over-approximate non-linear dynamics with a linear system whose controllers are guaranteed to be controllers of the original system. We evaluate performance of our approach on meaningful control synthesis benchmarks, also comparing it to a state-of-the-art tool. |
| 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 |
0018-9286 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
no |
| Call Number |
Sapienza @ mari @ ref7902199 |
Serial |
164 |
| Permanent link to this record |
| |
|
| |
| Author |
Cesta, Amedeo; Fratini, Simone; Orlandini, Andrea; Finzi, Alberto; Tronci, Enrico |
| Title |
Flexible Plan Verification: Feasibility Results |
Type |
Journal Article |
| Year |
2011 |
Publication |
Fundamenta Informaticae |
Abbreviated Journal |
|
| Volume |
107 |
Issue |
2 |
Pages |
111-137 |
| 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 @ fi11 |
Serial |
15 |
| Permanent link to this record |
| |
|
| |
| Author |
Gribaudo, Marco; Horváth, Andras; Bobbio, Andrea; Tronci, Enrico; Ciancamerla, Ester; Minichino, Michele |
| Title |
Fluid Petri Nets and hybrid model checking: a comparative case study |
Type |
Journal Article |
| Year |
2003 |
Publication |
Int. Journal on: Reliability Engineering & System Safety |
Abbreviated Journal |
|
| Volume |
81 |
Issue |
3 |
Pages |
239-257 |
| Keywords |
|
| Abstract |
The modeling and analysis of hybrid systems is a recent and challenging research area which is actually dominated by two main lines: a functional analysis based on the description of the system in terms of discrete state (hybrid) automata (whose goal is to ascertain conformity and reachability properties), and a stochastic analysis (whose aim is to provide performance and dependability measures). This paper investigates a unifying view between formal methods and stochastic methods by proposing an analysis methodology of hybrid systems based on Fluid Petri Nets (FPNs). FPNs can be analyzed directly using appropriate tools. Our paper shows that the same FPN model can be fed to different functional analyzers for model checking. In order to extensively explore the capability of the technique, we have converted the original FPN into languages for discrete as well as hybrid as well as stochastic model checkers. In this way, a first comparison among the modeling power of well known tools can be carried out. Our approach is illustrated by means of a ’real world’ hybrid system: the temperature control system of a co-generative plant. |
| 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 |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ ress03 |
Serial |
40 |
| Permanent link to this record |
| |
|
| |
| Author |
Piperno, Adolfo; Tronci, Enrico |
| Title |
Regular Systems of Equations in λ-calculus |
Type |
Journal Article |
| Year |
1990 |
Publication |
Int. J. Found. Comput. Sci. |
Abbreviated Journal |
|
| Volume |
1 |
Issue |
3 |
Pages |
325-340 |
| Keywords |
|
| Abstract |
Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable. |
| 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 @ ijfcs90 |
Serial |
60 |
| Permanent link to this record |
| |
|
| |
| Author |
Hayes, B. P. ; Melatti, I.; Mancini, T.; Prodanovic, M.; Tronci, E. |
| Title |
Residential Demand Management using Individualised Demand Aware Price Policies |
Type |
Journal Article |
| Year |
2017 |
Publication |
IEEE Transactions On Smart Grid |
Abbreviated Journal |
|
| Volume |
8 |
Issue |
3 |
Pages |
1284-1294 |
| 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 |
no |
| Call Number |
MCLab @ davi @ |
Serial |
157 |
| Permanent link to this record |
| |
|
| |
| Author |
Bobbio, Andrea; Ciancamerla, Ester; Minichino, Michele; Tronci, Enrico |
| Title |
Functional analysis of a telecontrol system and stochastic measures of its GSM/GPRS connections |
Type |
Journal Article |
| Year |
2005 |
Publication |
Archives of Transport – International Journal of Transport Problems |
Abbreviated Journal |
|
| Volume |
17 |
Issue |
3-4 |
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 @ jtp05 |
Serial |
31 |
| Permanent link to this record |
| |
|
| |
| Author |
Gorrieri, Roberto; Lanotte, Ruggero; Maggiolo-Schettini, Andrea; Martinelli, Fabio; Tini, Simone; Tronci, Enrico |
| Title |
Automated analysis of timed security: a case study on web privacy |
Type |
Journal Article |
| Year |
2004 |
Publication |
International Journal of Information Security |
Abbreviated Journal |
|
| Volume |
2 |
Issue |
3-4 |
Pages |
168-186 |
| Keywords |
|
| Abstract |
This paper presents a case study on an automated analysis of real-time security models. The case study on a web system (originally proposed by Felten and Schneider) is presented that shows a timing attack on the privacy of browser users. Three different approaches are followed: LH-Timed Automata (analyzed using the model checker HyTech), finite-state automata (analyzed using the model checker NuSMV), and process algebras (analyzed using the model checker CWB-NC). A comparative analysis of these three approaches is given. |
| 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 @ ijis04 |
Serial |
33 |
| Permanent link to this record |
