Entries in the “Tech Talks” category

Tech Talk Video: abcBridge: Functional interfaces for AIGs and SAT solving

August 27th, 2010 by Iavor S. Diatchki

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.

Posted in Formal Methods, Functional Programming, Haskell, Tech Talks, Video | Comments (0)

Tech talk video: Computers As We Don’t Know Them

August 23rd, 2010 by Iavor S. Diatchki

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.

Posted in Tech Talks, Technology, Video | Comments (1)

Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving

August 19th, 2010 by Iavor S. Diatchki

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/

Posted in Formal Methods, Functional Programming, Haskell, Open Source, Tech Talks | Comments (0)

Tech Talk Video: Developing Good Habits for Bare-Metal Programming

August 11th, 2010 by Iavor S. Diatchki

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.

Posted in Functional Programming, Haskell, Tech Talks, Technology, Video | Comments (0)

Tech talk: Computers As We Don’t Know Them

August 11th, 2010 by Iavor S. Diatchki

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

Posted in Tech Talks, Technology | Comments (0)

Tech talk video: PReach – A Distributed Murphi-Based Model Checker

August 9th, 2010 by Iavor S. Diatchki

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.

Posted in Formal Methods, Tech Talks, Technology, Video | Comments (0)

Tech Talk Video: Requirement and Performance of Data Intensive, Irregular Applications

August 3rd, 2010 by Iavor S. Diatchki

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.

Posted in Tech Talks, Technology, Video | Comments (0)

Industrial Strength Distributed Explicit Model Checking

July 27th, 2010 by Lee Pike

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.

Posted in Formal Methods, Misc, Tech Talks | Comments (0)

Galois Tech Talk Video: Large-Scale Static Analysis at Mozilla

July 9th, 2010 by Iavor S. Diatchki

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.

Large-Scale Static Analysis at Mozilla from Galois Video on Vimeo.

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

Posted in Community, Open Source, Tech Talks, Technology, Video | Comments (0)

Tech Talk: Requirements and Performance of Data Intensive, Irregular Applications

July 2nd, 2010 by Iavor S. Diatchki

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

Please note the unusual day for this talk: it is on Friday, 9 July 2010

title:

Requirements and Performance of Data Intensive, Irregular Applications (video)

presenter:

Dr. John Feo

time:

10:30am, Friday, 9 July 2010

location:

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

Abstract:

Many fundamental science, national security, and business applications need to process large volumes of irregular, unstructured data. Data collection and analysis is rapidly changing the way the scientific, national security, and economic communities operate. There are worldwide operational deployments of instruments to detect the proliferation of weapons of mass destruction, monitor terrorist cells, and track the movement of illicit goods and services. In the next 15 years 30% of battle-space defense forces will be autonomous with each advanced robotic device carrying dozens of sophisticated sensors collecting, processing, analyzing and transmitting large amounts of data. American economic competitiveness will depend increasingly on the timely analysis of many Petabytes of data collected in diverse computing clouds charting the social and economic behavior of consumers.

Unlike traditional scientific applications based on linear algebra routines, data analytic applications comprise large, integer-based graph computations with irregular data access patterns, low computation to memory access ratios, and high levels of fine grain parallelism that pass data and synchronize frequently. Traditional architectures optimized to run large-scale floating point intensive simulations are inadequate, and more suitable high-end architectures such as the Cray XMT are needed. In this talk I will discuss the programming language, tools, and system requirements for data analytic applications. I will survey the research at PNNL’s Center for Adaptive Supercomputer Software as regards graph analytics. In particular, I will present several key graph algorithms we have developed with an emphasis on structure, use of special hardware features, performance, and scalability.

bio:

Dr. John Feo is the director of the Center for Adaptive Supercomputer Software at the Pacific Northwest Laboratory. Dr. Feo received his Ph.D. in Computer Science from The University of Texas at Austin. He began his career at Lawrence Livermore National Laboratory where he managed the Computer Science Group and was the principal investigator of the Sisal Language Project. Dr. Feo then joined Tera Computer Company (now Cray Inc) where he was a principal engineer and product manager for the MTA-1 and MTA-2, the first two generations of the Cray’s multithreaded architecture. After a short two year “sabbatical” at Microsoft where he led a software group developing a next-generation virtual reality platform, he joined PNNL

Dr. Feo’s research interests are parallel programming, graph algorithms, multithreaded architectures, functional languages, and performance studies. He has published extensively in these fields. He has held academic positions at UC Davis and is an adjunct faculty at Washington State University.

Posted in Tech Talks, Technology | Comments (0)