Formal Methods

At Nanjing University, from 1996-1999, I had been invloved in two projects on formal methods and verification. One is the design of a wide spectrum language/tool, called DD-VDM++, supporting systematic and rigorous software development. It is based on VDM with concurrent and object-oriented extensions. The other is the specification and verification of hybrid systems. Based on a state space decomposition approach, the design process is verified via an extended Hoare logic, whose soundness is mechanically verified in the PVS system.




Contact Info

Princeton University
Department of Computer Science
35 Olden Street
Princeton, NJ 08544

Tel: (609) 258-1794
Fax: (609) 258-1771
E-mail: dinghao@cs.princeton.edu

Home