@INPROCEEDINGS{DASIA11,
  author = {Federico Cavaliere and Federico Mari and Igor Melatti and Giovanni Minei and Ivano Salvo and Enrico Tronci and Giovanni Verzino and Yuri Yushtein},
  title = {Model Checking Satellite Operational Procedures},
  booktitle = {In: DAta Systems In Aerospace (DASIA), Org. EuroSpace,
                  Canadian Space Agency, CNES, ESA,
                  EUMETSAT. San Anton, Malta, EuroSpace.},
  month = {May},
  year = {2011}
}

@article{journals/corr/abs-1107-5638,
  author    = {Federico Mari and
               Igor Melatti and
               Ivano Salvo and
               Enrico Tronci},
  title     = {Quantized Feedback Control Software Synthesis from System
               Level Formal Specifications},
  journal   = {CoRR},
  volume    = {abs/1107.5638},
  year      = {2011},
  ee        = {http://arxiv.org/abs/1107.5638}
}

@article{journals/corr/abs-1106-0468,
  author    = {Federico Mari and
               Igor Melatti and
               Ivano Salvo and
               Enrico Tronci},
  title     = {From Boolean Functional Equations to Control Software},
  journal   = {CoRR},
  volume    = {abs/1106.0468},
  year      = {2011},
  ee        = {http://arxiv.org/abs/1106.0468}
}

@article{journals/corr/abs-1105-5640,
  author    = {Federico Mari and
               Igor Melatti and
               Ivano Salvo and
               Enrico Tronci},
  title     = {Quantized Feedback Control Software Synthesis from System
               Level Formal Specifications for Buck DC/DC Converters},
  journal   = {CoRR},
  volume    = {abs/1105.5640},
  year      = {2011},
  ee        = {http://arxiv.org/abs/1105.5640}
}

@INPROCEEDINGS{cav2010,
  author = {Mari,, Federico and Melatti,, Igor and Salvo,, Ivano and Tronci,, Enrico},
  title = {Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems},
  booktitle = {Computer Aided Verification},
  series = {Lecture Notes in Computer Science},
  editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul},
  publisher = {Springer Berlin / Heidelberg},
  pages = {180-195},
  volume = {6174},
  doi = {10.1007/978-3-642-14295-6_20},
  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.},
  year = {2010}
}

@INPROCEEDINGS{crisis09,
  author={Bobbio, A. and Ciancamerla, E. and Di Blasi, S. and Iacomini, A. and Mari, F. and Melatti, I. and Minichino, M. and Scarlatti, A. and Tronci, E. and Terruggia, R. and Zendri, E.}, 
  booktitle={Risks and Security of Internet and Systems (CRiSIS), 2009 Fourth International Conference on}, title={Risk analysis via heterogeneous models of SCADA interconnecting Power Grids and Telco networks}, 
  year={2009}, 
  month={oct.}, 
  volume={}, 
  number={}, 
  pages={90 -97}, 
  abstract={The automation of power grids by means of supervisory control and data acquisition (SCADA) systems has led to an improvement of power grid operations and functionalities but also to pervasive cyber interdependencies between power grids and telecommunication networks. Many power grid services are increasingly depending upon the adequate functionality of SCADA system which in turn strictly depends on the adequate functionality of its communication infrastructure. We propose to tackle the SCADA risk analysis by means of different and heterogeneous modeling techniques and software tools. We demonstrate the applicability of our approach through a case study on an actual SCADA system for an electrical power distribution grid. The modeling techniques we discuss aim at providing a probabilistic dependability analysis, followed by a worst case analysis in presence of malicious attacks and a real-time performance evaluation.}, 
  doi={10.1109/CRISIS.2009.5411974}, 
  ISSN={2151-4763}
}

@INPROCEEDINGS{sss09,
  author = {Mari,, Federico and Melatti,, Igor and Salvo,, Ivano and Tronci,, Enrico and Alvisi,, Lorenzo and Clement,, Allen and Li,, Harry C.},
  title = {Model Checking Coalition Nash Equilibria in MAD Distributed Systems},
  editor = {Rachid Guerraoui and Franck Petit},
  booktitle = {Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings},
  year = {2009},
  pages = {531-546},
  doi = {10.1007/978-3-642-05118-0_37},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5873},
  abstract = {We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems with possibly colluding agents (coalitions) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a proposed protocol for each agent and the maximum sizes f for Byzantine agents and q for agents collusions, our model checkers return Pass if the proposed protocol is an $\epsilon$-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than $\epsilon$ in deviating from the proposed protocol when up to f Byzantine agents are present, Fail otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one explicitly checks equilibria for each coalition, while the second represents symbolically all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than $5 \times 10^{21}$ entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.}
}

