You are here

Marco Roveri

Senior Researcher
  • SKYPE: roveri.marco
  • Phone: 0461314326
  • FBK Povo
Short bio

Marco Roveri is a senior researcher in the Embedded Systems Unit of the Fondazione Bruno Kessler, Trento, Italy. He received a Ph.D. degree in Computer Science from the University of Milano, Italy in 2002. He joined the Automated Reasoning Division of the Istituto Trentino di Cultura, Trento, Italy, in 1998, first as a consultant, and in 2002 as a full time researcher. In 2008 he was appointed as a senior researcher in the Embedded Systems Unit of the Fondazione Bruno Kessler, Trento, Italy. His research interests include automated formal verification of hardware and software systems, formal requirements validation of embedded systems, and automated model based planning.

Interest

Research interests
Symbolic Model Checking Automated Planning Formal Requirements Engineering
Publications

2016

  1. Cimatti, Alessandro; Hunsberger, Luke; Micheli, Andrea; Posenato, Roberto; Roveri, Marco,
    in «ACTA INFORMATICA»,
    2016
    , pp. 1 -
    42
  2. Irfan, Ahmed; Cimatti, Alessandro; Griggio, Alberto; Roveri, Marco; Sebastiani, Roberto,
    Design, Automation & Test in Europe Conference & Exhibition (DATE), 2016,
    2016
    , pp. 1156-
    1159
    , (2016 Design, Automation & Test in Europe Conference & Exhibition (DATE),
    Dresden, Germany,
    14-18 March 2016)
  3. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    Proceedings of the Thirtieth AAAI}Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA,
    2016
    , pp. 3116-
    3122
    , (Thirtieth AAAI}Conference on Artificial Intelligence,
    Phoenix, Arizona, USA,
    February 12-17, 2016)

2015

  1. Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta,
    Safety Assessment of AltaRica Models via Symbolic Model Checking,
    in «SCIENCE OF COMPUTER PROGRAMMING»,
    vol. 98,
    2015
    , pp. 464 -
    483
  2. Alessandro Cimatti;Andrea Micheli;Marco Roveri,
    An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 224,
    2015
    , pp. 1 -
    27
  3. Griggio, Alberto; Roveri, Marco,
    in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
    2015
    , pp. 1 -
    1
  4. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano,
    in «INFORMATION AND COMPUTATION»,
    vol. 245,
    2015
    , pp. 54 -
    71
  5. Cimatti A.; Micheli A.; Roveri M,
    Strong Temporal Planning with Uncontrollable Durations: a State-Space Approach,
    Proceedings of the 29th AAAI Conference on Artificial Intelligence,
    Palo Alto, California,
    AAAI Press,
    2015
    , (AAAI 2015,
    Austin, Texas, USA,
    25/01/2015 - 30/01/2015)
  6. Bliudze, Simon; Cimatti, Alessandro; Jaber, Mohamad; Mover, Sergio; Roveri, Marco; Saab, Wajeb; Wang, Qiang,
    Proceedings of ATVA,
    Springer,
    vol.9364,
    2015
    , pp. 326-
    343
    , (Automated Technology for Verification and Analysis 13th International Symposium, ATVA 2015,
    Shanghai, China,
    October 12-15, 2015)

2014

  1. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    Solving strong controllability of temporal problems with uncertainty using SMT,
    in «CONSTRAINTS»,
    2014
  2. Bozzano M.; Cimatti A.; Katoen J.-P.; Katsaros P.; Mokos K.; Nguyen V.Y.; Noll T.; Postma B.; Roveri M.,
    Spacecraft Early Design Validation using Formal Methods,
    in «RELIABILITY ENGINEERING & SYSTEM SAFETY»,
    vol. 132,
    2014
    , pp. 20 -
    35
  3. Robin Steel;Alexander Hoffmann;Marc Niezette;Alessandro Cimatti;Marco Roveri;Konstantinos Kapellos;Alessandro Donati;Nicola Policella,
    13th International Conference on Space Operations 2014,
    2014
  4. R. Cavada;A. Cimatti;M. Dorigatti;A. Griggio;A. Mariotti;A. Micheli;S. Mover;M. Roveri;S. Tonetta,
    The nuXmv Symbolic Model Checker,
    CAV,
    2014
    , pp. 334-
    342
    , (Computer Aided Verification,
    Vienna,
    2014)
  5. Cimatti A.; Hunsberger L.; Micheli A.; Roveri M.,
    Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence,
    Palo Alto, California, USA,
    AAAI Press,
    2014
    , pp. 2242-
    2249
    , (Twenty-Eighth AAAI Conference on Artificial Intelligence,
    Quebec City, Quebec, Canada,
    27/07/2014 - 31/07/2014)
  6. Cimatti A.; Hunsberger L.; Micheli A.; Posenato R; Roveri M.,
    Sound and Complete Algorithms for Checking the Dynamic Controllability of Temporal Networks with Uncertainty, Disjunction and Observation,
    Proceedings of the 21st International Symposium on Temporal Representation and Reasoning,
    IEEE,
    2014
    , pp. 27-
    36
    , (21st International Symposium on Temporal Representation and Reasoning,
    Verona, Italia,
    08/09/2014 - 10/09/2014)

