|
Records |
Links |
|
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 |
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 |
Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa |
|
|
Title |
Exploiting Transition Locality in Automatic Verification |
Type |
Conference Article |
|
Year |
2001 |
Publication |
11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
259-274 |
|
|
Keywords |
|
|
|
Abstract |
In this paper we present an algorithm to contrast state explosion when using Explicit State Space Exploration to verify protocols. We show experimentally that protocols exhibit transition locality. We present a verification algorithm that exploits transition locality as well as an implementation of it within the Mur$\varphi$ verifier. Our algorithm is compatible with all Breadth First (BF) optimization techniques present in the Mur$\varphi$ verifier and it is by no means a substitute for any of them. In fact, since our algorithm trades space with time, it is typically most useful when one runs out of memory and has already used all other state reduction techniques present in the Mur$\varphi$ verifier. Our experimental results show that using our approach we can typically save more than 40% of RAM with an average time penalty of about 50% when using (Mur$\varphi$) bit compression and 100% when using bit compression and hash compaction. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
Springer |
Place of Publication |
Livingston, Scotland, UK |
Editor |
Margaria, T.; Melham, T.F. |
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
Lecture Notes in Computer Science |
Abbreviated Series Title |
|
|
|
Series Volume |
2144 |
Series Issue |
|
Edition |
|
|
|
ISSN |
3-540-42541-1 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ charme01 |
Serial |
44 |
|
Permanent link to this record |
|
|
|
|
Author |
Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa |
|
|
Title |
A Probabilistic Approach to Automatic Verification of Concurrent Systems |
Type |
Conference Article |
|
Year |
2001 |
Publication |
8th Asia-Pacific Software Engineering Conference (APSEC) |
Abbreviated Journal |
|
|
|
Volume |
|
Issue |
|
Pages |
317-324 |
|
|
Keywords |
|
|
|
Abstract |
The main barrier to automatic verification of concurrent systems is the huge amount of memory required to complete the verification task (state explosion). In this paper we present a probabilistic algorithm for automatic verification via model checking. Our algorithm trades space with time. In particular, when memory is full because of state explosion our algorithm does not give up verification. Instead it just proceeds at a lower speed and its results will only hold with some arbitrarily small error probability. Our preliminary experimental results show that by using our probabilistic algorithm we can typically save more than 30% of RAM with an average time penalty of about 100% w.r.t. a deterministic state space exploration with enough memory to complete the verification task. This is better than giving up the verification task because of lack of memory. |
|
|
Address |
|
|
|
Corporate Author |
|
Thesis |
|
|
|
Publisher |
IEEE Computer Society |
Place of Publication |
Macau, China |
Editor |
|
|
|
Language |
|
Summary Language |
|
Original Title |
|
|
|
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
|
Series Volume |
|
Series Issue |
|
Edition |
|
|
|
ISSN |
0-7695-1408-1 |
ISBN |
|
Medium |
|
|
|
Area |
|
Expedition |
|
Conference |
|
|
|
Notes |
|
Approved |
yes |
|
|
Call Number |
Sapienza @ mari @ apsec01 |
Serial |
43 |
|
Permanent link to this record |
|
|
|
|
Author |
Verzino Giovanni ; Cavaliere, Federico; Mari, Federico; Melatti, Igor; Minei, Giovanni; Salvo, Ivano; Yushtein, Yuri; Tronci, Enrico |
|
|
Title |
Model checking driven simulation of sat procedures |
Type |
Conference Article |
|
Year |
2012 |
Publication |
Proceedings of 12th International Conference on Space Operations (SpaceOps 2012) |
Abbreviated Journal |
International Conference on Space Operations |
|
|
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 |
no |
|
|
Call Number |
Sapienza @ melatti @ |
Serial |
117 |
|
Permanent link to this record |