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.
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 PNNLDr. 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.
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
It seems obvious that the reliability of critical software can be improved by using high-level, memory-safe languages (Haskell, ML, Java, C#, etc.). But most existing implementations of these languages rely on large, complex run-time systems coded in C. Using such an RTS leads to a large “credibility gap” at the heart of the assurance argument for the overall system. To fill this gap, we are working to build a new high-assurance run-time system (HARTS), using an approach grounded in machine-assisted verification, with an initial focus on providing certifiably correct garbage collection.This talk will describe a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy’s Coq-certified Compcert compiler and Cminor intermediate language. We add a new intermediate language, GCminor, that supports GC’ed languages and has a proven semantics-preserving translation to assembly code. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the GHC’s Core intermediate language to GCminor. (This is joint work with Andrew McCreight and Tim Chevalier.)
bio:
Andrew Tolmach has been a faculty member at Portland State University since receiving his Ph.D.in Computer Science from Princeton in 1992. His current research interests, pursued under the aegis of the PSU High Assurance Systems Programming (HASP) project, focus on high-assurance systems software development, in particular using formal verification. His past publications, mostly about functional languages, include work on operating systems in Haskell, garbage collection, compilation, debugger implementation, integration with logic languages, and lazy functional algorithms.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title:
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
presenter:
Joe Hendrix
time:
10:30am, Tuesday, 22 June 2010.
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Many inductive theorem provers use induction schemes derived from the recursive calls in functions definitions. This widely-used strategy is called coverset induction in the context of algebraic specifications. One challenge in applying coverset induction is that it typically requires using a total recursive function, while many operations on data structures are only meaningful on some well-formed subset of their possible inputs.
In this talk, I’ll discuss a generalization of coverset induction to handle partial constructors and operations. The generalization is implemented in the Maude ITP, and used in an extensive case study involving powerlists — a data structure introduced by J. Misra to elegantly formalize parallel algorithms based on divide and conquer strategy. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about powerlists can be elegantly proven using the generalized coverset induction scheme implemented in the Maude ITP.
bio:
Joe is a member of the technical staff at Galois, Inc. He is interested in developing tools for making software development easier and safer. He started out developing software for civil engineers to analyze the safety of bridge foundations. He worked on automated decision procedures during his PhD at the University of Illinois. Immediately prior to joining Galois, he developed software within Microsoft’s Trustworthy Computing Initiative.
We are pleased to announce the availability of a new Galois tech talk video: “Databases are Categories”, presented by David Spivak. More details about the talk are available on the announcement page.
Orc is a concurrent scripting language, now available as an embedded DSL in Haskell. I like to think of Orc as the combination of three things: many-valued concurrency, external actions (effects), and managed resources, all packaged in a high-level set of abstractions that feel more like scripting rather than programming. It provides a very flexible way to manage multiple concurrent actions, like querying remote web sites, along with timeouts and default actions.Source code is available on Hackage; the easiest way to access it is with cabal (i.e. ‘cabal install orc’).Also available is a draft paper entitled Concurrent Orchestration in Haskell which explains how to use Orc, as well as describing the implementation in detail.Feedback welcome. Enjoy!
For a number of years, Galois Inc. has been organizing technical seminars presented by visiting researchers, Galois engineers, and members of the vibrant Portland technical community. The seminars span a wide variety of topics, ranging from functional programming, formal methods, and compiler and language design, to cryptography, and operating system construction. The talks are free and open to the interested public. Announcements of upcoming talks are posted to this blog about a week in advance.Over the last few months we have received a number of requests to share videos of the talks with the wider community. As a result, we are very pleased to announce the Galois tech talk channel on Vimeo. Recent Galois talks should become available over the next few weeks, followed by future presentations.Enjoy!Galois tech talk channel: http://vimeo.com/channels/galois
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of well-founded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort.
bio:
Eric is a member of the technical staff at Galois, Inc., where he holds roles in software design and development for projects focusing on secure collaboration and secure network protocols. He specializes in Haskell programming and in leveraging Haskell’s unique type-system to improve various network and web-focused interfaces.
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.