Home << 1 2 3 4 5 6 7 >>
List View
 | 
Citations
 | 
Details
   web
Records
Author Mancini, T.; Mari, F.; Melatti, I.; Salvo, I.; Tronci, E.; Gruber, J.K.; Hayes, B.; Prodanovic, M.; Elmegaard, L.
Title (down) User Flexibility Aware Price Policy Synthesis for Smart Grids Type Conference Article
Year 2015 Publication Digital System Design (DSD), 2015 Euromicro Conference on Abbreviated Journal
Volume Issue Pages 478-485
Keywords Contracts; Current measurement; Load management; Power demand; Power measurement; State estimation; Substations; Grid State Estimation; Peak Shaving; Policy Robustness Verification; Price Policy Synthesis
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 @ preissler @ Mancini_etal2015_3 Serial 136
Permanent link to this record
 
 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title (down) Undecidability of Quantized State Feedback Control for Discrete Time Linear Hybrid Systems Type Book Chapter
Year 2012 Publication Theoretical Aspects of Computing – ICTAC 2012 Abbreviated Journal
Volume Issue Pages 243-258
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer Berlin Heidelberg Place of Publication Editor Roychoudhury, A.; D'Souza, M.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 7521 Series Issue Edition
ISSN ISBN 978-3-642-32942-5 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Mari2012 Serial 99
Permanent link to this record
 
 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Merli, Fabio; Tronci, Enrico
Title (down) System Level Formal Verification via Model Checking Driven Simulation Type Conference Article
Year 2013 Publication Proceedings of the 25th International Conference on Computer Aided Verification. July 13-19, 2013, Saint Petersburg, Russia Abbreviated Journal CAV 2013
Volume Issue Pages 296-312
Keywords
Abstract
Address
Corporate Author Thesis
Publisher Springer - Verlag Place of Publication Editor
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 8044 Series Issue Edition
ISSN 0302-9743 ISBN 978-3-642-39798-1 Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ Serial 113
Permanent link to this record
 
 
Author Mancini, Toni ; Mari, Federico ; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title (down) System Level Formal Verification via Distributed Multi-Core Hardware in the Loop Simulation Type Conference Article
Year 2014 Publication Proc. of the 22nd Euromicro International Conference on Parallel, Distributed and Network-Based Processing Abbreviated Journal Euromicro International Conference on Parallel, Distributed and Network-Based Processing
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 ISBN Medium
Area Expedition Conference
Notes Approved no
Call Number Sapienza @ melatti @ Serial 118
Permanent link to this record
 
 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title (down) Synthesizing Control Software from Boolean Relations Type Journal Article
Year 2012 Publication International Journal on Advances in Software Abbreviated Journal Intern. Journal on Advances in SW
Volume vol. 5, nr 3&4 Issue Pages 212-223
Keywords Control Software Synthesis; Embedded Systems; Model Checking
Abstract Many software as well digital hardware automatic
synthesis methods define the set of
implementations meeting the given system
specifications with a boolean relation K. In
such a context a fundamental step in the software
(hardware) synthesis process is finding effective
solutions to the functional equation defined by
K. This entails finding a (set of) boolean
function(s) F (typically represented using
OBDDs, Ordered Binary Decision Diagrams)
such that: 1) for all x for which K is
satisfiable, K(x, F(x)) = 1 holds; 2) the
implementation of F is efficient with respect
to given implementation parameters such as code
size or execution time. While this problem has
been widely studied in digital hardware synthesis,
little has been done in a software synthesis
context. Unfortunately, the approaches developed
for hardware synthesis cannot be directly used in
a software context. This motivates investigation
of effective methods to solve the above problem
when F has to be implemented with software. In
this paper, we present an algorithm that, from an
OBDD representation for K, generates a C code
implementation for F that has the same size as
the OBDD for F and a worst case execution time
linear in nr, being n = |x| the number of
input arguments for functions in F and r the
number of functions in F. Moreover, a formal
proof of the proposed algorithm correctness is
also shown. Finally, we present experimental
results showing effectiveness of the proposed
algorithm.
Address
Corporate Author Thesis
Publisher IARIA Place of Publication Editor Luigi Lavazza
Language Summary Language Original Title
Series Editor Series Title Abbreviated Series Title
Series Volume Series Issue Edition
ISSN 1942-2628 ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ melatti @ Serial 108
Permanent link to this record
 
 
Author Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico
Title (down) Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems Type Conference Article
Year 2010 Publication Computer Aided Verification Abbreviated Journal
Volume Issue Pages 180-195
Keywords
Abstract We present an algorithm that given a Discrete Time Linear Hybrid System returns a correct-by-construction software implementation K for a (near time optimal) robust quantized feedback controller for along with the set of states on which K is guaranteed to work correctly (controllable region). Furthermore, K has a Worst Case Execution Time linear in the number of bits of the quantization schema.
Address
Corporate Author Thesis
Publisher Springer Berlin / Heidelberg Place of Publication Editor Touili, T.; Cook, B.; Jackson, P.
Language Summary Language Original Title
Series Editor Series Title Lecture Notes in Computer Science Abbreviated Series Title
Series Volume 6174 Series Issue Edition
ISSN ISBN Medium
Area Expedition Conference
Notes Approved yes
Call Number Sapienza @ mari @ cav2010 Serial 16
Permanent link to this record
 
 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa
