Duties:

Program Convenor: Bachelor of Information Technology (BIT)

Research interests:

• Software and systems engineering for safety and security critical systems
• Automata theory, temporal logics, and formal languages
• Runtime verification
• Access control
• Diagnosis

Bio:

since 2009: Senior Research Engineer, NICTA
since 2009: Adjunct Fellow, Research School of Computer Science, ANU
2007-2009: Research Fellow, RSISE, CSL, ANU
2007: PhD, TU Munich, Germany
2003: Master's in Computer Science, TU Munich, Germany

Research opportunities with Dr Andreas BAUER

• Android Security
• Reasoning about business operations

Research interests:

Advancement of automated deduction, in particular first-order logic theorem proving. Design of calculi (in particular the Model Evolution calculus), implementations (in particular the Darwin system) and their application for software verification and knowledge representation purposes; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.

Research opportunities with Dr Peter BAUMGARTNER

• Finding Models of Unsolvable First Order Goals
• Reasoning about business operations

Research interests:

I am interested in the application of logic, algebra and category theory to computer science. In particular, I have looked at the ubiquitous computer science notion of names that may be bound, and co-created Nominal Equational Logic for formalisms definable via equations modulated by side conditions regarding the 'freshness' of names.

I am currently interested in generalising this logic to deal with the complex and subtle binding structure that may occur in realistic computing applications.

Duties:

I am a postdoctoral researcher with the Logic and Computation group in the Research School of Computer Science.

Bio:

I obtained my PhD at the University of Cambridge. Prior to that I studied up to Masters level at Victoria University of Wellington.

Research interests:

Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.

Duties:

My research work previously at NICTA (and, prior to that, in my position as a Senior Research Associate on an ARC Large Grant held by Dr Rajeev Gore at the ANU) has largely been embedding a display calculus in Isabelle/HOL, and proving, in Isabelle, Belnap's cut-elimination theorem. In the course of work on a stronger result, the strong normalization property of the set of proof reductions used in cut-elimination, we discovered that the published proof of this omits a case, requiring a largely new proof, which we have now completed. We have realised that this proof can be translated into the context of general term-rewriting theory, and have accordingly derived theorems on termination of term-rewriting. Recently I have also mechanised some cut-elimination proofs for sequent calculi. I've been doing other things as well, see the publication list on my homepage. In the last couple of years with NICTA I was mostly working on Isabelle theories for fixed-length words in support of NICTA's L4 MicroKernel Verification project. Since returning to RSISE I first worked on machine-checked proof theory, doing a proof in Isabelle of the cut-elimination result for provability logic. Now I am working with Alwen Tiu on machine-checked proofs for the spi-calculus. Most recently I have formalised bitrace consistency, and proved results making it clear that consistency of an observer theory is decidable. I have also proved results which show, in combination with other published work, that consistency of a bitrace is decidable.

Research interests:

My main interests are in Gentzen systems for various logics, particularly modal logics and temporal logics. Currently I am working on the intricacies of Display Logic and how to obtain Gentzen systems for hybrid logics like intuitionistic modal logic. With Jeremy Dawson, I am working on formalising proofs of weak and strong normalisation for various calculi in the logical framework Isabelle. With Vaughan Coulthard, Jen Davoren and Thomas Moor I am working on inventing bi-modal tense logics with applications in hybrid systems. I am also interested in software engineering and security aspects of Java applications, particularly for JavaCards.

Duties:

I am currently the Leader of the Logic and Computation Group and am happy to answer questions about our group via email.

Bio:

I obtained my PhD from the Computer Laboratory of the University of Cambridge in 1992. Before that I completed my BSc (hons) and MSc at the Unviversity of Melbourne.

Research interests:

Dr Huang is a senior researcher at NICTA (Managing Complexity Research Group), with an adjunct appointment in the Research School of Computer Science at the Australian National University. His research interests include logical and probabilistic reasoning and their applications, and artificial intelligence in general. He completed his PhD in 2005 in the Computer Science Department at the University of California, Los Angeles as a member of the Automated Reasoning Group.