2013

  1. Alessandro Cimatti;Iman Narasamdya;Marco Roveri,
    Software Model Checking SystemC,
    in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
    vol. 32,
    2013
    , pp. 774 -
    787
  2. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    AAAI,
    David Leake,
    2013
    , pp. 195-
    201
    , (Twenty-Seventh AAAI Conference on Artificial Intelligence,
    Bellevue, Washington, USA,
    14/07/2013 - 18/07/2013)

2012

  1. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Validation of Requirements for Hybrid Systems: a Formal Approach,
    in «ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY»,
    vol. 21,
    n. 4,
    2012
    , pp. 22:1 -
    22:34
  2. Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    Software Model Checking with Explicit Scheduler and Symbolic Threads,
    in «LOGICAL METHODS IN COMPUTER SCIENCE»,
    vol. 8,
    2012
    , pp. 1 -
    42
  3. María Alpuente; Christophe Joubert; Stefan Kowalewski; Marco Roveri,
    Preface to the special issue on Formal Methods for Industrial Critical Systems (FMICS 2009 + FMICS 2010),
    Elsevier,
    2012
    , pp. 1 -
    3
  4. Alessandro Cimatti; Raffaele Corvino; Armando Lazzaro; Iman Narasamdya; Tiziana Rizzo; Marco Roveri; Angela Sanseviero; Andrei Tchaltsev,
    Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System,
    CAV,
    Springer,
    vol.7358,
    2012
    , pp. 378-
    393
    , (Computer Aided Verification - 24th International Conference, CAV 2012,
    Berkeley, CA, USA,
    da 07/07/2012 a 07/13/2012)
  5. Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    Verification of Parametric System Designs,
    2012
    , (Formal Methods in Computer Aided Design (FMCAD) 2012,
    Cambridge, UK,
    da 10/22/2012 a 10/25/2012)
  6. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    Solving Temporal Problems using SMT: Weak Controllability,
    Proceedings of the Twenty-Sixth AAAI Conference on Artificial Intelligence,
    AAAI Press,
    2012
    , (AAAI 2012,
    Toronto, Canada,
    da 07/22/2012 a 07/26/2012)
  7. Alessandro Cimatti; Andrea Micheli; Marco Roveri,
    Solving Temporal Problems using SMT: Strong Controllability,
    Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming,
    2012
    , (CP 2012,
    Quebec City, Canada,
    da 10/08/2012 a 10/12/2012)
  8. Robin Steel; Alexander Hoffman; Mark Niézette; Alessandro Cimatti; Marco Roveri; Konstantinos Kapellos; Alessandro Donati; Nicola Policella,
    Innovative Rover Operations Concepts - Autonomous Planner (IRONCAP) - Supporting Rover Operations Planning on Ground,
    SpaceOps 2012 Conference,
    2012
    , (12th International Conference on Space Operations, SpaceOps, At Stockholm, Sweden,
  9. Jörg Brauer; Marco Roveri; Hendrik Tews (eds.),
    6th International Workshop on Systems Software Verification, SSV 2011,
    Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
    2012

2011

  1. Alessandro Cimatti; Angelo Susi; Stefano Tonetta; Marco Roveri,
    in «SOFTWARE AND SYSTEMS MODELING»,
    vol. 10,
    n. 2,
    2011
    , pp. 147 -
    160
  2. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Safety, Dependability and Performance Analysis of Extended AADL Models,
    in «COMPUTER JOURNAL»,
    vol. 54,
    n. 5,
    2011
    , pp. 754 -
    775
  3. Alessandro Cimatti; Sergio Mover; Marco Roveri; Stefano Tonetta,
    From Sequential Extended Regular Expressions to NFA with Symbolic Labels,
    Proceedings of 15th Int. Conference on Implementation and Application of Automata,
    vol.6482,
    2011
    , pp. 87-
    94
    , (CIAA 2010,
    Winnipeg, Canada,
    12-15/08/2010)
  4. Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    Boosting Lazy Abstraction for SystemC with Partial Order Reduction,
    Proceedings of 17th Int. Conference on Tools and Algorithms for the Construction and Analysis of Systems,
    vol.To appear,
    2011
    , (TACAS 2011,
    Saarbrücken, Germany,
    26/03/2011-03/04/2011)
  5. Alessandro Cimatti; Alberto Griggio; Andrea Micheli; Iman Narasamdya; Marco Roveri,
    2011
    , (Accepted at CAV 2011 - 23rd International Conference onComputer Aided Verification,
    Cliff Lodge, Snowbird, Utah,
    14-20/07/2011)
  6. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,
    A Comprehensive Approach to On-Board Autonomy Verification and Validation,
    AAAI (Conference on Artificial Intelligence)
    Press
    ,
    2011
    , (IJCAI 2011,
    Barcelona, Catalonia (Spain),
    16-22/07/2011)
  7. Rosella Gennari; Anna Roubickova; Marco Roveri,
    vol.To appear,
    2011
    , (3rd ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems - VVPS 2011,
    Freiburg, Germany,
    13/06/2011)
  8. Daniele Campana; Alessandro Cimatti; Iman Narasamdya; Marco Roveri,
    2011
    , (18th Int. Workshop on Model Checking of Software - SPIN,
    Cliff Lodge, Snowbird, Utah,
    14–15/07/2011)
  9. M. Bozzano; A. Cimatti; O. Lisagor; C. Mattarei; S. Mover; M. Roveri; S. Tonetta,
    Model Checking and Safety Assessment of Altarica models,
    in «ELECTRONIC COMMUNICATIONS OF THE EASST»
    Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011),
    Berlin,
    EASST,
    vol.46,
    2011
    , (AVOCS 2011 - 11th International Workshop on Automated Verification of Critical Systems,
    Newcastle, UK,
    da 09/12/2011 a 09/14/2011)
  10. Roberto Cavada; Alessandro Cimatti; Andrea Micheli; Marco Roveri; Angelo Susi; Stefano Tonetta,
    OthelloPlay: a plug-in based tool for requirement formalization and validation,
    Proceedings of the 1st Workshop on Developing Tools as Plug-ins,
    2011
    , pp. 59-
    59
    , (TOPI 2011,
    Honolulu, Hawaii, USA,
    da 05/28/2011 a 05/28/2011)
  11. Robin Steel; Alexander Hoffman; Alessandro Cimatti; Marco Roveri; Konstantinos Kapellos; Alessandro Donati; Nicola Policella,
    Innovative Rover Operations Concepts–Autonomous Planning: Keeping a dog on the lead,
    International Workshop on Planning and Scheduling for Space, IWPSS 2011,
    2011
    , (International Workshop on Planning and Scheduling for Space, IWPSS 2011,
    Freiburg, Germany,
    Giugno 2011)