Title (down) Synchronized regular expressions Type Journal Article
Year 2003 Publication Acta Inf. Abbreviated Journal
Volume 39 Issue 1 Pages 31-70
Keywords
Abstract Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday also increases the need of more powerful tools to interact with texts. Indeed, much work has been done to provide simple and versatile tools that can be useful for the most common text manipulation tasks. Regular Expressions (RE), introduced by Kleene, are well known in the formal language theory. RE have been extended in various ways, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [15] UNIX command, or the Perl [20] language pattern matching constructs) we find backreferences, i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. In this paper we introduce the Synchronized Regular Expressions (SRE) as an extension of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are dealing with formalisms that should have a practical utility and be used in real applications, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user-friendly syntax for SRE to be used in implementations of SRE-powered search algorithms.
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 @ actainf03 Serial 39
Permanent link to this record
 
 
Author Della Penna, Giuseppe; Intrigila, Benedetto; Tronci, Enrico; Venturini Zilli, Marisa
Title (down) Synchronized Regular Expressions Type Journal Article
Year 2002 Publication Electr. Notes Theor. Comput. Sci. Abbreviated Journal
Volume 62 Issue Pages 195-210
Keywords
Abstract Text manipulation is one of the most common tasks for everyone using a computer. The increasing number of textual information in electronic format that every computer user collects everyday stresses the need of more powerful tools to interact with texts. Indeed, much work has been done to provide nonprogramming tools that can be useful for the most common text manipulation issues. Regular Expressions (RE), introduced by Kleene, are well–known in the formal language theory. RE received several extensions, depending on the application of interest. In almost all the implementations of RE search algorithms (e.g. the egrep [A] UNIX command, or the Perl [17] language pattern matching constructs) we find backreferences (as defind in [1]), i.e. expressions that make reference to the string matched by a previous subexpression. Generally speaking, it seems that all the kinds of synchronizations between subexpressions in a RE can be very useful when interacting with texts. Therefore, we introduce the Synchronized Regular Expressions (SRE) as a derivation of the Regular Expressions. We use SRE to present a formal study of the already known backreferences extension, and of a new extension proposed by us, which we call the synchronized exponents. Moreover, since we are talking about formalisms that should have a practical utility and can be used in the real world, we have the problem of how to present SRE to the final users. Therefore, in this paper we also propose a user–friendly syntax for SRE to be used in implementations of SRE–powered search algorithms.
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 TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types Approved yes
Call Number Sapienza @ mari @ entcs02 Serial 46
Permanent link to this record
 
 
Author Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Tronci, Enrico
Title (down) SyLVaaS: System Level Formal Verification as a Service Type Conference Article
Year 2015 Publication Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP 2015), special session on Formal Approaches to Parallel and Distributed Systems (4PAD) 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 no
Call Number MCLab @ davi @ Serial 123
Permanent link to this record
 
 
Author Mancini, T.; Mari, F.; Massini, A.; Melatti, I.; Tronci, E.
Title (down) 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