Nisansala Yatapanage

Dr. Nisansala Prasanthi Yatapanage
Research Fellow
ANU-ASD / Research School of Computer Science
Australian National University

I've been a researcher in formal methods since 2004. My research interests are in the verification of systems which exhibit a high degree of complexity, making them prone to errors and difficult to verify. I am particularly interested in safety-critical systems, which can potentially have serious impact. My research explores the various challenges associated with such systems, including methods to handle the concurrency aspects and methods for conducting failure analyses on systems that include potentially faulty hardware components.

At ANU, I'm currently looking at techniques for the verification of security protocols, working with Prof. Alwen Tiu.

Previously, I was a Senior Lecturer at De Montfort University, Leicester, U.K. I taught Data Structures & Algorithms and Concurrent & Parallel Algorithms to 2nd year students. I was also Deputy Programme Leader of the BSc Computer Science & BSc Software Engineering degrees.

From 2013 to 2017 I worked at Newcastle University in the UK on the Taming Concurrency project. This project aimed to investigate the fundamental aspects of concurrency, comparing the various methods for handling concurrency in order to extract an understanding of these core aspects. With Cliff Jones, I published a paper at SEFM 2015 (see below), which explores the use of abstraction for handling problems with strong separation of components, providing an alternative approach to the common separation logic methods. This abstraction solution helps to shed light on the fundamental qualities of separation. Similarly, we are now investigating a concurrent garbage-collection algorithm using rely-guarantee methods, in an attempt to understand the underlying qualities exhibited by such systems. Read the relevant papers here.

Before that, in my hometown Brisbane, I worked on several projects at Griffith University and The University of Queensland (UQ) from 2004 to 2007, as part of the ARC Centre for Complex Systems, on the verification of safety-critical systems using the Behavior Tree specification language, a language which maintains strong links between the natural language requirements and the formal model. My research focussed on using Behavior Trees and model checking to automate safety analyses. Read the relevant papers here.

My PhD thesis (obtained in 2012 from Griffith University, supervised by Kirsten Winter from UQ and Geoff Dromey at the start) is on the use of slicing techniques to reduce Behavior Tree models prior to model checking, to allow large systems to be verified. I also developed a novel form of branching bisimulation, called Next-preserving Branching Bisimulation, which allows stuttering behaviour to be removed while still preserving full CTL*, including the Next operator (see my journal paper listed below). Read the relevant papers or download my thesis here.

Following my PhD studies, I applied the failure analysis technique to an air-traffic control system for a project at UQ funded by NICTA.

Details of these projects can be found on my projects page.

See my papers or my thesis .

Latest News

Recent papers:
Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example with Cliff B. Jones published in Formal Aspects of Computing.
Next-preserving Branching Bisimulation with Kirsten Winter published in Theoretical Computer Science.
For details of both and to watch the Audioslides presentation for the TCS paper, see my papers page.