Dr Huang is available to supervise summer scholar, honors, and PhD projects at the ANU.

Research interests:

Computational logic, agents, declarative programming languages, and machine learning.

Duties:

John Lloyd is a Professor as well as the Associate Director (Research) within the Research School of Computer Science. In his capacity as the Associate Director (Research), he is responsible for providing advice on the strategic direction and coordination of research activity for the school. He provides support and advice to the Director of the Research School of Computer Science on all research matters including identifying emerging research areas, supporting academic research performance and ensuring effective recruitment to support the School's strategic directions. He represents the School at all networking forums, conferences and seminars within the College and the University in relation to research matters. Professor Lloyd is also the Program Convenor for the Bachelor of Computer Science (Honours).

Research interests:

formal methods, programming language semantics,theorem proving infrastructure, software engineering

Research interests:

My research interests lie in the areas of formal methods, interactive theorem proving (I am one of the developers of the HOL4 system), and formal semantics for complicated real-world systems. I am currently involved in the Trustworthy Embedded Systems and Automap projects within NICTA.

Bio:

I received my PhD in 1999 from the University of Cambridge, and was an undergraduate at Victoria University of Wellington.

Research opportunities with Dr Michael NORRISH

• Theory of Co-algebraic Types with Binders
• Proof Optimisation
• Finding Models of Unsolvable First Order Goals

Research interests:

Logic

• Relevant logic
• Other substructural logics
• Paraconsistency
• Temporal logic
• MaGIC

• ROO (Radically Optimized Otter)
• SCOTT (Semantically Constrained Otter)
• Miscellaneous contributions

• Constraint satisfaction
• Search
• Planning

Duties:

Professor in the Computer Sciences Laboratory, Research School of Information Sciences and Engineering. Head of Automated Reasoning Group since 1991.

Former leader of the Logic and Computation Program in NICTA (National ICT Centre of Excellence, Australia).

Instigator and convenor of the annual Logic Summer School.

Bio:

I was born in England but escaped, taught logic in philosophy departments for several years, escaped again and moved to Canberra in 1988 where I have been automating reasoning ever since.

I like doing this. The ANU is an idyllic place to be a researcher, Canberra is a better city to live in than you would believe from listening to Australians from anywhere else, NICTA is the most exciting research lab I know, and I actually get paid for thinking about logic and hacking code! That's as good as it gets.

Other likes: travel, good food (enthusiastic but inexpert cook), classical music (ditto pianist).

Dislikes: no really interesting ones (sorry).

Research interests:

My main interests are in logic, proof theory and process algebra, and their applications in computer science, in particular, in specifying and reasoning about models of computation and programming languages. I have recently taken interest in modeling security protocols in process algebra, using extensions of the pi-calculus, and in reasoning about such specifications using proof theoretic techniques. Other related areas of interest include theorem proving, logic programming, type theory, and formal verification of algorithms.

Duties:

I am a Fellow (senior researcher) in the Logic and Computation group in the Research School of Computer Science.

Bio:

I obtained my PhD degree from the Pennsylvania State University in 2004. I spent about a year as a visiting student at Ecole Polytechnique (France) during my PhD. I did a one-year postdoc at LORIA/INRIA Lorraine (2004 - 2005), prior to joining the ANU in 2006.

Research opportunities with Dr Alwen TIU

• Formal Logical Analysis of Security Protocols
• Solving Deduction Constraint Problems for Security Protocol Analysis
• Reasoning about Operational Semantics and Type Systems

Bio:

I completed my Ph.D. in Computer Science at Christian-Albrechts-University Kiel (Germany) in 2010. Before that, I obtained my Masters in Information Systems from Massey University (New Zealand) and Bachelor of Engineering from South China University of Technology (China).

Research opportunities with Dr Qing WANG

• Database Evolution and Migration
• Discovering Inconsistent Data
• Reasoning about XML Updates
• Institutional data matching