My area is automated deduction (AD). AD is concerned with push-button technology for logical reasoning on computer. AD systems take as input a formula of a formal (mathematical) logical language, such as propositional or first-order predicate logic, and apply inference rules of a logical calculus to analyse the formula for its properties (see here and here for an overview of the area, and here for mathematical logic more in general). Typically, one is interested in determining whether the formula is valid ("always true"), satisfiable ("sometimes true"), under what conditions it is valid, whether it is valid in a fixed interpretation ("model checking"), among others.
Research in AD is highly specialized. My specific research interest is the design of AD systems for first-order predicate logic and applying them to solve real-world problems. Often this requires "smarter" theorem provers than those available today, by adding dedicated reasoning support for specific theories, such as (integer) arithmetic.
Please see the Automated Reasoning project page for more information on what we are doing.
I welcome students to work with me on in the areas mentioned. Student projects can be carried out towards a honors degree, a masters degreee, a Ph.D. degree, a Summer Internship or a project in the Erasmus Mundus CL program. We have compiled a list of projects that is targetted for EMCL students but other students may find something of interest as well.
General information on NICTA scholarships is here.