2010

  1. Alessandro Cimatti; Anders Franzen; Alberto Griggio; Kalyanasundaram Krishnamani; Marco Roveri,
    Tighter Integration of BDD and SMT for Predicate Abstraction,
    Proceedings of the Design, Automation & Test in Europe,
    2010
    , pp. 1707-
    1712
    , (DATE 2010,
    Dresden, Germany,
    08-12/03/2010)
  2. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Formalization and Validation of Safety-Critical Requirements,
    Proceedings of the Workshop on Formal Methods for Aerospace,
    vol.20,
    2010
    , pp. 68-
    75
    , (FMA'09 - 16th Int. Symposium on Formal Methods FM'09,
    Eindhoven, The Netherlands,
    03/11/2009)
  3. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer,
    A Model Checker for AADL,
    Proceedings of 22nd International Conference on Computer Aided Verification,
    Springer,
    vol.6174,
    2010
    , pp. 562-
    565
    , (CAV 2010,
    Edinburgh, UK,
    15-19/07/2010)
  4. Roderick Bloem; Alessandro Cimatti; Karin Greimel; Georg Hofferek; Robert Koenighofer; Marco Roveri; Viktor Schuppan; Richard Seeber,
    RATSY - A new Requirements Analysis Tool with Synthesis,
    Proceedings of 22nd Int. Conference on Computer Aided Verification,
    Springer,
    vol.6174,
    2010
    , pp. 425-
    429
    , (CAV 2010,
    Edinburgh, UK,
    15-19/07/2010)
  5. Giuseppe Di Guglielmo; Franco Fummi; Graziano Pravadelli; Marco Roveri; Stefano Soffia,
    Semi-Formal Functional Verification by EFSM traversing via NuSMV,
    Proceedings of the High Level Design Validation and Test Workshop,
    2010
    , pp. 58-
    65
    , (HLDVT 2010,
    Anaheim, CA,
    10-12/06/2010)
  6. Angelo Chiappini; Alessandro Cimatti; Luca Macchi; Oscar Rebollo; Marco Roveri; Angelo Susi; Stefano Tonetta; Berardino Vittorini,
    Formalization and validation of a subset of the European Train Control System,
    Proceedings of 32nd Int. Conference on Software Engineering,
    New York,
    vol.2,
    2010
    , pp. 109-
    118
    , (ICSE (2),
    Cape Town, South Africa,
    01-08/05/2010)
  7. Alessandro Cimatti; Andrea Micheli; Iman Narasamdya; Marco Roveri,
    Verifying SystemC: a Software Model Checking Approach,
    Proceedings of the 10th Int. Conference on Formal Methods in Computer-Aided Design,
    2010
    , pp. 51-
    60
    , (FMCAD 2010,
    Lugano, Switzerland,
    October, 20-23, 2010)
  8. Stefan Kowalewski; Marco Roveri (eds.),
    Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20-21, 2010. Proceedings,
    Verlag Berlin Heidelberg,
    Springer,
    2010
  9. Marco Roveri; Alessandro Cimatti; Iman Narasamdya; Andrea Micheli; Daniele Campana; Alberto Griggio; Andrei Tchaltsev,
    2010,
  10. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri; Ralf Wimmer; Roberto Cavada,
    2010,

