Tech Talk: Towards a Formally Verified Component Platform

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Towards a Formally Verified Component Platform

speaker: Matthew Fernandez

time: Tuesday, 16 October 2012, 10:30am

Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.

bio: Matthew is a current PhD student at NICTA and the University of New South Wales, Australia. His research interests include kernel design, compilers, component systems and compiler implementation. His current work is aiming to provide formal guarantees for a component-based development environment on the seL4 microkernel.


Galois is hiring!

We are currently seeking software engineers/researchers to play a pivotal role in fulfilling our mission of creating trustworthiness in critical systems.

Galois engineers/researchers participate in one or more projects concurrently, and specific roles vary greatly according to skills, interests, and company needs. Your role may include technology research and development, requirements gathering, implementation, testing, formal verification, infrastructure development, project leadership, and/or supporting new business development.

Skills & Requirements

Education: Minimum of a Bachelor's degree in computer science or equivalent. MS or PhD in CS or a related field desirable but optional, depending on specific role.

Required Technical Expertise: Must have hands-on experience developing software and/or performing computer science research. Demonstrated expertise in aspects of software development mentioned above.

Desired Technical Expertise: Fluency in the use of formal or semi-formal methods such as Haskell or other functional programming languages. Direct experience in developing high assurance systems and/or security products. Experience with identity management, security risk analysis, systems software, or networking.

Required General Skills: Must work well with customers, including building rapport, identifying needs, and communicating with strong written, verbal, and presentation skills. Must be highly motivated and able to self-manage to deadlines and quality goals.

Our engineers/researchers develop in programming languages including functional languages, designing and developing advanced technologies for safety- and security-critical systems, networks, and applications. Engineers/researchers work in small team settings and must successfully interact with clients, partners, and other employees in a highly cooperative, collaborative, and intellectually challenging environment.

We’re looking for people who can invent, learn, think, and inspire. We reward creativity and thrive on collaboration. If you are interested, please send your cover letter and resume to us at careers@galois.com.


Galois at ICFP 2012


Fill the Bike Racks Day

The Galois office is home to 18 bike racks, about one for every two employees. Tuesday, September 18 was Fill the Bike Racks Day. We didn't fill all the racks, but we still had 15 employee cycles gracing the office today.

Fill the Bike Racks Day was scheduled in September to complement the annual Bike Commute Challenge.


Tech Talk Video: Comprehensive Analysis of the Android Ecosystem

We are pleased to announce the availability of a new tech talk video: "Comprehensive Analysis of the Android Ecosystem", presented by Iulian Neamtiu. For more details, please visit the talk announcement page.

For more videos, please visit our Vimeo channel.