SSRG News

A finite state Markov chain M can be viewed as a linear transform operating on the space of probability distributions over its set of nodes. We discretize the probability value space [0,1] into a finite set of intervals.. More...

It is difficult to build complex systems that (almost) never go (badly) wrong, yet this is what we expect of airplanes and pacemakers and the phone system. In essence, we have to anticipate everything that could fail or go wrong, develop countermeasures, and then provide compelling evidence that we have done all this correctly. Dr Rushby outline's some of the intellectual challenges in construction of suitable evidence, particularly as applied to software. More...

Formally modelling the software functionality and interactivity of safety-critical devices allows us to prove properties about their behaviours and be certain that they will respond to user interaction correctly. In domains such as medical environments, where many different devices may be used, it is equally important to ensure that all devices used adhere to a set of safety, and other, principles designed for that environment. More...

We present a novel coalgebraic formulation of infinite extensive games. We define both the game trees and the strategy profiles by possibly infinite systems of corecursive equations. More...

One of our main research goals is to empirically understand how software engineers work with technologies and interact with each otters when developing software. To this end, we have conducted several dozens of empirical studies in industrial and academic environments. More...

The fields of neural computation and artificial neural networks have developed much in the last decades. Since technical, physical, and also cognitive processes evolve in time, neural networks should be considered, which allow us to model the synthesis and analysis of continuous and possibly periodic processes in time besides computing discrete classification functions. More...

Over the last years, the means to collect personal data implicitly or explicitly over the Web and by various kinds of sensors and to combine data for profiling individuals dramatically increased thus leading privacy violations. More...

Simple games are yes/no cooperative games which arise in many practical applications, such as in political sciences and economics. We have obtained amazing positive results when using the BDD-based relation algebra tool RelView for solving computational problems on them. More...

In this talk we consider the problem of representing and reasoning about systems, especially probabilistic systems, with hidden state.   We consider transition systems where the state is not completely visible to an outside observer. Instead, there are observables that partly identify the state More...

While parallel hardware substrate has evolved considerably over time, a key performance problem has remained the same: how best to feed processing cores with data fast enough. Managing locality is a key aspect of mitigating the memory wall. Yet this is non-trivial given unpredictable memory sharing patterns, coupled with complex and distributed memory hierarchies. More...

Featuring lectures by international leaders in computer systems from industry and academia, interspersed with short student talks and poster sessions. Topics include virtual machines, hypervisors, compilers, operating systems, language implementation, memory management and security. Detailed page here

Over the past few years, cloud computing and the growth of global large scale computing systems have led to applications which require data management across multiple datacenters. Initially the models provided single row level transactions with eventual consistency. Although protocols based on these models provide high availability, they are not ideal for applications needing a consistent view of the data. More ...

A filestore is a structured collection of data files housed in a conventional hierarchical file system. Many applications use filestores as a poor-man's database, and the correct execution of these applications requires that the collection of files, directories, and symbolic links stored on disk satisfy a variety of precise invariants. Moreover, all of these structures must have acceptable ownership, permission, and timestamp attributes. Unfortunately, current programming languages do not provide support for documenting assumptions about filestores, detecting errors in them, or safely loading from and storing to them. More ...

A multi-million-dollar contract with the United States Government will see a team of computer scientists from NICTA develop a new breed of software to protect the critical systems in unmanned vehicles from cyber attack. NICTA press release

Over two days, this summer school will feature lectures by international leaders in computer systems from industry and academia, interspersed with short student talks and poster sessions. We will emphasise a friendly and informal setting where students can learn and obtain feedback from experts. Topics include compilers, operating systems, language implementation, security and formal verification. Postgraduate students may apply ...

Andreas Bauer together with Ylies Falcone, University of Grenoble, France, won the best paper award at the International Symposium on Formal Methods (FM 2012) for the paper Decentralised LTL Monitoring. This work is the first to introduce a truly distributed runtime verification procedure for a class of distributed systems that have no means of a global trace collection. FM is one of the premier conferences in the area of formal methods research for the improvement of software and hardware in computer-based systems.

Timothy Bourke, Matthias Daum, Gerwin Klein and Rafal Kolanski won this year's best paper award at the Conferences on Intelligent Computer Mathematics (CICM 2012) for their submission Challenges and Experiences in Managing Large-Scale Proofs. Their paper describes problems and solutions specific to large machine-checked proofs such as NICTA's seL4 microkernel verification or formally verified software stacks as in the German Verisoft project. Such proofs take multiple people over multiple years. They create new problems, because no single human has the ability to understand all details of all aspects of the proof.

Liming Zhu, Ross Jeffery & Jason Zhang won the Best Paper Award @ the 17th International Conference on Evaluation & Assessment in Software Engineering
(EASE 2012). This paper An Initial Evaluation of Requirements Dependency Types in Change Propagation Analysis is the result of ongoing collaboration with the Chinese Academy of Science and improves the understanding of systems dependency in change propagation.

Gernot Heiser has accepted the position of PC co-chair @ the 9th Annual Conference on Virtual Execution Environments (VEE 2013) to be held in Houston, Texas, USA.

Guido Governatori has been made Associate Editor of the Journal of Research and Practice of Information Technology. The Journal has a dual emphasis and contains articles that are of interest both to practicing information technology professionals and to university and industry researchers. In particular, it encourages papers that report on activities that have successfully connected fundamental and applied research with practical application.

Liming Zhu, Ross Jeffery, Quanqing Xu & Anna Liu have been awarded the Australia-China Group Mission Grant from the Dept of Industry & Innovation, Science, Research & Tertiary Education. This will be used to promote research and technology collaborations with the Institute of Software Chinese Academy of Science (ISCAS) and Peking University, to build dependable systems and demonstrate NICTA technologies to companies in China.

We have released one of the main C verification tools in the L4.verified project under BSD license. The C-to-Isabelle parser reads C99 files into the theorem prover Isabelle/HOL and provides the basis for their formal verification.

Download the C parser here.

NICTA and German IT security specialist secunet Security Networks AG have entered a strategic research collaboration to develop high-security information technology (IT) products for the defence and government sectors. The research will combine secunet's experience in designing and building high-security devices with NICTA's expertise in formal verification and secure microkernel technology.

Download the full press release here.

SSRG students Etienne Le Sueur, Bernard Blackham, Martin Pflauminger and Aaron Carroll have won the 2011 Lantronix XPort Pro Design Contest with their e⁴Meter.

NICTA and OK Labs have announced the first joint public release of the formally verified seL4 microkernel (branded OKL4 Verified). The release, for non-commercial and evaluation use, contains seL4 kernel binaries for ARM and x86, documentation, user level examples, x86 Linux on top of seL4, and the formal specification of the kernel for the ARM platform.

NICTA press release
Download seL4
L4.verified project

OK Labs has announced that OKL4, derived from NICTA's L4-embedded microkernel, has now shipped in more than 1.1 billion mobile phones. This makes OKL4 one of the most widely-deployed OS kernels ever.

NICTA press release

We have released a snapshot of the vNUMA source for download.

A paper titled Improved device driver reliability through hardware verification reuse has been accepted for publication in the 16^th ASPLOS Conference. The paper is the result of a collaboration with Intel (Hillsboro, OR) lead by SSRG researcher Leonid Ryzhyk.