2009

  1. Alessandro Cimatti; Marco Roveri; Stefano Tonetta,
    Requirements Validation for Hybrid Systems,
    Proceedings 21st Int. Conference on Computer Aided Verification,
    Springer,
    vol.5643,
    2009
    , pp. 188-
    203
    , (CAV 2009,
    Grenoble, France,
    26/06/2009-02/07/2009)
  2. Alessandro Cimatti; Jori Juhani Dubrovin; Tommi Antero Junttila; Marco Roveri,
    Proceedings of the Formal Methods in Computer Aided Design,
    2009
    , pp. 9-
    16
    , (FMCAD 2009,
    AUSTIN, TX, USA,
    15/11/2009 - 18/11/2009)
  3. Roberto Cavada; Alessandro Cimatti; Alessandro Mariotti; Cristian Mattarei; Andrea Micheli; Sergio Mover; Marco Pensallorto; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Supporting Requirements Validation: The EuRailCheck Tool,
    Proceedings of 24th Int. Conference Automated Software Engineering,
    2009
    , pp. 665-
    667
    , (ASE 2009,
    Auckland, New Zealand,
    16/11/2009 - 20/11/2009)
  4. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Andrei Tchaltsev,
    Workshop on Verification and Validation of Planning and Scheduling Systems,
    2009
    , pp. 1-
    10
    , (VV&PS 2009 - ICAPS,
    Thessaloniki, Greece,
    20/09/2009)
  5. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,
    Proceedings of 28th Int. International Conference on Computer Safety, Reliability and Security,
    Springer,
    vol.5775,
    2009
    , pp. 173-
    186
    , (SAFECOMP 2009,
    Hamburg, Germany,
    15-18/09/2009)
  6. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll,
    Verification and performance evaluation of AADL models,
    Proceedings of the the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering,
    New York,
    ACM,
    2009
    , pp. 285-
    286
    , (ESEC/FSE 2009,
    Amsterdam, The Netherlands,
    24-28/08/2009)
  7. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Proceedings 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems,
    CEUR-WS.org,
    vol.507,
    2009
    , pp. 87-
    91
    , (ACESMB09,
    Denver, Colorado, USA,
    06/10/2009)
  8. Marco Bozzano; Alessandro Cimatti; Marco Roveri; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll,
    Codesign of Dependable Systems: A Component-Based Modeling Language,
    Proceedings of the 7th IEEE/ACM Int. Conference on Formal Methods and Models for Codesign,
    Piscataway, NJ,
    2009
    , pp. 121-
    130
    , (MEMOCODE'09,
    Cambridge, Massachusetts, USA,
    13-15/07/2009)
  9. Marco Roveri; Alessandro Cimatti; Viktor Schuppan; Andrei Tchaltsev; Roberto Cavada,
    2009,
  10. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    Codesign of Dependable Systems: A Component-Based Language,
    2009
  11. Marco Bozzano; Alessandro Cimatti; Joost-Pieter Katoen; Viet Yen Nguyen; Thomas Noll; Marco Roveri,
    The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems,
    2009

