Publications
This page contains the list of publications that uses nuXmv or describe a functionality that has been integrated in nuXmv.
Remark! This page is in continuous evolution.
-
Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta (2013) IC3 Modulo Theories via Implicit Predicate Abstraction. CoRR, abs/1310.6847. (url) (BibTeX)
-
Alessandro Cimatti, Raffaele Corvino, Armando Lazzaro, Iman Narasamdya, Tiziana Rizzo, Marco Roveri, Angela Sanseviero and Andrei Tchaltsev (2012) Formal Verification and Validation of ERTMS Industrial Railway Train Spacing System. In CAV., pages 378-393. (url) (BibTeX)
-
Alessandro Cimatti and Alberto Griggio (2012) Software Model Checking via IC3. In CAV., pages 277-293. (url) (BibTeX)
-
Alberto Griggio (2011) Effective word-level interpolation for software verification. In FMCAD., pages 28-36. (url) (BibTeX)
-
Alessandro Cimatti, Marco Roveri, Angelo Susi and Stefano Tonetta (2011) Formalizing requirements with object models and temporal constraints. Software and System Modeling, 10(2):147-160.(BibTeX)
-
Alessandro Cimatti, Marco Roveri, Angelo Susi and Stefano Tonetta (2011) Validation of Requirements for Hybrid Systems: a Formal Approach. ACM Trans. Softw. Eng. Methodol.. (BibTeX)
-
A. Cimatti, S. Mover, M. Roveri and S. Tonetta (2010) From Sequential Extended Regular Expressions to NFA with Symbolic Labels. In CIAA.. (BibTeX)
-
A. Chiappini, A. Cimatti, L. Macchi, O. Rebollo, M. Roveri, A. Susi, S. Tonetta and B. Vittorini (2010) Formalization and Validation of a Subset of the European Train Control System. In ICSE 2010.. (BibTeX)
-
A. Cimatti, M. Roveri, A. Susi and S. Tonetta (2010) Formalizing requirements with object models and temporal constraints. Journal of Software and Systems Modeling (SoSyM), To appear. DOI 10.1007/s10270-009-0130-7. (BibTeX)
-
A. Cimatti, M. Roveri, A. Susi and S. Tonetta (2010) Formalization and Validation of Safety-Critical Requirements. CoRR, abs/1003.1741, 2009 Workshop on Formal Methods for Aerospace. (BibTeX)
-
R. Sebastiani, S. Tonetta and M.Y. Vardi (2010) Symbolic Systems, Explicit Properties: On Hybrid Approachesfor LTL Symbolic Model Checking. STTT, To appear. DOI: 10.1007/s10009-010-0168-4. (BibTeX)
-
A. Cimatti, M. Roveri and S. Tonetta (2009) Requirements Validation for Hybrid Systems. In CAV 2009.. Springer, pages 188-203. (BibTeX)
-
S. Tonetta (2009) Abstract Model Checking without Computing the Abstraction. In FM 2009.. (BibTeX)
-
R. Cavada, A. Cimatti, A. Mariotti, C. Mattarei, A. Micheli, S. Mover, M. Pensallorto, M. Roveri, A. Susi and S. Tonetta (2009) EuRailCheck: Tool Support for Requirements Validation. In ASE 2009.. (BibTeX)
-
A. Cimatti, M. Roveri, A. Susi and S. Tonetta (2008) From Informal Requirements to Property-Driven Formal Validation. In FMICS., pages 166-181. (BibTeX)
-
A. Cimatti, M. Roveri, A. Susi and S. Tonetta (2008) Object models with temporal constraints. In SEFM.. IEEE Computer Society, pages 249-258. (BibTeX)
-
A. Cimatti, M. Roveri and S. Tonetta (2008) PSL Symbolic Compilation. IEEE Trans. on CAD of Integrated Circuits and Systems, 27(10):1737-1750. (BibTeX)
-
Alessandro Cimatti, Marco Roveri, Viktor Schuppan and Stefano Tonetta (2007) Boolean Abstraction for Temporal Logic Satisfiability. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. (Werner Damm and Holger Hermanns, Eds.) Springer, pages 532-546. (url) (BibTeX)
-
Alessandro Cimatti, Marco Roveri and Stefano Tonetta (2007) Syntactic Optimizations for PSL Verification.. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings. (Orna Grumberg and Michael Huth, Eds.) Springer, pages 505-518. (url) (BibTeX)
-
Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri and Andrei Tchaltsev (2007) RAT: A Tool for the Formal Analysis of Requirements. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. (Werner Damm and Holger Hermanns, Eds.) Springer, pages 263-267. (url) (BibTeX)
-
Alessandro Cimatti, Marco Roveri, Simone Semprini and Stefano Tonetta (2006) From PSL to NBA: a Modular Symbolic Encoding.. In Formal Methods in Computer-Aided Design, 6th International Confrence, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings.. IEEE Computer Society, pages 125-133. (url) (BibTeX)
-
Ingo Pill, Simone Semprini, Roberto Cavada, Marco Roveri, Roderick Bloem and Alessandro Cimatti (2006) Formal analysis of hardware requirements.. In Proceedings of the 43rd Design Automation Conference, DAC 2006, San Francisco, CA, USA, July 24-28, 2006. (Ellen Sentovich, Eds.) ACM, pages 821-826. (url) (BibTeX)
-
Roderick Bloem, Alessandro Cimatti, I. Pill, Marco Roveri and Simone Semprini (2006) Symbolic Implementation of Alternating Automata.. In Implementation and Application of Automata, 11th International Conference, CIAA 2006, Taipei, Taiwan, August 21-23, 2006, Proceedings. (Oscar H. Ibarra and Hsu-Chun Yen, Eds.) Springer, pages 208-218. (url) (BibTeX)
-
Alessandro Cimatti, Marco Roveri and Daniel Sheridan (2004) Bounded Verification of Past LTL.. In Formal Methods in Computer-Aided Design, 5th International Confrence, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004, Proceedings. (Alan J. Hu and Andrew K. Martin, Eds.) Springer, pages 245-259. (url) (BibTeX)