Tech Talk: Automatic Function Annotations for Hoare Logic

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: Automatic Function Annotations for Hoare Logic

speaker: Daniel Matichuk

time: Tuesday, 12 February 2013, 10:30am.

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

abstract:

Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a side-condition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning.

bio:

Daniel Matichuk obtained his B.Sc. in Honors Computer Science from the University of Alberta, Canada in 2011 and has since been working at NICTA in Sydney as a Research Engineer. He will soon be starting his PhD at NICTA and the University of New South Wales. His recent work was aiding in the noninterference proof for the seL4 microkernel and he is interested in maintenance and refactoring in large formal proofs.

Tech Talk: Computers and privacy, ACLU of Oregon discusses their 2013 agenda

(There is no need to pre-register for the talk.)

title: Computers and privacy, ACLU of Oregon discusses their 2013 agenda

speaker: Becky Straus

time: Tuesday, 4 December 2012, 10:30am.

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

abstract:

Efforts at the federal level to pass laws like the Stop Online Piracy Act (SOPA) and the Cyber Intelligence Sharing and Protection Act (CISPA) have attracted widespread attention and criticism, and rightly so. But Washington, D.C. is far from the only place that officials are making decisions that impact the privacy and free speech rights. State and local officials are jumping into the fray as well, passing laws or creating policies that have immediate impact without the spotlight that accompanies federal action. The fact is that privacy laws have failed to keep up with emerging technologies. This presentation will survey several areas where state and local officials in Oregon have recently been active, including reviewing policies on automated license plate recognition, surveillance cameras, and use of domestic drones. We will discuss how the ACLU of Oregon has been involved and what is on our agenda for the upcoming 2013 state legislative session.

bio:

Becky Straus is the legislative director for the American Civil Liberties Union of Oregon. She joined the staff in 2011 and directs ACLU’s advocacy and lobbying efforts before the Oregon Legislature and coordinates ACLU testimony before public bodies on the full range of civil liberties and civil rights issues in Oregon. She is also ACLU’s primary lobbyist on City of Portland matters.

2012 Bike Commute Challenge

Galois once again participated in the annual September Bike Commute Challenge, which promotes biking to work via a friendly competition.

Galois had a 33.13% commute rate in September. 14 employees made 146 bike commutes for a total of about 1,400 miles. This year's commute rate is a company record:

• 2007: 17.1%
• 2008: 22.9%
• 2009: 15.2%
• 2010: 26.4%
• 2011: 29.1%
• 2012: 33.1%

According to the Commute Challenge's final results, Galois placed 21st out of 242 teams in the Business and Non-Profits with 25-99 Employees category.

The Galois offices are located in downtown Portland, OR, which Bicycling magazine named America's Best Bike City. Galois encourages use of public and active transportation by providing bike racks and a shower room in our office. Our location is directly on two of Portland's light-rail lines and only a couple blocks from two others.

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

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

abstract:
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.