2008

  1. Alessandro Cimatti; Marco Roveri; Stefano Tonetta,
    Symbolic Compilation of PSL,
    in «IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS»,
    vol. 27,
    n. 10,
    2008
    , pp. 1737 -
    1750
  2. Alessandro Cimatti; Marco Roveri; Viktor Schuppan; Andrei Tchaltsev,
    Diagnostic Information for Realizability,
    Proceedings of 9th Int. Conference Verification, Model Checking, and Abstract Interpretation,
    Springer,
    vol.4905,
    2008
    , pp. 52-
    67
    , (VMCAI 2008,
    San Francisco, USA,
    07/01/2008-09/01/2008)
  3. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    Object Models with Temporal Constraints,
    Proceedings 6th Int. Conference on Software Engineering and Formal Methods,
    2008
    , pp. 249-
    258
    , (SEFM 2008,
    Cape Town,
    10/11/2008 - 14/11/2008)
  4. Alessandro Cimatti; Marco Roveri; Angelo Susi; Stefano Tonetta,
    From Informal Requirements to Property-Driven Formal Validation,
    Proceedings of 13th Int. Workshop on Formal Methods for Industrial Critical Systems,
    Springer Verlag,
    vol.5596,
    2008
    , pp. 166-
    181
    , (FMICS 2008,
    L’Aquila, Italy,
    15/09/2008 - 16/09/2008)
  5. Marco Bozzano; Alessandro Cimatti; Andrea Guiotto; Andrea Martelli; Marco Roveri; Andrei Tchaltsev; Yuri Yushtein,
    On-Board Autonomy via Symbolic Model Based Reasoning,
    Proceedings of 10th Workshop on Advanced Space Technologies for Robotics and Automation,
    Noordwijk,
    2008
    , (ASTRA 2008,
    Noordwijk, The Netherlands,
    11/11/2008 - 13/11/2008)
  6. Alessandro Cimatti; Andrea Guiotto; Marco Roveri,
    On Board Model Checking for Space Applications,
    Proceedings of ESA Workshop on Avionics Data, Control and Software Systems,
    Noordwijk,
    2008
    , pp. 10-
    11
    , (ADCSS,
    Noordwijk, The Netherlands,
    29/10/2008 - 31/10/2008)

2007

  1. Roderick Bloem; Alessandro Cimatti; Ingo Pill; Marco Roveri,
    Symbolic Implementation of Alternating Automata,
    in «INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE»,
    vol. 18,
    n. 4,
    2007
    , pp. 727 -
    743
  2. Alessandro Cimatti; Marco Roveri; Viktor Schuppan; Stefano Tonetta,
    Boolean Abstraction for Temporal Logic Satisfiability,
    Proceedings of 19th Int. Conference Computer Aided Verification,
    Springer,
    vol.4590,
    2007
    , pp. 532-
    546
    , (CAV,
    Berlin, Germany,
    03/07/2007-07/07/2007)
  3. Roberto Cavada; Alessandro Cimatti; Anders Franzen; Kalyanasundaram Krishnamani; Marco Roveri; R. K. Shyamasundar,
    Computing Predicate Abstractions by Integrating BDDs and SMT Solvers,
    Proceedings of the Formal Methods in Computer Aided Design,
    Washington, DC,
    2007
    , pp. 69-
    76
    , (FMCAD '07,
    Austin, Texas,
    11/11/2007-14/11/2007)
  4. Alessandro Cimatti; Marco Roveri; Stefano Tonetta,
    Syntactic Optimizations for PSL Verification,
    Proceedings of 13th Int. Conference Tools and Algorithms for the Construction and Analysis of Systems,
    Springer,
    vol.4424,
    2007
    , pp. 505-
    518
    , (TACAS,
    Braga, Portugal,
    24/03/2007-01/04/2007)
  5. Roderick Bloem; Roberto Cavada; Ingo Pill; Marco Roveri; Andrei Tchaltsev,
    Rat: A tool for the formal analysis of requirements,
    Proceedings of 19th Int. Conference Computer Aided Verification,
    Springer,
    vol.4590,
    2007
    , pp. 263-
    267
    , (CAV 2007,
    Berlin, Germany,
    03/07/2007-07/07/2007)
  6. Roderick Bloem;Marco Roveri;Fabio Somenzi (eds.),
    Preface,
    2007

2006

  1. P. Bertoli; A. Cimatti; M. Roveri; P. Traverso,
    Strong Planning under Partial Observability,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 170,
    n. 4-5,
    2006
    , pp. 337 -
    384
  2. R. Bloem; A. Cimatti; I. Pill; M. Roveri; S. Semprini,
    Symbolic Implementation of Alternating Automata,
    Proceedings of 11th Int. Conference Implementation and Application of Automata,
    Springer,
    vol.4094,
    2006
    , pp. 208-
    218
    , (CIAA,
    Taipei, Taiwan,
    21/08/2006-23/08/2006)
  3. I. Pill; S. Semprini; R. Cavada; M. Roveri; R. Bloem; A. Cimatti,
    Formal analysis of hardware requirements,
    Proceedings of 43rd annual Design Automation Conference,
    New York, NY,
    2006
    , pp. 821-
    826
    , (DAC,
    San Francisco, USA,
    24/07/2006-28/07/2006)
  4. Roderick Bloem; Alessandro Cimatti; Ingo Pill; Marco Roveri; Simone Semprini; Andrei Tchaltsev,
    RAT: A tool for formal analysis of requirements,
    Demo Session of the 17th European Conference on Artificial Intelligence,
    2006
    , (ECAI,
    Riva del Garda, Italy,
    28/08/2006-01/09/2006)
  5. Alessandro Cimatti; Marco Roveri; Simone Semprini; Stefano Tonetta,
    From PSL to NBA: a Modular Symbolic Encoding,
    Proceedings of 6th Int. Conference on Formal Methods in Computer Aided Design,
    2006
    , pp. 125-
    133
    , (FMCAD,
    San Jose, CA, USA,
    12/11/2006-16/11/2006)

