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.
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.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title:
Large-Scale Static Analysis at Mozilla (slides, video)
presenter:
Taras Glek
time:
10:30 am, 8 June 2010, Tuesday
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
A competitive browser market requires fast-paced improvements to the codebase. Such improvements may require significant refactoring of large parts of the codebase. Mozilla Firefox is one of the largest open source C++ projects. Unfortunately C++ is a complex language: method overloading, virtual functions, template instantiation, pointer arithmetic, etc reduce developer productivity. Mozilla developed C++ static analysis and refactoring tools to increase developer leverage in C++. Static analysis is done via Dehydra/Treehydra GCC plugins and refactoring is accomplished by extending the Elsa C++ parser. This talk will discuss why Mozilla needs static analysis, why there are so few tools for C++, and specific projects that we’ve embarked on.
bio:
Taras Glek is a software engineer at Mozilla Corporation. He works on static analysis and startup performance. Taras blogs about it at http://blog.mozilla.com/tglek/.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!IMPORTANT: Please note that this talk is Thursday.
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Category theory is a powerful language for organizing layers of abstraction in all areas of mathematics. Databases are powerful tools for organizing information of all sorts. Whereas categories are often considered hopelessly abstract, databases are often considered horrifically mundane. Thus it is either strange or fitting that, mathematically speaking, categories and databases are the same concept. In this talk I’ll show how to turn any database into a category and any category into a database. I’ll also discuss functors and how they may be useful for issues of data migration and merging.
bio:
David Spivak graduated with a PhD in mathematics from UC Berkeley in 2007; his thesis used higher category theory to fix an old problem in geometry. From 2007 to the present, he have been a postdoc at the University of Oregon in the Math Department. During this time, his focus has moved toward the idea of using category theory to understand information and communication. This summer, he will become a mathematics postdoc at MIT for three years, focusing on information and communication from a category-theoretic perspective.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
IMPORTANT: Please note that this talk is Monday.
title:
The L4.verified Project
presenter:
Dr. Gerwin Klein
time:
10:30 am, 24 May 2010, Monday
location
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.
bio:
Dr Gerwin Klein is a Principal Researcher at NICTA and Conjoint Associate Professor at the University of New South Wales, Australia. He is working in the area of formal software verification, interactive theorem proving, and operating systems. He is the project leader of L4.verified. He received his PhD in 2003 from Technische Universitaet Munich on the topic of Java Bytecode Verification and has been working in the area of machine-checked formal proof in various projects since 1998.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title
Developing Good Habits for Bare-Metal Programming (slides, video)
presenter
Mark Jones
High Assurance Systems Programming Project (HASP)
Portland State University
time
10:30am, Tuesday, 18 May 2010
location
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract
Developers of systems software must often deal with low-level and performance-critical details that are hard to address in high-level programming languages. As a result, much of the systems software that is produced today is written in languages like C and assembly code, without the benefit of more expressive type systems or other features from modern functional programming languages that could help to increase programmer productivity or software quality. In this talk, we present an update on the status of Habit, a dialect of Haskell that we are designing, as part of the HASP project at PSU, to meet the needs of high assurance systems programming. Among other features, Habit provides: mechanisms for fine control over representation of bit-level and memory-based data structures; strong support for both functional and imperative programming; and a flexible type system that allows precise characterization of size and bound information via type level naturals, as well as termination properties resulting from the use of unpointed types.
bio
(from http://web.cecs.pdx.edu/~mpj/)Mark Jones is a Professor in the Department of Computer Science in the Maseeh College of Engineering & Computer Science at Portland State University in Portland, Oregon, USA. His interests include all aspects of programming language design, implementation, and application. He is particularly interested in the use of advanced programming language technologies for systems programming, and in the development and application of expressive type and module systems that support the construction and certification of secure and reliable software systems.
Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!The talk will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
Typing DirectoriesDetails:
Presenter: Kathleen Fisher, AT&T Labs
Date: Monday May 03, 2010
Time: 3:30pm (NOTE THE CHANGED DATE AND TIME!)
Abstract: PADS describes the contents of individual ad hoc data files, but has no provisions for describing collections of files, i.e., directories. In this talk, I explore examples where having a declarative description of directories as well as files would be useful, including websites, source code trees, source code control systems, operating systems, and scientific data sets. As part of this exploration, I identify essential features of a directory description language and useful tools that might be produced from such a description. I end with a series of questions about how such a language might most easily be implemented in the context of Haskell.This is joint work with David Walker and Kenny Zhu.Bio: (from http://www.research.att.com/people/Fisher_Kathleen_S) Kathleen Fisher is a Principal Member of the Technical Staff at AT&T Labs Research and a Consulting Faculty Member in the Computer Science Department at Stanford University. Kathleen’s research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data, including the Hancock system for efficiently building signatures from massive transaction streams and the PADS system for managing ad hoc data.Kathleen is an ACM Distinguished Scientist. She has served as program chair for FOOL, CUFP, and ICFP. She is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), Co-Chair of CRA’s Committee on the Status of Women (CRA-W), and an editor of the Journal of Functional Programming. She is currently serving on the CRA Board.
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.