First-order logic theorem proving; applications for software verification,
knowledge representation, and dynamic systems analysis; exploiting connections
into related areas such as logic programming, description logics and
nonmonotonic
reasoning.
Project: Verification
Tools and Automation.
See my NICTA home page for a brief CV.