2005

  1. Marco Roveri; Alessandro Cimatti; Andrei Tchaltsev; Roberto Cavada; Simone Semprini; Roderick Bloem; Ingo Pill,
    2005,

2004

  1. A. Fuxman; L. Liu; J. Mylopoulos; M. Pistore; M. Roveri; P. Traverso,
    in «REQUIREMENTS ENGINEERING»,
    vol. 9,
    n. 2,
    2004
    , pp. 132 -
    150
  2. Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli,
    Conformant Planning via Symbolic Model Checking and Heuristic Search,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 159,
    n. 1-2,
    2004
    , pp. 127 -
    206
  3. P. Traverso; M. Pistore; M. Roveri; A. Marconi; R. Kazhamiakin; P. Lucchese; P. Busetta; P. Bertoli,
    Towards a Framework for Supporting Negotiation between Global and Local Business Requirements,
    Proceedings of 2nd Int. Conference on Service-Oriented Computing,
    2004
    , pp. 56-
    65
    , (ICSOC,
    New York City, NY, USA,
    15/11/2004-18/11/2004)
  4. R. Kazhamiakin; M. Pistore; M. Roveri,
    A Framework for Integrating Business Processes and Business Requirements,
    Proceedings of 8th Int. Conference Enterprise Distributed Object Computing,
    Washington, DC,
    2004
    , pp. 9-
    20
    , (EDOC,
    Monterey, California, USA,
    20/09/2004-24/09/2004)
  5. R. Kazhamiakin; M. Pistore; M. Roveri,
    Formal Verification of Requirements using Spin: A Case Study on Web Services,
    Proceedings od 2nd Int. Conference on Software Engineering and Formal Methods,
    2004
    , pp. 406-
    415
    , (SEFM,
    Beijing, China,
    28/09/2004-30/09/2004)
  6. A. Cimatti; M. Roveri; D. Sheridan,
    Bounded Verification of Past LTL,
    Proceedings of 5th Int. Conference on Formal Methods in Computer-Aided Design,
    Springer,
    vol.3312,
    2004
    , pp. 245-
    259
    , (FMCAD,
    Austin, Texas, USA,
    14/11/2004-17/11/2004)
  7. Marco Pistore; Marco Roveri; Paolo Busetta,
    Requirements-Driven Verification of Web Services,
    Proceedings of 1st Int. Workshop on Web Services and Formal Methods,
    2004
    , (WS-FM,
    Pisa, Italu,
    23-24/02/2004)
  8. P. Traverso; M. Pistore; M. Roveri; A. Marconi; R. Kazhamiakin; P. Lucchese; P. Busetta; P. Bertoli,
    Supporting the Negotiation between Global and Local Business Requirements in Service oriented Development,
    The development of service oriented applications very often needs to address the problem of satisfying two conflicting kinds of business needs: global business requirements, i.e., the regulations that dictate the rules of engagement between different organizations, and local business requirements, i.e., the rules local to each involved partner which derive from its internal business needs. In this paper, we propose a development process where both global and local service requirements, as well as their behaviors, are incrementally agreed among partners and built through negotiation steps. The development process is supported by the explicit definition of both global and local requirements at different levels of abstraction. We express requirements in a language with a clear semantics, and which allows for explicit links to executable business processes, e.g., written in BPEL4WS. This development process opens up the possibility to adopt a variety of supporting techniques. In particular, automated verification is used to detect design or implementation problems. Automated synthesis of executable business processes allows for a speed up in the development process and reduces development effort. Finally, execution monitoring is able to detect run-time problems with respect to specified requirements,
    2004

