Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   title:  Verifying seL4-based Systems   presenter: Simon Winwood   time: Tuesday, 01 February 2011, 10:30am   location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)   abstract:   In […]

We are pleased to announce the availability of a new Galois tech talk video: “Program Inconsistency Detection using Weakest Preconditions”, presented by Aaron Tomb.  More details about the talk are available on the announcement page. Program Inconsistency Detection using Weakest Preconditions from Galois Video on Vimeo. For more videos, please visit http://vimeo.com/channels/galois.

Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers — extensions to SAT solvers with support for variables of non-boolean type — offer powerful automation for solving a variety of assurance […]

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   title: Program Inconsistency Detection using Weakest Preconditions   presenter: Aaron Tomb   time: Tuesday, 25 January 2011, 10:30am   location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)   abstract:  Many tools […]

We are pleased to announce the availability of a new Galois tech talk video: “Control Flow Graph-guided Exploration in DDT”, presented by Rebekah Leslie.  More details about the talk are available on the announcement page. Control Flow Graph-guided Exploration in DDT from Galois Video on Vimeo.   For more videos, please visit http://vimeo.com/channels/galois.

Isaac Potoczny-Jones February 18, 2014: This project has recently been spun-out into a new startup company, Tozny – read more about this world-class, secure login technology at www.tozny.com. Introduction In this blog post, we propose an authentication scheme using QR codes and Internet-connected smart phones to allow a user to quickly sign into a web site without having […]

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!   title: Control-flow Graph Guided Exploration in DDT   presenter: Rebekah Leslie   time: Tuesday, 11 January 2011, 10:30am   location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA3rd floor of the Commonwealth building) […]

Galois has been selected by AFRL/OSD for a Phase I Small Business Innovative Research (SBIR) award to develop countermeasures against malicious hardware. In this project, Galois will address the class of hardware threats known as “deterministically triggered trojans”, and develop tools that inhibit malicious hardware activation by applying attack incompatibility techniques.   This effort builds […]

Performing consistent builds is critical in software development, but the current system in GHC/Haskell of per-user and per-system GHC package databases interferes with this need for consistency. It is difficult to precisely identify the dependencies of a given project, and changes necessary to enable one project to build may render another project inoperable. If each […]

Copilot is an embedded domain-specific language designed by Galois, that allows you to generate assured, embedded C code from programs written essentially as Haskell lists (using Atom as a backend for the C code generation).  Lee Pike has written a tutorial on how to use Copilot to program an Arduino controller to play “Jingle Bells”. Read the full tutorial on […]