Marco Roveri: Areas of Interest

• Software Engineering. with a particular focus  in the integration of Formal Methods in the development process. In doing this we started the investigation of the integration of Formal Methods in the Tropos development process.
• Formal Methods, with a particular focus on Symbolic Model Checking:
  • SMV model checker developed at Carnegie Mellon.
  • VIS (Verification Interacting with Synthesis) is a system for formal verification, synthesis, and simulation of finite state systems. It has been developed jointly at the University of California at Berkeley, the University of Colorado at Boulder, and more recently at the University of Texas, Austin.
  • Abstraction and Symbolic Model Checking, and all the new reduction techniques applicable in Symbolic Model Checking.
    
  • I am working at the development of NuSMV, a new model checker which should be usable, customizable and extensible, with as little effort as possible, also by people different from the developers. A further goal is to produce a system which is very robust, and close to the standards required by industry. The starting point for this project is the SMV system developed at CMU. The development of NuSMV is being carried out as a joint project between Fondazione Bruno Kessler (formerly ITC-irst) and Ed Clarke's group at CMU.
    • The NuSMV model checker is currently available at the URL: http://nusmv.fbk.eu.
      

  • Integration of Formal Methods in the design cycle of complex systems.

• Planning via Model Checking.
  • This new approach to planning is based on two main ideas. First, we use a high level action language to represent complex (e.g. nondeterministic) planning domains. A domain description can be automatically reduced to a finite state automaton. Second, model checking techniques are used to compatcly represent and efficiently search the automaton. A more expressive notion of plan, which includes conditionals and iterative constructs, allows for the solution of complex planning problems in nondeterministic domains. The MBP (Model Based Planner) planner, based on the ideas discussed above, was developed on top of NuSMV.
  • Conformant Planning is the problem of finding, in a nondeterministic domain, a sequence of actions which will achieve the goal for all possible contingencies. Main result of this research is the developent of an efficient algorithm for conformant planning, based on symbolic model checking technques. Information about the algorithm can be found visiting this link.

• Abstraction is a mapping between the languages of two formal systems. It has been widely used in theorem proving as a tool for explanation and for reducing the search space.
  
• ABSFOL is an interactive theorem prover by abstraction. ABSFOL is built on top of GETFOL and is developed by Fausto Giunchiglia, Adolfo Villafiorita, Roberto Sebastiani and myself. If you want to have more information about this system, please send en e-mail to or to Adolfo.
  

Marco Roveri <>