2003

  1. Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking,
    in «ARTIFICIAL INTELLIGENCE»,
    vol. 147,
    n. 1-2,
    2003
  2. Anna Perini; Marco Pistore; Marco Roveri; Angelo Susi,
    Agent-oriented modeling by interleaving formal and informal specification,
    Agent-Oriented Software Engineering IV,
    Springer,
    2003
    , pp. 36 -
    52
  3. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    ICAPS`03: system demo session,
    2003
    , (ICAPS`03: system demo session,
    2003)
  4. A. Fuxman; L. Liu; Marco Pistore; Marco Roveri; John Mylopoulos,
    Specifying and Analyzing Early Requirements: Some Experimental Results,
    11th IEEE International Conference on Requirements Engineering (RE 2003),
    IEEE Computer Society,
    2003
    , pp. 105-
    114
    , (11th IEEE International Conference on Requirements Engineering (RE 2003),
    Monterey Bay, USA,
    08/09/2003 - 12/09/2003)
  5. A. Fuxman; L. Liu; Marco Pistore; Marco Roveri; John Mylopoulos,
    Specifying and Analyzing Early Requirements: Some Experimental Results,
    Formal Tropos is a specification language for early requirements. It is based on concepts from an agent-oriented early requirement model framework (i*) and extends them with a rich temporal specification language. In earlier work, we demonstrated through a small case study how model checking could be used to verify early requirements written in Formal Tropos. In this paper we address issues of methodology and scalability for our earlier proposal. In particular, we propose guidelines for producing a Formal Tropos specification from an i* diagram and for deciding what model checking technique to use when a particular formal property is to be validated. We also evaluate the scope and scalability of our proposal using a tool, the T-Tool, that maps Formal Tropos specifications to a language that can be handled by NuSMV, a state-of-the-art model checker. Our experiments are based on a course management case study,
    2003
  6. Anna Perini; Marco Pistore; Marco Roveri; Angelo Susi,
    Agent-oriented modeling by interleaving formal and informal specification,
    The goal of this paper is to discuss possibilities of inter-mixing formal and informal specification in order to guide and support the conceptual modeling process in software development. We sketch a framework which rests on an agent-oriented methodology that provides a modeling language which allows for the definition of both informal and formal specification. We show how formal techniques can be used to guide and support the analyst while building and refining a conceptual model. Examples of its applications are discussed, with reference to the decision making process undertaken by the analyst when performing a set of activities relevant for requirements engineering, such as requirements elicitation and refinement, user validation of requirements specification, or management of requirements evolution. A case study taken from a technology transfer project in the agricultural domain is used to illustrate the approach,
    2003

2002

  1. Alessandro Cimatti; Marco Pistore; Marco Roveri; Roberto Sebastiani,
    Improving the encoding of LTL Model Checking into SAT,
    VMCAI-2002 Workshop on Verification Model Checking and Abstract Interpretation,
    Springer,
    vol.2294,
    2002
    , pp. 196-
    207
    , (VMCAI-2002 Workshop on Verification Model Checking and Abstract Interpretation,
    2002)
  2. Alessandro Cimatti; E. Giunchiglia; Marco Roveri; Marco Pistore; Roberto Sebastiani; A. Tacchella,
    Integrating BDD-based and SAT-based Symbolic Model Checking,
    Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002,
    Springer,
    vol.2309,
    2002
    , pp. 49-
    56
    , (Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002,
    Santa Margherita Ligure, Italy,
    2002)
  3. Alessandro Cimatti; E.M. Clarke; Enrico Giunchiglia; Fausto Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
    NuSMV 2: An OpenSource Tool for Symbolic model Checking,
    CAV 2002, Conference on Computer-Aided Verification,
    Springer,
    vol.2404,
    2002
    , pp. 359-
    364
    , (CAV 2002, Conference on Computer-Aided Verification,
    Copenhagen, Denmark,
    2002)
  4. Marco Roveri; Alessandro Cimatti; Roberto Cavada; Andrei Tchaltsev; Andrea Micheli; Alessandro Mariotti; Sergio Mover; Marco Pensallorto; Armando Tacchella; Daniel Sheridan; Gavin Keighren; Tommi Junttila; Timo Latvala,
    2002,
  5. Marco Roveri,
    Planning in Non-Deterministic Domains via Symbolic Model Checking,
    In the thesis is tackled the Artificial Intelligence (AI) problem of Automatic Planning using Symbolic Model Checking (SMC) techniques developed within the Formal Verification community for the verification of designs. The use of SMC techniques allowed for a formal definition and for an efficient handling of a large class of planning problems that classical planning systems developed within AI Planning are not able to deal with. In the thesis two restricting hypothesis of classical planning have been discarded. Planning domains are assumed to be non-deterministic and are modeled as non-deterministic finite state automata. Moreover, a planning domain can be partially observable at execution time. A formal characterization of solutions to different planning problem is provided, distinguishing among weak solutions (that may achieve the goal), strong solution (that guarantee goal achievement) and strong cyclic solutions (that capture a trial and error behavior guaranteeing goal achievement under `fair` executions); under different hypothesis of domain run-time observability (i.e., full, null and partial observability). A family of algorithms to synthesize solutions to the different planning problems characterized are provided and proved to be correct. The algorithms have been implemented in the Model Based Planner (MBP) using SMC techniques. An extensive experimental analysis is carried out to show the effectiveness of the proposed approach w.r.t. the other state of the art planners,
    2002

