Research in this area focuses on the study of logic-based methodologies for the development of correct software from formal specifications. We consider programming environments where specifications use a formalism based on suitable fragments of predicate logic, and programs are written in a declarative programming language, such as, constraint or logic programming. This approach allows us to view the process of software development as deduction in a logical theory, thereby guaranteeing the correctness of the final software product. A major effort is being expended to mechanize those deductive techniques which can be employed for the automated production of correct software.Research topics
Rule-based transformation of constraint and logic programs; automatic program improvement; program specialization; program synthesis.
VERIFICATION OF SOFTWARE SYSTEMS
Automated theorem proving in first-order logic; verification or reactive systems; model checking of infinite-state systems.