Log in
Memory violations are a major cause of security breaches and operational flaws in today's software systems. Proving memory safety was traditionally a core challenge in program verification due to the high complexity of reasoning about pointer manipulations. Researchers at Queen Mary and Imperial jointly produced breakthrough algorithms for automatically reasoning about pointers, enabling highly-scalable automatic verification for industrial code. These techniques resulted in the industrial program analysis tool INFER developed by Monoidics Ltd, and used by customers across the world. The verification algorithms developed at Queen Mary and Imperial were also incorporated in Microsoft tools used to secure Windows device drivers.
Graph-theoretic and mathematically rigorous algorithmic methods developed at the University of Hertfordshire have improved the applicability of compiler technology and parallel processing. A compiler developed in the course of a ten-year research programme at the university has been successfully applied to a number of commercial problems by re-purposing the research tool. NAG Ltd has adapted the tool into a commercial product [text removed for publication]. Numerous applications of the mathematical methods (such as type-flow graphs used conjointly for correctness and optimisation) have been deployed by industry (including SAP, SCCH, German Waterways Board) working closely with the university.
Analytical Software Design (ASD), based on Communicating Sequential Processes (CSP) and the Failures Divergences Refinement tool (FDR), has been developed and patented by the specially created Dutch company Verum. The new software, based on research in the UoA, was released in 2009 and has allowed customers to build rigorous, error-free software systems automatically by specifying state machines. ASD, using FDR as its verification engine, has produced many millions of lines of verified code for customers including Philips Medical Systems, Ericsson, FEI and ASML, who typically report at least a 50% reduction in costs and a 90% reduction in errors.
The spin-out company CSM Ltd. was set up in 1991 to commercially develop Durham research on program transformation. Up until 1999, this company (which in the mid-90's became Durham Software Engineering Ltd. and subsequently Software Migrations Ltd.) and researchers at Durham University developed the FermaT Workbench: an industrial-strength assembler re-engineering workbench for program comprehension, migration and re-engineering. In 1999, Software Migrations Ltd. relocated to St. Albans and now has an extensive list of national and international clients. All its products (software and services) are built on the FermaT Workbench and has generated considerable revenue with this revenue strongly expected to rise steeply in the near future.
Teaching and learning of computer architecture has been enhanced using highly interactive simulations with carefully constructed visualisations and animations. Computer scientists need to understand and observe how different parts of a modern computer system's architecture and organization fit together, interact and support each other. Unique educational simulation software has been designed, developed and evaluated with these requirements in mind. Since the software and teaching materials have been made public, numerous universities worldwide adopted it in their courses with claimed positive impact on student engagement, course popularity, grades, speed of delivery of curriculum, attendance and peer recognition of best practice.
The development, review and acceptance of an explicit 'safety case' forms a key component of the assurance and regulation of many safety critical systems, including those in the nuclear, defence, railway, automotive, medical device, and process industries. Industrial practice in safety case development prior to York's development of the Goal Structuring Notation (GSN) relied almost exclusively upon narrative text to communicate the safety argument within the safety case. This approach suffered from problems of lack of clarity, difficulty in comprehension, poor structure, and limited formalised development of 'case law' in safety argumentation. GSN was developed and matured by York to tackle these problems directly, and is now used internationally by safety critical industries in a large number of domains including defence, transport, nuclear and medical devices.
From 2005, a body of research undertaken at the University of Essex has developed a novel debug support architecture for systems on a chip (SoC). This platform successfully addresses the challenge of debugging applications executing on SoCs with multiple processor cores. A system-centric architecture is used, which achieves substantial improvement in compression and requires dramatically less silicon real estate than existing state of the art applications. The research underpins `UltraDebug', which is commercialised via the spin-out `UltraSoC'. UltraSoC has attracted investment worth £5million (the majority coming from venture capital sources) and is currently working with PMC-Sierra to incorporate its innovative technology into PMC's next generation of storage controllers.
Results of research at Royal Holloway in Machine Learning — Support Vector Machine (SVM), kernel methods and conformal-prediction techniques — are at the source of the analytics and `Big Data' revolution, whose impact is transforming the economy (and society), from data mining to machine vision, from Web search to spam detection.
Although SVMs were not invented at Royal Holloway, our contributions include the original reference monograph (Vapnik 1998), basic underpinning theory (such as [3.2]), the first widely distributed open-source implementation [3.1], the first accessible textbook (Cristiniani and Shawe-Taylor 2000), and multiple extensions (such as [3.3] and [3.4]).
A spin-out company, Contemplate Ltd, is using advanced static analysis technology in global top-ten investment banks and other clients to discover previously undetected defects in enterprise-scale business-critical multi-threaded Java codebases. The impact is in terms of the benefits delivered to Contemplate's clients by this technology and in terms of the formation and growth of Contemplate as an employer and a successful business.
Impact: The underpinning research resulted in an innovative Worst-Case Execution time (WCET) analysis technology now called RapiTime, which was transferred to industry via a spin-out company, Rapita Systems Ltd. The technology enables companies in the aerospace and automotive industries to reduce the time and cost required to obtain confidence in the timing correctness of the systems they develop. The RapiTime technology has global reach having been deployed on major aerospace and automotive projects in the UK, Europe, Brazil, India, China, and the USA. Key customers include leading aerospace companies such as: [text removed for publication]; as well as major automotive suppliers: [text removed for publication]. Since 2008, Rapita has won export orders to China worth over [text removed for publication]. From 2008/9 to 2011/12, the company's annual revenues have more than doubled from [text removed for publication] to over [text removed for publication]. As of August 2013, Rapita employs [text removed for publication] people at its offices in York and Cambridge.