2001

  1. Alessandro Cimatti; Marco Roveri; Piergiorgio Bertoli,
    Searching Porwerset Automata by Combining Explicit-State and Symbolic Model Checking,
    Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings,
    Springer,
    vol.2031,
    2001
    , pp. 313-
    327
    , (Tools and Algorithms for the Construction and Analysis of Systems [TACAS 2001], Conference Proceedings,
    2001)
  2. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri,
    Heuristic Search + Symbolic Model Checking = Efficient Conformant Planning,
    17th International Joint Conference on Artificial Intelligence, IJCAI 2001,
    Morgan Kaufmann,
    2001
    , pp. 467-
    472
    , (17th International Joint Conference on Artificial Intelligence, IJCAI 2001,
    Seattle, USA,
    04/08/2001 - 10/08/2001)
  3. Alessandro Cimatti; E. Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
    NuSMV Version 2: BDD-based + SAT-based Symbolic Model Checking,
    Proceedings of the IJCAR Workshop `Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics`,
    no publisher,
    2001
    , (Proceedings of the IJCAR Workshop `Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics`,
    Siena, Italy,
    19/06/2001)
  4. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri,
    Conditional Planning under Partial Obserbability as Heuristic-Symbolic Search in Belief Space,
    Sixth European Conference on Planning [ECP-01],
    Springer,
    2001
    , pp. 379-
    384
    , (Sixth European Conference on Planning [ECP-01],
    2001)
  5. Piergiorgio Bertoli; Alessandro Cimatti; Marco Pistore; Marco Roveri; Paolo Traverso,
    IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
    2001
    , (IJCAI-2001 Workshop on Planning under Uncertainty and Incomplete Information (PRO-2),
    Seattle, Washington, USA,
    2001)
  6. Piergiorgio Bertoli; Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
    Morgan Kaufmann,
    2001
    , pp. 473-
    478
    , (Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01), Proceedings,
    Seattle, Washington, USA,
    2001)

2000

  1. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Symbolic Model Checking,
    in «THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH»,
    vol. 13,
    2000
    , pp. 305 -
    338
  2. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: a new symbolic model checker,
    in «INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER»,
    2000
    , pp. 410 -
    425
  3. Alessandro Cimatti; Marco Roveri,
    Forward Conformant Planning via Symbolic Model Checking,
    AIPS 2000 Workshop on Model-Theoretic Approaches to Planning,
    2000
    , (AIPS 2000 Workshop on Model-Theoretic Approaches to Planning,
    2000)
  4. Marco Roveri,
    Abstraction in Model Checking for Bug Hunting,
    Modeling and Verification of Parallel Processes, 4th Summer School, MOVEP 2000,
    2000
    , pp. 219-
    223
    , (Modeling and Verification of Parallel Processes, 4th Summer School, MOVEP 2000,
    Nantes, France,
    19/06/2000 - 23/06/2000)
  5. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Model Checking,
    Fifth European Conference on Planning [ECP`99],
    Springer,
    2000
    , pp. 21-
    34
    , (Fifth European Conference on Planning [ECP`99],
    Durham, UK,
    08/09/1999 - 10/09/1999)

1999

  1. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: a New Symbolic Model Verifier,
    11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
    Springer,
    1999
    , (11th International Conference on Computer Aided Verification (CAV`99), Proceedings,
    Trento, Italy,
    1999)
  2. Alessandro Cimatti; Marco Roveri,
    Conformant Planning via Model Checking,
    Fifth European Conference on Planning [ECP`99],
    Springer,
    1999
    , (Fifth European Conference on Planning [ECP`99],
    Durham, UK,
    08/09/1999 - 10/09/1999)

1998

  1. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: A Reimplementation of SMV,
    International Workshop on Software Tools for Technology Transfer (STTT-98),
    vol.NS-98-4,
    1998
    , pp. 25-
    31
    , (International Workshop on Software Tools for Technology Transfer (STTT-98),
    1998)
  2. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    1998
    , (Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    Pittsburgh, USA,
    1998)
  3. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains,
    Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    AAAI Press,
    1998
    , pp. 875-
    881
    , (Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    Madison, USA,
    1998)
  4. Alessandro Cimatti; Fausto Giunchiglia; Marco Roveri,
    Abstraction in Planning via Model Checking,
    Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998
    , pp. 37-
    41
    , (Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998)