FMCAD Conference in Portland, OR: October 20 - 23, 2013

This year's Formal Methods in Computer-Aided Design (FMCAD) conference is being held from October 20 - 23 here in Portland, OR. Galois is proud to be one of the sponsors of this annual event - we're excited to be having it in our own back yard!

Dr. Lee Pike is on the program committee, and he's also giving a keynote address at the co-located MEMOCODE conference on October 18.

We hope to see folks there!


Lee Pike Giving Keynote at MEMOCODE

For those registered to attend MEMOCODE 2013 this week in Portland, OR, Dr. Lee Pike will be presenting the keynote address titled "Building a High-Assurance Unpiloted Air Vehicle" on October 18 at 11:00 a.m.


A drone autopilot is a complex software artifact that includes operating systems, networking, and sensor systems.  With support from DARPA, Galois is addressing the challenge of building an open-source high-assurance autopilot that is resistant to security attacks and software faults.  We are tackling the problem by borrowing from a suite of formal-methods-inspired technologies such as strongly-typed domain-specific languages for embedded control systems, software model-checking, and runtime-verification.

Just over one year in, we have designed two new languages and compilers and have a provisional autopilot developed.  I will describe how we have achieved low-cost high-assurance software, the challenges ahead, and the open problems we do not yet know how to address.

The autopilot and more information is available at


2013 Bike Commute Challenge

Our area's local Bike Commute Challenge is held annually in September. Hundreds of companies and individuals in Oregon and southwest Washington participate in the friendly competition.

Galois had a 32.85% commute rate, down just a little bit from last year's company record, but pretty good considering Portland in 2013 saw its rainiest September ever. To put our commute rate in context, here are our past numbers:

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

Despite the slightly lower commute rate, Galois placed 16th this year, ahead of last year's 21st-place finish, which serves as evidence that the wet weather took a toll on this year's participation.

Galois encourages public and active transportation by providing bike racks and a shower room in our office. Our location is located directly on Portland's light-rail line and is easily reachable by several bike-friendly routes.


SMACCMPilot: Open-Source Autopilot Software for UAVs

As part of DARPA's High Assurance Cyber Military Systems (HACMS), Galois is building critical flight control software using new software methods for embedded systems programming. Recently, Signal Online reported an overview of the HACMS program. We've been working on the HACMS program for about a year and we'd like to share more details about open source work we've done so far.

The flagship application for the technologies we've developed under the HACMS program is called SMACCMPilot: a new flight controller for small quadcopter unmanned aerial vehicles (UAVs). SMACCMPilot is written in the Ivory language, a new domain-specific language for safe systems programming. We've built an ecosystem of libraries on top of the Ivory language, including a concurrency framework and drivers for microcontroller hardware. Ivory has a simple interface to external C code, which allows SMACCMPilot to re-use software components from the ArduCopter open source project. We've also implemented communications protocol stacks and control primitives in Ivory. SMACCMPilot is currently alpha-quality software as we actively develop the flight control software itself and evolve the new technologies we've used to build it. We'll be continuing work on the SMACCMPilot project for the next few years. 

All of the software behind SMACCMPilot is open source and available on Galois's github, and documented on the project web site. We welcome collaboration with programming languages, formal methods, and flight control researchers!

For more information, contact Lee Pike and Pat Hickey.


Automated Tools for Binary Analysis & Optimization

Galois was awarded a contract through the Office of Naval Research - we're partnering with SRI to build automated tools for binary analysis and optimization to minimize software bloat and reduce costs and complexity. Read more about the effort here: