We are pleased to announce the availability of a new Galois tech talk video: “Trust relationship modeling for software assurance”, presented by John Launchbury. This talk is an in-absentia presentation to the FAST 2010 audience.
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.
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.
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/
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.
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
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.
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.
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.
We are pleased to announce the availability of a new Galois tech talk video: “Large-Scale Static Analysis at Mozilla”, presented by Taras Glek.Slides and more details about the talk are available on the announcement page.
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.