We are pleased to announce the availability of a new Galois tech talk video: “abcBridge: Functional interfaces for AIGs and SAT solving”, presented by Edward Z. Yang . More details about the talk are available on the announcement page.

abcBridge: Functional Interfaces for AIGs & SAT Solving from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

We are pleased to announce the availability of a new Galois tech talk video: “Computers As We Don’t Know Them”, presented by Christof Teuscher. More details about the talk are available on the announcement page.

Computers As We Don’t Know Them from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

abcBridge: Functional interfaces for AIGs and SAT solving (slides, video)

presenter:

Edward Z. Yang

time:

10:30am, Tuesday, 24 August 2010

location:

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

abstract:

SAT solvers are perhaps the most under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NP-complete problems in time for lunch, and there are many, many practical problem domains which involve NP-complete problems. However, a major roadblock to using a SAT solver in your every day routine is translating your problem into SAT, and then running it on a highly optimized SAT solver, which is probably implemented in C or C++ and not your usual favorite programming language.

This talk is about the use, design and implementation of abcBridge, a set of Haskell bindings for ABC, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC looks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs), are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.

bio:

Edward Z. Yang is an undergraduate studying computer science at MIT. He has been interning at Galois over the summer and enjoying every second of it. His interests include blogging, functional programming and practical applications of computer science research. You can read his blog at http://blog.ezyang.com/

Galois is pleased to announce a new white paper entitled High Assurance Software Development, written by David Burke, Joe Hurd and Aaron Tomb.

The purpose of this paper is describe how to make software assurance a part of a science of security. Software assurance as practiced is a grab-bag of techniques, heuristics, and lessons learned from earlier failures. Given the importance of software to critical infrastructures (electricity, banking, medicine), this is an untenable situation; the smooth functioning of our society depends on this software, and we need a more rigorous foundation for assessments about the trustworthiness of these systems.

In this paper we present an evidence-based approach to high assurance, in which diverse development teams can communicate in a common language to tackle the challenges of developing secure systems. Furthermore, this framework supports formal inference techniques (in particular, a trust relationship analysis), so that we can use automated reasoning to deal with scalability issues. Perhaps most importantly, an evidence-based approach lets us tailor the tools that we bring to bear on each claim: formal methods: testing; configuration management; and so forth all have their place in an assurance argument. In the end, it’s all about deploying systems where the residual risk has been minimized, given finite resources and time. Understanding this and managing it effectively is what the science of security is all about.

We are pleased to announce the availability of a new Galois tech talk video: “Developing Good Habits for Bare-Metal Programming”, presented by Mark Jones. More details about the talk are available on the announcement page.

Developing Good Habits for Bare-Metal Programming from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

titie:

Computers As We Don’t Know Them (slides, video)

speaker:

Christof Teuscher, PhD

Department of Electrical and Computer Engineering

Portland State University

time:

10:30am, 17 August 2010

location:

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

abstract:

Since the beginning of modern computer science some sixty years ago, we are building computers in pretty much the same way. Silicon transistor electronics serves as a physical device, the von Neumann architecture provides a computer design model, while the abstract Turing machine concept supports the theoretical foundations. However, in recent years, unimagined computing devices have seen the light because of advances in synthetic biology, nanotechnology, material science, and neuroscience. Many of these novel devices share the following characteristics: (1) they are made up from massive numbers of simple, stochastic components which (2) are embedded in 2D or 3D space in some disordered way. A grand challenge in consists in developing computing paradigms, design methodologies, formal frameworks, architectures, and tools that allow to reliably compute and efficiently solve problems with such devices. In this talk, I will outline my visionary and long-term research efforts to address the grand challenge of building, organizing, and programming future computing machines. First, I will review exemplary future and emerging computing devices and highlight the particular challenges that arise for performing computations them. I will then delineate potential solutions on how these challenges might be addressed. Self-assembled nano-scale cellular automata (CAs) and random boolean networks (RBNs) will serve as a simple showcase. I will also present the efforts underway to self-assemble massive-scale nanowire-based interconnect fabrics for spatial computers and what the challenges are in terms of computations and communication in such a non-classical system.

bio:

Christof Teuscher currently holds an assistant professor position in the Department of Electrical and Computer Engineering (ECE) with joint appointments in the Department of Computer Science and the Systems Science Graduate Program. He also holds an Adjunct Assistant Professor appointment in Computer Science at the University of New Mexico (UNM). Dr. Teuscher obtained his M.Sc. and Ph.D. degree in computer science from the Swiss Federal Institute of Technology in Lausanne (EPFL) in 2000 and 2004 respectively. His main research interests include emerging computing architectures and paradigms, biologically-inspired computing, complex & adaptive systems, and cognitive science. Teuscher has received several prestigious awards and fellowships. For more information visit: http://www.teuscher-lab.com/christof