@INPROCEEDINGS{DASIA09,
  author = {Mazzini,, S. and Puri,, S. and Mari,, Federico and Melatti,, Igor and Tronci,, Enrico},
  title = {Formal Verification at System Level},
  booktitle = {In: DAta Systems In Aerospace (DASIA), Org. EuroSpace,
                  Canadian Space Agency, CNES, ESA,
                  EUMETSAT. Instanbul, Turkey, EuroSpace.},
  month = {May},
  day = {26--29},
  year = {2009}
}

@INPROCEEDINGS{MarTro07,
  author = {Mari,, Federico and Tronci,, Enrico},
  title = {{C}{E}{G}{A}{R} {B}ased {B}ounded {M}odel {C}hecking of {D}iscrete {T}ime {H}ybrid {S}ystems},
  booktitle = {Hybrid Systems: Computation and Control (HSCC 2007)},
  editor = {Alberto Bemporad and Antonio Bicchi and Giorgio C. Buttazzo},
  keywords = {Model Checking, Abstraction, CEGAR, SAT, Hybrid Systems, DTHS},
  pages = {399-412},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4416},
  month = {April},
  year = {2007},
  doi = {10.1007/978-3-540-71493-4_32},
  abstract = {Many hybrid systems can be conveniently modeled as Piecewise Affine Discrete Time Hybrid Systems PA-DTHS. As well known Bounded Model Checking (BMC) for such systems comes down to solve a Mixed Integer Linear Programming (MILP) feasibility problem.
  We present a SAT based BMC algorithm for automatic verification of PA-DTHSs. Using Counterexample Guided Abstraction Refinement (CEGAR) our algorithm gradually transforms a PA-DTHS verification problem into larger and larger SAT problems.
  Our experimental results show that our approach can handle PA-DTHSs that are more then 50 times larger than those that can be handled using a MILP solver.}
}

@INPROCEEDINGS{MarMelSalTroAlvCle08,
  author = {Mari,, Federico and Melatti,, Igor and Salvo,, Ivano and Tronci,, Enrico and Alvisi,, Lorenzo and Clement,, Allen and Li,, Harry},
  title = {{M}odel {C}hecking {N}ash {E}quilibria in {M}{A}{D} {D}istributed {S}ystems},
  booktitle = {FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design},
  editor = {Alessandro Cimatti and Robert Jones},
  keywords = {Model Checking, MAD Distributed System, Nash Equilibrium},
  month = {November},
  year = 2008,
  isbn = {978-1-4244-2735-2},
  pages = {1--8},
  location = {Portland, Oregon},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
  doi = {10.1109/FMCAD.2008.ECP.16},
  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.}
}

@INPROCEEDINGS{ChiLatMar08,
  author = {Chierichetti,, Flavio and Lattanzi,, Silvio and Mari,, Federico and Panconesi,, Alessandro},
  title = {{O}n {P}lacing {S}kips {O}ptimally in {E}xpectation},
  booktitle = {Web Search and Web Data Mining (WSDM 2008)},
  editor = {Marc Najork and Andrei Z. Broder and Soumen Chakrabarti},
  keywords = {Information Retrieval},
  pages = {15-24},
  publisher = {ACM},
  month = {February},
  year = 2008,
  doi = {10.1145/1341531.1341537},
  abstract = {We study the problem of optimal skip placement in an inverted list.  Assuming the query distribution to be known in advance, we formally prove that an optimal skip placement can be computed quite efficiently. Our best algorithm runs in time O(n log n), n being the length of the list. 
    The placement is optimal in the sense that it minimizes the expected time to process a query. Our theoretical results are matched by experiments with a real corpus, showing that substantial savings can be obtained with respect to the tra- ditional skip placement strategy, that of placing consecutive skips, each spanning sqrt(n) many locations.}
}