| Records |
| 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 |
Equational Programming in lambda-calculus |
Type |
Conference Article |
| Year |
1991 |
Publication |
Sixth Annual IEEE Symposium on Logic in Computer Science (LICS) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
191-202 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
IEEE Computer Society |
Place of Publication |
Amsterdam, The Netherlands |
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 @ lics91 |
Serial |
58 |
| Permanent link to this record |
| |
|
| |
| Author |
Böhm, Corrado; Tronci, Enrico |
| Title |
X-Separability and Left-Invertibility in lambda-calculus |
Type |
Conference Article |
| Year |
1987 |
Publication |
Symposium on Logic in Computer Science (LICS) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
320-328 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
IEEE Computer Society |
Place of Publication |
Ithaca, New York, 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 @ lics87 |
Serial |
63 |
| Permanent link to this record |
| |
|
| |
| Author |
Martinelli, Marco; Tronci, Enrico; Dipoppa, Giovanni; Balducelli, Claudio |
| Title |
Electric Power System Anomaly Detection Using Neural Networks |
Type |
Conference Article |
| Year |
2004 |
Publication |
8th International Conference on: Knowledge-Based Intelligent Information and Engineering Systems (KES) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
1242-1248 |
| Keywords |
|
| Abstract |
The aim of this work is to propose an approach to monitor and protect Electric Power System by learning normal system behaviour at substations level, and raising an alarm signal when an abnormal status is detected; the problem is addressed by the use of autoassociative neural networks, reading substation measures. Experimental results show that, through the proposed approach, neural networks can be used to learn parameters underlaying system behaviour, and their output processed to detecting anomalies due to hijacking of measures, changes in the power network topology (i.e. transmission lines breaking) and unexpected power demand trend. |
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
Springer |
Place of Publication |
Wellington, New Zealand |
Editor |
Negoita, M.G.; Howlett, R.J.; Jain, L.C. |
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
| Series Volume |
3213 |
Series Issue |
|
Edition |
|
| ISSN |
3-540-23318-0 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ kes04 |
Serial |
35 |
| 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 |
Conference Article |
| Year |
2008 |
Publication |
In E-Proc. of ICAPS Workshop on Knowledge Engineering for Planning and Scheduling |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
|
| 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 |
|
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 @ Keps08 |
Serial |
25 |
| 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 |
Tronci, Enrico |
| Title |
Defining Data Structures via Böhm-Out |
Type |
Journal Article |
| Year |
1995 |
Publication |
J. Funct. Program. |
Abbreviated Journal |
|
| Volume |
5 |
Issue |
1 |
Pages |
51-64 |
| Keywords |
|
| Abstract |
We show that any recursively enumerable subset of a data structure can be regarded as the solution set to a B??hm-out problem. |
| 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 @ jfp95 |
Serial |
57 |
| Permanent link to this record |
| |
|
| |
| Author |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico |
| Title |
Control Software Visualization |
Type |
Conference Article |
| Year |
2012 |
Publication |
Proceedings of INFOCOMP 2012, The Second International Conference on Advanced Communications and Computation |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
15-20 |
| Keywords |
|
| Abstract |
|
| Address |
|
| Corporate Author |
|
Thesis |
|
| Publisher |
ThinkMind |
Place of Publication |
|
Editor |
|
| Language |
|
Summary Language |
|
Original Title |
|
| Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
| Series Volume |
|
Series Issue |
|
Edition |
|
| ISSN |
978-1-61208-226-4 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ infocomp2012 |
Serial |
100 |
| Permanent link to this record |
| |
|
| |
| Author |
Böhm, Corrado; Tronci, Enrico |
| Title |
About Systems of Equations, X-Separability, and Left-Invertibility in the lambda-Calculus |
Type |
Journal Article |
| Year |
1991 |
Publication |
Inf. Comput. |
Abbreviated Journal |
|
| Volume |
90 |
Issue |
1 |
Pages |
1-32 |
| 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 @ infcomp91 |
Serial |
59 |
| Permanent link to this record |
| |
|
| |
| Author |
Intrigila, Benedetto; Magazzeni, Daniele; Melatti, Igor; Tronci, Enrico |
| Title |
A Model Checking Technique for the Verification of Fuzzy Control Systems |
Type |
Conference Article |
| Year |
2005 |
Publication |
CIMCA '05: Proceedings of the International Conference on Computational Intelligence for Modelling, Control and Automation and International Conference on Intelligent Agents, Web Technologies and Internet Commerce Vol-1 (CIMCA-IAWTIC'06) |
Abbreviated Journal |
|
| Volume |
|
Issue |
|
Pages |
536-542 |
| Keywords |
|
| Abstract |
Fuzzy control is well known as a powerful technique for designing and realizing control systems. However, statistical evidence for their correct behavior may be not enough, even when it is based on a large number of samplings. In order to provide a more systematic verification process, the cell-to-cell mapping technology has been used in a number of cases as a verification tool for fuzzy control systems and, more recently, to assess their optimality and robustness. However, cell-to-cell mapping is typically limited in the number of cells it can explore. To overcome this limitation, in this paper we show how model checking techniques may be instead used to verify the correct behavior of a fuzzy control system. To this end, we use a modified version of theMurphi verifier, which ease the modeling phase by allowing to use finite precision real numbers and external C functions. In this way, also already designed simulators may be used for the verification phase. With respect to the cell mapping technique, our approach appears to be complementary; indeed, it explores a much larger number of states, at the cost of being less informative on the global dynamic of the system. |
| 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-2504-0-01 |
ISBN |
|
Medium |
|
| Area |
|
Expedition |
|
Conference |
|
| Notes |
|
Approved |
yes |
| Call Number |
Sapienza @ mari @ Immt05 |
Serial |
75 |
| Permanent link to this record |
