Galois' Open-Source Projects on GitHub

Galois is pleased to announce the movement of our open source projects to GitHub!

As part of our commitment to giving back to the open source community, we have decided that we can best publish our work using GitHub's public website. This move should provide the open source community more direct access to our repositories, as well as more advanced collaboration tools.

Moved repositories include the widely-used XML and JSON libraries, our FiveUI extensible UI Analysis tool, our high-speed Cereal serialization library, our SHA and RSA crypto packages, the HaLVM, and more.

For a list of our open source packages, please see our main GitHub page here:

We are very excited to interact with the GitHub community and utilize all the great tools there. On the other hand, if you're not a GitHub user, please feel free to continue to send us any patches or suggestions as per usual.

For those currently hacking on projects using our old repositories at, we apologize for the inconvenience! The trees on GitHub hold the exact same trees, however, so you should be able to add a remote tree (git remote add) and push without too much difficulty.

As always, we would love to hear your feedback. Been waiting for this change? Hate it? Wonder how to push your changes to us? Please email us at


FiveUI: Extensible UI Analysis in your browser

Galois is excited to announce the Open-Source release of FiveUI!

FiveUI is a framework and tool for checking web-based user interfaces against codified UI guidelines. It is the first step towards an extensible, semantically aware, reusable and pragmatic toolchain for checking aspects of user interfaces against arbitrary guidelines.

FiveUI currently works as a browser extension for Google Chrome and Mozilla Firefox, but we are hard at work on a batch system for running guidelines in a non-interactive, headless environment, such as the Jenkins continuous integration system. For now, you can load FiveUI in your browser and navigate around web sites by hand. We think it's a pretty useful tool, as-is, even if you still have to do some clicking to trigger guidelines that check web pages.

The real strength of FiveUI is its extensibility. Anyone can encode guidelines as rules and rulesets, which are just literal javascript objects (much like JSON; in fact, they would be JSON, but rules require actual functions). Once you've written a set of rules, we would love it if you would add them to the growing collection of rule sets available for FiveUI. Because guidelines are general-purpose, the rules should be written to apply to any web site. This makes it trivial to take collections of rules and run them on any web page or web app you create, any rules you share can be used by others, and you'll be able to take advantage of the rules contributed by everyone else as well.

Take a look at the Install Guide, the Getting Started guide and the FiveUI Prelude to learn more about using and writing Rules and Rule Sets.

Last, but not least, let us know what you think! Send comments, email us, submit pull requests and file issues. We're listening for everything, and we'll do everything we can to make the tool and the community work for you.


HTML5 is Paving the Way for Semantically Aware Tools

Rich semantics are the Holy Grail for automated analysis tools; combined with extensible, familiar, and reusable tools and techniques we can seriously cut the costs associated with robust user interface development and testing.

Previously, we discussed the set of tools available for validating and linting HTML5-based user interfaces; (eg: the  W3C, numerous HTML/CSS editors, and tools like  HTML Lint). These tools help to identify syntactic issues, but what else is possible? The syntactic (and limited semantic) checks that these tools perform are necessary, but they aren't sufficient to cover the body of intricate failures that can occur while creating the rich user experiences we've come to expect from interactive web applications and mobile devices. Linters and Validators can't, for example, find bugs relating to the visual layout, and with good reason: Checking a UI is hard; it's repetitive, monotonous, and more importantly, subjective work.

However, there is still room for improvement. Surely we can push the envelope to do more. What's next, and how can we automate tasks that still challenge human analysts?

The first important insight is that many general guidelines for creating a good user interface have quantitative approximations. For example, the Windows 7 guidelines state:

Use title-style capitalization for titles, and sentence-style capitalization for all other UI elements.


Write the label as a phrase or an imperative sentence, and use no ending punctuation.

In the words of Richard Anderson: We have the technology! Which brings us to the first of a few key areas or techniques that could improve the tools that help ensure UI Consistency.

Click to read more ...


Tech talk video: Efficient Implementation of Property Directed Reachability

We are pleased to announced the availability of a new tech talk video, Alan Mishchenko talking about an efficient implementation of a novel model checking technique. For more information, please visit the talk announcement page.

For more Galois tech talk videos, please visit our Vimeo channel.


Tech Talk: Efficient Implementation of Property Directed Reachability 

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.)

Please note the unusual date and time for this talk, it is on Monday, 6 February 2012, at 10am.

title: Efficient Implementation of Property Directed Reachability

speaker: Alan Mishchenko

time: Monday, 6 February 2012, 10:00am

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


Last spring, in March 2010, Aaron Bradley published the first truly new bit-level symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it.

Relevant links: the paper, slides for the talk.

bio: Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998. Currently, Alan is an Associate Researcher at University of California, Berkeley. His research interests are in developing computationally efficient methods for logic synthesis and verification.