She first worked on some problems related to pattern recognition.
She worked on programming language semantics, program properties and their automatic proofs. She defined a semantics for PASCAL in LCF (Logic for Computable Functions) and machine checked several proofs of (nontrivial) properties.
She designed and implemented a theorem prover named PPC, Pisa Proof Checker; published some papers describing the (object oriented) programming paradigm used in its development, and its evaluator (an interpreter for the full lambda calculus).
She participated and contributed to the development and use of Wehyrauch's FOL system.
She has investigated on the advantages of the use of meta-level knowledge in AI systems, both to control search and to do reasoning about reasoning in multi-agent systems.
In addition to some work in the area of Logic Programming and data bases, she carried on some experiments of application of Artificial Intelligence techniques to the development of Expert Systems for medical diagnosis; she has also done some work in Intelligent Tutorins Systems, both for supporting the learning of scientific disciplines, and of English as a second language for Italians.