Candidate will be developing case studies of the use of model checking (and/or Symbolic AI) technology in the application of developing simulation/controller codes. Workflows in this domain are currently undertaken using detailed simulation studies that appeal to hard/expensive to acquire data. These expensive incumbent workflows identify potential issues with a simulator/controller, which can then be addressed by scientists and engineers. Codes are developed over years, an become quite complex and thereby potentially error prone. Model checking and symbolic AI are motivated here, to push the envelope on the class of errors which can be eliminated prior to expensive computational or physical resources are expended.
This project contemplates the development and empirical study of simplistic codes, derived by the candidate should they wish to do that. Many codes (Fortran and C++) that are amenable to model checking in practice are already available for study.
Possible prospective investigations
For a class of potential issues—e.g., (1) exceeding superconducting coil current limits, or (2) simulated soundwave in a plasma exceeding the speed of light—determine whether existing software model checking tools are able to efficiently reason about those issues, and characterise the computational effort of doing so.
General information about the Work Group, the University and the region
Collaborations between Australian and European scientists played a pioneering role in fusion science, with the first laboratory fusion reaction realised by Mark Oliphant (Australian) and Paul Harteck (Austrian). The tradition of Oliphant’s pioneering research continues at the Australian National University (ANU), which is ranked 1st in Australia, and 27th in the world, by the QS World University Rankings, 2022, and 2nd in Australia, and 54th in the world, by Times Higher Education Rankings, 2022. Australia has a 77 year history of studying plasma physics, with ANU playing a historical and central role, being for example the first institution in the world outside the (then) USSR to host experimental Tokamaks (1964-69). With regulatory changes in April 2023 in the USA, opening the door to an significant 21st century commercial fusion industry, now is an exciting time to get involved in fusion science and the development of the enabling AI technologies for that.
The student will be working at the ANU under the supervision of computer scientist Dr Charles Gretton. Dr Gretton is a member of the Intelligence Cluster in the School of Computing, which is part of the College of Engineering and Computer Science at the Australian National University. Dr Gretton collaborates with and is co-located with fusion science experts, such as Prof. Matthew Hole in the Mathematical Sciences Institute.
Canberra is a sunny modern city located on the traditional lands of the Ngunawal and Ngambri peoples, who lived in the region for more than 20,000 years. The city is the so-called “bush capital", showcasing the unique flora and fauna adjacent Australia’s eastern seaboard. Canberra is the capital city of Australia, located ~3.5 hours from Sydney by road, and 1 hour from Sydney by plane. In Canberra you are also a short (bus) drive from beautiful beaches (Batemans Bay), and from the highest alpine region of Australia for those who like bush walking (Kosciuszko National Park).
IMAGE: Photomontage of rendering of next step fusion experiment ITER, taken from Australian ITER forum (https://fusion.ainse.edu.au/)
Although these skills can be acquired over the course of the project, familiarity with compilation of Fortran and/or C++ via LLVM will be a plus. Familiarity with bounded model checking (e.g., using CBMC) also a bonus, and otherwise something to look forward to learning. And of course, if you are already a plasma physicist, then that likely puts you ahead-of-the-curve when interpreting codes and their outputs.