Galois, Inc., a Portland, Oregon computer science R&D company, has been awarded two 2010 Phase I SBIR research awards, and one 2010 Phase 2 award from the US Department of Energy Office of Advanced Scientific Computing Research, to conduct research into high performance computing infrastructure.

A Deployable, Robust File System for Parallel I/O

When considering high-performance parallel computers, it is easy to overlook the importance of disk storage. In this research, Galois will address the topic of disk storage for parallel computers, and create a deployable, robust file system that will reduce downtime due to faults and increase productivity through improved system performance. Galois’ will take a synthesis approach, combining several strands of existing research on the subject of file systems and transitioning it into a robust, fully-featured product. In doing so, we will utilize modern formal methods research, in the form of model checking, to validate our design and improve the reliability of our implementation. The benefits of this research will be to improve the efficiency and decrease the cost of large, parallel file systems. This work will be applicable to Department of Energy laboratories, as well as to commercial users of massive parallel or distributed storage, such as online storage and backup providers or grid storage providers.

This project builds on Galois’ experience with industrial model checking, and our prior work on file system design and implementation via formal methods.

Improved Symbol Resolution for Portable Build Systems

Modern High Performance Computing utilizes a variety of different hardware and software platforms. These differences make it difficult to develop reusable components, which leads to a significant decrease of productivity. This project will investigate the design of portable build systems that are simple, yet sufficiently robust with respect to symbol resolution, so that they are able to adapt and build software across many different platforms. This project will result in increased productivity for software developers who design portable software components. In particular, we anticipate significant benefits in the area of High Performance Computing, where the multitude of different hardware and software platforms make the problem of reusing software particularly acute.

This work takes advantage of Galois’ background in domain specific language design, and build systems, in particular, Cabal, and other system configuration software.

Collaboration and Sharing on the Grid

The goal of the “Grid 2.0″ project is to improve the ability of a distributed team of researchers to collaborate on research using grid middleware computing infrastructure. In Phase I of this project, we developed a prototype integration of a typical collaboration-oriented web application with an open source data grid middleware system, establishing that such integration is feasible. In Phase II, we directly address the weakest point for collaboration applications on grid systems: open, standardized protocols for identity management, authorization, and delegation on the grid, via a federated identity management system providing support for software authorization and delegation on the Open Science Grid. The intent is to provide a secure, open, and flexible identity management system for use on grid infrastructure projects, portable to other grid middleware systems, and interoperable with existing identity management schemes. The open source results of the research will form the basis for applications of identity management systems in commercial cloud and grid systems.

This project builds on Galois’ experience with cross-domain collaboration tools and secure identity management systems (including OpenID, OAuth, SAML and X.509) developed for several clients over the past decade.

For more information about these projects, contact Don Stewart (dons@galois.com).

We are pleased to announce the availability of a new Galois tech talk video: “PReach – A Distributed Murphi-Based Model Checker”, presented by John Erickson. More details about the talk are available on the announcement page.

PReach – A Distributed Murphi-Based Model Checker from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

We are pleased to announce the availability of a new Galois tech talk video: “Requirement and Performance of Data Intensive, Irregular Applications”, presented by John Feo. More details about the talk are available on the announcement page.

Requirement and Performance of Data Intensive, Irregular Applications from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

Galois is pleased to host the following tech talk.  These talks are open to the interested public.  Please join us!

title:

Industrial Strength Distributed Explicit Model Checking

presenter:

John Erickson

time:

10:30am,  August 3rd, 2010

location:

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

Abstract:

We present PReach, an industrial strength distributed explicit state model checker based on Murphi. The goal of this project was to develop a reliable, easy to maintain, scalable model checker that was compatible with the Murphi specification language. PReach is implemented in the concurrent functional language Erlang, chosen for its parallel programming elegance. We use the original Murphi front-end to parse the model description, a layer written in Erlang to handle the communication aspects of the algorithm, and also use Murphi as a back-end for state expansion and to store the hash table. This allowed a clean and simple implementation, with the core parallel algorithms written in under 1000 lines of code. This talk describes the PReach implementation including the various features that are necessary for the large models we target. We have used PReach to model check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published for a distributed explicit state model checker. PReach has been released to the public under an open source BSD license.

bio:

John Erickson is a Design Engineer at Intel Hillsboro.  He graduated with his PhD in Computer Science from The University of Texas at Austin in 2008.  Currently he is working on the validation of uncore components in a 50+ core processor using a variety of formal and dynamic techniques. Past research interests include theorem proving with a focus on lemma generation and generalization in the context of induction.