Older Events
| 2014-12-20 Gernot Heiser named ACM Fellow |
|---|
| Professor Gernot Heiser has been recognised as an ACM Fellow. |
| 2014-12-13 Doctorate Awarded |
| Andrew Boyton’s PhD thesis has just been officially accepted, without changes from either reviewer and only 2.5 months after submission. |
| 2014-12-05 — Visitors to NICTA and UNSW |
| Tony Hosking (Purdue) and Haibo Chen (Shanghai'TJ) visited UNSW and NICTA. Both gave seminars and met with staff and students |
| 2014-11-25 Best student research paper award |
| David Cock won the CiSRA/CSE best student research paper award for his paper, ‘The last mile, an empirical study of timing channels on seL4’ with Qian Ge,Toby Murray and Gernot Heiser. |
| 2014-11-22 Paper presented at Top Security Venue |
| David Cock presented his paper on analysing covert timing channels in seL4 at CCS, one of the top security venues |
| 2014-11-17 German Chancellor Angela Merkel arrived at the National ICT Australia’s offices in Sydney |
| The German Chancellor and most powerful woman in the world had a host of post-G20 commitments in Sydney and chose to spend 45 minutes touring NICTA’s labs near Redfern. She was accompanied by Communications Minister Malcolm Turnbull and Industry Minister Ian Macfarlane during her tour of NICTA. more |
| 2014-09-30 Seminar Pablo González de Aledo - Symbolic-Execution for software verification |
| In this talk Pablo is going to talk about his work on symbolic execution and how the technique can be used for different purposes in software verification, particularly Automated Test Pattern Generation, Model-Checking, bug detection and equivalence checking. Future work and possible collaborations with Nicta in this area will be spotted |
| 2014-09-26 A Software Architect's Perspective |
| Len Bass, Ingo Weber and Liming Zhu completed the first pass of the book DevOps: A software Architect's perspective and it has been written and posted to SlideShare. |
| 2014-09-19 Entrepreneur of the Year award |
| Prof Gernot Heiser was awarded Entrepreneur of the year award at the Engineers Australia 2014 Sydney Engineering Excellence awards. |
| 2014-09-06 UNSW Open Day |
| UNSW open day had an SSRG stand showing the quadcopters and SMACCM video |
| 2014-08-29: DevOps Book publishes another chapter |
| Another chapter of the book DevOps has been published. It is written by Len Bass, Ingo Weber and Liming Zhu — A software Architect's Perspective. In 2 days it had 75 views |
| 2014-08-27: AURIN/HTS Grant Received |
| A further 150K external funding has been approved for AURIN/HTS project to integrate HTS data on the national map. |
| 2014-08-26: Seminar Prof Vladimir Estivill-Castro on Correctness by Construction with Logic-Labelled Finite-State Machines – Comparison with Event-B |
| Formal methods have seen emergent success recently with the deployment of Event-B. However, Event-B explicitly postulates that models there are not executable. This seems to contradict the parallel emergence of model-driven development (MDD). We show here that logic-labelled finite-state machines (LLFSMs) are effective in carrying out the “correct from construction” agenda of formal methods such as Event-B and simultaneously achieve the aims of MDD. As a result, we obtain models that are directly interpretable, compilable, and executable enabling traceability, transparency and rapid maintainability; while at the same time enabling simulation, validation and formal verification with model checking. Moreover, the Event-B capacity to develop closed models is also very natural with arrangements of LLFSMs; and therefore further safety analysis such as failure-mode effects analysis (FMEA) can be performed. We demonstrate this with two well-known examples in the literature. |
| 2014-08-25 Seminar Dr Han on Next-Generation Storage and Its Software |
| Recently, storage devices have been greatly improved in terms of both bandwidth and latency by using non-volatile memories such as Flash and PRAM. However, traditional storage software stack such as operating systems and database systems becomes major performance bottleneck since they are optimized for hard disk drives and they are not suitable for new storage devices. We call this phenomenon "slow software on fast storage". For the seminar, histories of storage devices will be given in terms of interconnection and bandwidth. Then, I will show an example of software optimizations for fast storage devices, and describe our current work about virtual memory of operating systems. Finally, I'll present our future work about application-level optimizations for fast storage devices. |
| 2014-08-23 Doctorate Awarded |
| David Cock has received his Doctorate. He worked to extend seL4's assurance case to non-functional security properties. Established an empirical approach to detecting and mitigating covert and side channels. |
| 2014-08-13 Seminar Roy on A CSP-theoretic framework of checking conformance of business processes |
| In this talk, we tackle the problem of conformance checking which > verifies if the event logs (observed) match/fit the reference (arbitrary) process. We use concepts from Communicating Sequential Processes (CSP), which facilitates automated analysis using PAT toolkit. By this technique one can identify all the logs which cannot be properly replayed on the process. We illustrate our approach with an example. Finally, we introduce some metrics based on conformance checking. They are related to fitness, closeness, and appropriateness of the event logs vis-a-vis reference process models. We further indicate that such a framework can be used to tackle the problem of both static and run-time compliance checking for business processes. Our work is motivated by user friendly need of employing easy input technique of models and keeping the model checking work at the back-end. |
| 2014-08-05: Podcast Interview with Len Bass |
| Architect Len Bass and author of Software Architecture in Practice has been interviewed for a podcast . |
| 2014-07-29: seL4 is open source! |
|
Today seL4 was released as open-source. In addition to
kernel and proofs, sample projects, the CAmkES component
framework, and a test suite were made available.
Details on how to download are at http://sel4.systems/. |
| 2014-07-26 Paper accepted at OSDI |
| Adam Walker and Leonid Ryzhyk of SSRG have a paper accepted to OSDI--one of the most competitive and prestigious conferences in computer science. The paper describes their Termite device driver synthesis tool, which uses game theory to automate the tedious and error-prone task of driver development. Termite is a joint project with Intel Labs and University of Toronto. This work is part of the broader research agenda on using rigorous mathematical techniques to create better operating systems, pursued by the OS research group at SSRG |
| 2014-07-25: Ninth Max-SAT Evaluation |
|
Visiting Researcher Nina Narodytska, (University of
Torento) has won 3 awards with her solver Eva500a at the
ninth
Evaluation of Max-Sat Solvers. First place in
the weighted partial MaxSat category and third place in
both partial MaxSAT and the MaxSat (industrial)
category
|
| 2014-07-23: Beagle Theorem Prover |
| Peter Baumgartner has won a medal for his beagle theorem prover for the most improved automated theorem prover in the annual world championship of automated theorem provers |
| 2014-07-23: SYNTCOMP |
| Student Adam Christopher Walker received first place with his game solver in a sequential realisability track of the SYNTCOMP competition. The competitions goal is to collect benchmarks and foster research in new tools for automatic synthesis of systems |
| 2014-07-03 Seminar Sergey on Innopolos: A New Model for Academia and Industry Partnership |
| Building a partnership between software industry, academic, and research is a dramatic challenge due to the differences in the objectives and goals. The paper describes a recent Russian startup, an ambitious Innopolis project. The new city is to be erected 20 miles away from Kazan' the capital of Tatarstan Republic. The idea is the use the synergy of IT academicians, researchers and practitioners in a single location. The project will yield to a new powerful IT cluster of a university and hi-tech companies. By 2030, the new city is to host around 155,000 inhabitants and provide high-end residential conditions and recreation facilities in an ecology-friendly environment. The new IT university is to train up to 10,000 students, it will acquire the best experience from world-known computer science and software engineering schools including Carnegie Mellon, ETH Zurich, and some others |
| 2014-07-02 Seminar Pohl (University of Duisburg-Essen) on Challenges for Information Systems Engineering and Operation |
| After a short introduction of IoS and IoT the talk outlines the potential of future information systems which utilize the capabilities of IoS and IoT. He illustrates those potentials using examples from the logistic domain. Utilizing the capabilities of IoS and IoT raises new challenges for engineering and operating future information systems. We briefly discuss those challenges and sketch a potential architecture addressing those challenges which include monitoring, runtime, quality prediction and adaptation |
| 2014-05-23: Podcast Interview with Len Bass |
| Architect Len Bass and author of Software Architecture in Practice was interviewed for a podcast that was released on Friday 23rd May where he shared some of his stories over his 40+ year career in software |
| 2014-05-19: Seminar Bjørner (TU Denmark) on 40 years of Formal Methods |
| Dines Bjørner delineates what is meant by method, formal method, computer science, computing science, software engineering, and model-oriented and algebraic methods. Based on that he characterises a spectrum from specification-oriented methods to analysis-oriented methods. Then he provides a survey: which are the prerequisite works that have enabled formal methods and which are, to us, the classical formal methods. A related paper is at http://www.imm.dtu.dk/~dibj/2014/fm40-paper.pdf |
| 2014-05-06: NSW Big Picture Seminar Cutting (Stanford University, California) on The Future of Data |
| In recent years a wide range of new technologies have disrupted traditional data management. We're now in the middle of a revolution in data processing methods. Choosing allegiances in a revolution is risky. In this talk, Doug will present the underlying causes of the revolution and predict how the data world might look once we're through it. |
| 2014-05-05 CeBIT Australia |
| NICTA's stand at CeBIT showcases our trustworthy systems technology |
| 2014-04-01 ACM SIGBED Paul Caspi Memorial Dissertation Award |
| Former SSRG PhD student Bernard Blackham has won the ACM SIGBED Paul Caspi Memorial Dissertation Award. The selection criteria was the scientific quality of the paper and the exposition of the ideas |
| 2014-04-08 Most Influential Paper Award — ASWEC 2014 |
| Liming Zhu and Ross Jeffery from SSRG just won the most influential paper award at ASWEC 2014 for their paper “A framework for classifying and comparing software architecture evaluation methods” published in ASWEC 2004. The paper gathered a total of 160 citations. |
| 2014-04-06 Book Release for Public Review — DevOps: A Software Architect's Perspective |
| Len Bass, Ingo Weber and Liming Zhu are currently writing a book titled “DevOps: A Software Architect's Perspective,” which they will be releasing one chapter per month for public review. The first 6 chapters are currently available and already have 500 views each. |
| 2014-03-28 Engineering Panel of the Marsden Fund |
| Professor Gernot Heiser accepted invitation to Engineering Panel of the Marsden Fund, NZ equivalent of ARC Discovery More... |
| 2014-03-25: Seminar Venugopal (UNSW) on Towards a Unified View of Elasticity |
| The defining feature of cloud computing is elasticity, or the ability to add and remove resources at will. Elasticity has created interesting opportunities for research into resource provisioning, fault tolerance, and scalability. However, most of the current research into elasticity has focussed on linear scaling of application logic without reference to management of state information. Additionally, current solutions for scaling applications relies on centralised control using threshold-based rules. This talk will focus on research performed in UNSW on decentralised and autonomic scaling of applications on cloud resources. It will describe a scaling mechanism that learns application performance characteristics in order to make decisions on adding or removing cloud resources. It will also touch upon our efforts on elastically scaling the persistence layer. This talk will end with some thoughts on presenting a unified view of elasticity across the entire application stack. |
| 2014-03-21: Seminar Nestmann (TU Berlin) on Dynamic Coalitions and Dynamic Event Structures |
| Dynamic Coalitions essentially represent a coordination principle, where hierarchically nested sets are equipped with a notion of dynamic membership. Challenges, however, arise from extensions by further dimensions with, for example, private data and corresponding access policies. Dynamic Event Structures were developed in order to support the formation of Dynamic Coalitions. The first part of the talk provides an overview of our current work in this area. The second part focuses on some of the technical aspects of Dynamic Event Structures. |
| 2014-03-18: Seminar Luttik (TU Eindhoven) on Unique Parallel Decomposition |
| A recurring question in process theory is to what extent the behaviours definable in a certain process calculus have a unique decomposition into indecomposable parallel components. Milner and Moller were the first to consider the unique decomposition property in a process calculus for specifying simple finite behaviours. Since then, the property has been re-established several times for different process calculi, each time using a variant of the same proof idea, and most recently for a fragment of the applied pi-calculus. Bas Luttik will present and discuss an abstract theory of unique decomposition in commutative monoids that is tailored towards application in process theory, explain how the theory can be straightforwardly applied to establish unique parallel decomposition in process calculi modulo strong bisimilarity, and how an adaptation facilitates application in settings modulo weak and branching bisimilarity. |
| 2014-03-14: Seminar Futatsugi (JAIST) on Generate & Check Method for Verification of Transition Systems |
| Effective coordination of inference (a la theorem proving) and search (a la model checking) is one of the most important and interesting research topics in formal methods. We have developed several techniques for coordinating inference and search for verification with proof scores in CafeOBJ. The generate & check method is a recent development of this kind in verification of transition systems with CafeOBJ. The method is based on (1) state representations with state patterns, and (2) systematic generation of finite state patterns which subsume all possible infinite states. This talk explains the generate & check method using a simple but non-trivial example of mutual exclusion protocols. |
| 2014-02-25: Seminar Reeves (University of Waikato, Hamilton) on Adding Visualisations to Formal Models of Interactive Medical Devices |
| Creating formal models of interactive medical devices, such as infusion pumps, allows us to perform important checks to ensure that both the functionality of the device and its interaction possibilities correctly support requirements. As these are safety-critical devices errors can be potentially fatal. We often want to be able to demonstrate aspects of behaviour from the models to medical practitioners, bio-technicians, device manufacturers etc. who are not typically familiar with the languages and notations of our models. The best way to communicate with these people is via simulations of the device, however developing such simulations is time-consuming and error-prone. In this paper we describe ongoing work which looks at ways of creating visualisations and simulations directly from the formal models as a way of addressing this problem. |
| 2014-02-18: NSW Big Picture Seminar Franklin (University of California, Berkeley) on The Berkeley Data Analytics Stack: Present and Future |
| This talk will outline the AMPLab's research approach and describe how we have integrated the three main resources available to address the cross-disciplinary nature of Big Data challenges: Algorithms (such as machine learning and statistical techniques), Machines (in the form of scalable clusters and elastic cloud computing), and People (individually as analysts and as crowds). |
| 2014-01-16: Seminar Clarke & Osterweil (University of Massachusetts Amherst) on Process-based Security Analysis for Human-intensive Systems |
| This talk describes a process-model based, systematic approach for detecting security vulnerabilities in human-intensive systems. Such systems typically involve complex interaction and cooperation among software applications, hardware devices, and human participants, and are increasingly central to key societal infrastructure.Thus, protecting such systems from attack is correspondingly centrally important. Clarke and Osterweil view is that these systems can be viewed as collections of processes whose security can be improved by modelling, analysing, and subsequently using the feedback gained to support continuous improvement. Their work features a process-modelling notation, with rich and well-defined semantics, that is able to represent the complexity of such systems as well as be the subject of rigorous analysis, such as model checking and fault-tree analysis. In this talk, Clarke and Osterweil will describe how they applied their approach to models of election processes used in Yolo and Marin Counties in California, show how their analyses have identified some example vulnerabilities, and indicate the kinds of improvements that can reduce vulnerabilities. Although no system can ever be made immune to any possible attack, Clarke and Osterweil believe that their approach of using technology to support continuous improvement represents an effective way to address the urgent need to protect the key infrastructure. |
| 2013-12-17: Seminar Bourke (INRIA & ENS - Paris) on Mechanization of a mesh network routing protocol & the proof of its loop freedom in Isabelle/HOL |
| This talk describes recently completed work to transfer a formal but pencil-and-paper model and analysis of a wireless mesh network protocol (AODV) into the proof assistant Isabelle/HOL. The nodes of such networks are reactive systems that cooperate to provide a global service (the sending of messages from node to node) satisfying certain correctness properties (messages are never sent in circles). |
| 2013-12-09: Seminar Khakpour (Royal Institute of Technology KTH - Stockholm) on Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel |
| A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information security for a simple separation kernel for ARMv7. |
| 2013-11-12: Seminar Schryen (University of Regensburg) on Emergency Response in Natural Disaster Management |
| Emergency Response in Natural Disaster Management: Allocation and Scheduling of Rescue Units Natural disasters, such as earthquakes, tsunamis and hurricanes, cause tremendous harm each year. In order to reduce casualties and economic losses during the response phase, rescue units must be allocated and scheduled efficiently. As this problem is one of the key issues in emergency response and has been addressed only rarely in literature, we suggest a decision support model that minimises the sum of completion times of incidents weighted by their severity. |
| 2013-11-01: Seminar Kopetz (Technical University of Vienna) on The Time-Triggered Architecture |
| The Time-Triggered Architecture (TTA) provides a computing infrastructure for the design and implementation of dependable distributed embedded systems. A large real-time application is decomposed into nearly autonomous clusters and nodes, and a fault-tolerant global time base of known precision is generated at every node. In the TTA, this global time is used to precisely specify the interfaces among the nodes, to simplify the communication and agreement protocols, to perform prompt error detection, and to guarantee the timeliness of real- time applications. |
| 2013-09-30: Call for Participation - Second NICTA Software Systems Summer School |
| 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 operating systems, hypervisors, virtual machines, databases, compilers, language implementation, memory management and security. Postgraduate students may apply. |
| 2013-09-11: Paper accepted - ACM TOCS |
| A paper entitled Comprehensive Formal Verification of an OS Microkernel has been accepted for publication in ACM Transactions on Computer Systems |
| 2013-08-30: Best Paper Award - BPM 2013 |
| Marcello La Rosa, Principal Researcher and co-author of Slice, Mine and Dice: Complexity Aware Automated Discovery of Business Process Models won the Best Paper Award at the 11th International Conference on Business Process Management 2013 held in Beijing 27 - 28 August. More... |
| 2013-08-20: Seminar Sabelfeld (Chalmers University of Technology) on Tracking Information Flow in Web Applications |
| This talk discusses a principled approach to web application security through tracking information flow in web applications. Although the agile nature of developments in web application technology makes web application security much of a moving target, we show that there are some fundamental challenges and tradeoffs that determine possibilities and limitations of automatically securing web applications. |
| 2013-07-29: Best Student Paper Award - APSys 2013 |
| Aaron Carroll PhD Student won Student Best Paper at Asia Pacific Workshop on Systems (APSys 2013) for the paper The Systems Hacker's Guide to the Galaxy: Energy Usage in a Modern Smartphone. This paper is co-authored with Gernot Heiser. More... |
| 2013-04-24: Seminar Thiagarajan (National University of Singapore) on Approximate Verification of the Symbolic Dynamics of Markov Chains |
| 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. |
| 2013-04-23: Seminar Rushby (SRI International) on The Challenge of High-Assurance Software |
| 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. |
| 2013-04-19: Seminar Reeves (University of Waikato) on Modelling Safety Properties of Interactive Medical Systems |
| 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. |
| 2013-04-09: Seminar Abramsky (Oxford University) on Coalgebraic Analysis of Subgame-perfect Equilibria in Infinite Games without Discounting |
| 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. |
| 2013-03-20: Seminar Babar (Lancaster University) on Experiences from Human-Centric Software Engineering Research |
| 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. |
| 2013-03-19: Seminar Stolzenburg (Harz University) on Neural Learning with Applications in Object Recognition and Harmony Perception |
| 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. |
| 2013-03-12: Seminar Freytag (University of Humboldt) on Privacy Challenges in Data intensive Processing Systems |
| 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. |
| 2013-03-01: Seminar Berghammer (University of Kiel) on Simple Games and the Use of BDDs for solving Problems |
| 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. |
| 2013-02-26: Seminar Panangaden (McGill University) on Duality for Transition Systems |
| 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 |
| 2013-02-21: Seminar Stumm (University of Toronto) on Improving Memory Access Locality |
| 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. |
| 2013-02-05: First NICTA Software Systems Summer School - Sydney Australia. |
| 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. |
| 2013-02-01: Seminar Agrawal (UCSB) on Managing Geo-replicated Data in Multi-Datacenters |
| 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. |
| 2012-12-11: Seminar Fisher (DARPA) on Forest - A Language and Toolkit for Programming with Filestores |
| 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. |
| 2012-11-15: NICTA to develop critical software for multi-million-dollar US Government cyber-security project |
| 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. |
| 2012-10-31: Call for Participation - First NICTA Software Systems Summer School |
| 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 ... |
| 2012-08-27: Best Paper Award - FM 2012 |
| 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. |
| 2012-07-04: Best Paper Award — CICM 2012 |
| 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. |
| 2012-05-28: Best Paper Award — EASE 2012 |
|
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. |
| 2012-04-02: Program Committee co-chair @ VEE 2013 |
| 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. |
| 2012-04-17: Associate Editor @ the Journal of Research and Practice in Information Technology |
| Guido Governatori has been made Associate Editor of the Journal of Research and Practice in 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. |
| 2012-03-30: SSRG awarded Australia-China Mission Grant |
| 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. |
| 2011-12-14: C verification tool released. |
|
We have released one of the main C verification tools in the L4.verified project under a BSD license. The C-to-Isabelle parser reads C99 files into the theorem prover Isabelle/HOL and provides the basis for their formal verification. |
| 2011-06-02: NICTA and secunet work together to deliver highly secure computing |
| 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. |
| 2011-05-02: SSRG students win design competition. |
|
SSRG students Etienne Le Sueur, Bernard Blackham, Martin Pflauminger and Aaron Carroll have won the 2011 Lantronix XPort Pro Design Contest with their e4Meter. |
| 2011-01-27: Verified seL4 kernel released. |
|
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. |
| 2010-11-04: One Billion L4-powered phones |
|
Open Kernel 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. |
| 2010-11-02: vNUMA source released |
| 2010-10-29: Paper accepted for ASPLOS |
|
A paper titled Improved device driver reliability through hardware verification reuse has been accepted for publication in the 16th ASPLOS Conference. The paper is the result of a collaboration with Intel (Hillsboro, OR) lead by SSRG researcher Leonid Ryzhyk. |
|
A further 150K external funding was approved for AURIN/HTS project to integrate HTS data on the national map |
|
A further 150K external funding was approved for AURIN/HTS project to integrate HTS data on the national map |