The July 28th Galois Tech Talk will be delivered by Joe Hurd, titled “Mathematics of Cryptography: A Guided Tour.”

• Date: Tuesday, July 28th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building), Portland, OR 97204

Slides are now available.

Abstract:

In this informal talk I’ll give a guided tour of the mathematics underlying cryptography. No prior knowledge will be assumed: the goal of the talk is to demonstrate how simple mathematical concepts from algebra and number theory are used to build a wide range of cryptographic algorithms, from the familiar (encryption) to the exotic (zero knowledge proofs).

Bio:

Joe Hurd is a Formal Methods Engineer at Galois, Inc. He completed a Ph.D. at the University of Cambridge on the formal verification of probabilistic programs, and his work since has included: developing a package management system for higher order logic theories; applying automatic proof techniques for first order logic; and creating the world’s first formally verified chess endgame database.

The July 7th Galois Tech Talk will be delivered by Ivan Sutherland, titled “The Fleet Architecture”

• Date: Tuesday, July 7th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Slides are now available.Abstract: This talk describes a radically different architecture for computing called Fleet. Fleet accepts the limitations to computing imposed by physics: moving data around inside a computer costs more energy, more delay, and more chip area than the arithmetic and logical operations ordinarily called “computing.” Fleet puts the programmer firmly in charge of the most costly resource, communication, instead of in charge of the arithmetic and logical resources that are now almost free. Fleet treats arithmetic and logical operations as side effects of where the programmer sends data.Fleet achieves high performance through fine grain concurrency. Everything Fleet does is concurrent at the lowest level; programmers who wish sequentiality must program it explicitly. Fleet presents a stark contrast to today’s multi-core machines in which programmers seek concurrency in an inherently sequential environment.The Fleet architecture uses a uniform switch fabric to simplify chip design. A few thousand identical copies of a programmable interface connect a thousand or so repetitions of basic arithmetic, logical, input-output, and storage units to the switch fabric. The uniform switch fabric and its identical programmable interfaces replace many of the hard parts of designing the computing elements themselves.Both software and FPGA simulators of a Fleet system are available at UC Berkeley. Berkeley students have written a variety of Fleet programs; their work helped to define what the programmable interface between computing and communication must do. A simple compiler now produces the programs required at source and destination to provide flow-controlled communication. We expect work on a higher-level language to appear soon as a PhD dissertation.A recent 90 nanometer TSMC test chip, called Infinity, demonstrated switch fabric performance at about 4 GHz. A new test chip, called Marina, has just gone out for fabrication. Marina will test the programmable interface, and if successful, will give us confidence to build a complete Fleet. We seek participation from sponsors, programmers, and designers of basic computation elements.Bio: Ivan Sutherland is a Visiting Scientist at Portland State University where he and Marly Roncken have recently established the “Asynchronous Research Center” (ARC). The ARC occupies both physical and intellectual space half way between the Computer Science (CS) and Electrical and Computer Engineering (ECE) departments at the university. The ARC seeks to free designers from the tyranny of the clock by developing better tools and teaching methods for design of self-timed systems. Prior to moving to Portland, Ivan spent 25 years as a Fellow and Vice President at Sun Microsystems. A graduate of Carnegie Tech, Ivan got his PhD at MIT in 1963 and has taught at Harvard, University of Utah, and Caltech.Dr. Sutherland received the 1988 Turing Award, for his pioneering work in the field of computer graphics.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The June 30th Galois Tech Talk will be delivered by Brian Huffman, titled “Verifying Stream Fusion with Isabelle/HOLCF”

• Date: Tuesday, June 30th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Slides from the talk.Abstract: Stream fusion is a system for removing intermediate data structures from Haskell programs that manipulate lists.  Formal verification of such libraries requires very precise modeling in a theorem prover, to avoid strictness-related bugs.In this talk I will present a formalization of the stream fusion library in Isabelle/HOLCF, a theorem proving environment designed especially for reasoning about functional programs.  I will show how to prove the correctness of various stream functions using “fixed-point induction”, a powerful reasoning principle for general recursive functions.Bio: Brian Huffman is a PhD student in Computer Science at Portland State  University, working with advisor John Matthews. He studies formal reasoning with  the Isabelle theorem prover, specializing in formalized mathematics and semantics of functional languages. He is currently the maintainer of Isabelle/HOLCF, a logic for domain theory.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The June 23rd Galois Tech Talk will be delivered by John Launchbury, titled “A Newbie’s Exploration of Separation Logic.”

• Date: Tuesday, June 23rd, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: I was just privileged to be in a Separation Logic Tutorial, given by its inventor, John Reynolds. Separation logic allows descriptions of storage and other resources concisely, providing a novel system for reasoning about imperative programs with shared mutable data structures. Recent years have seen a flurry of activity in Separation Logic, extending it to apply from shared-variable concurrency to permission based access control mechanisms. In this informal chalk-talk I will introduce the basics of Separation Logic, providing an overview of the fundamental notions of proof techniques.Bio: John Launchbury is the CTO of Galois, Inc. Prior to founding Galois in 1999, John conducted research and instructed in Computer Science and Engineering at the Oregon Graduate Institute School of Science and Engineering at OHSU. John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society’s distinguished dissertation prize.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The June 16th Galois Tech Talk will be delivered by Trevor Elliott, titled “Orc in Haskell.”

• Date: Tuesday, June 16th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: Concurrency is difficult to realize successfully. The Orc language tackles this problem by introducing explicit concurrency as part of its core. It presents a clean, and somewhat monadic, style of programming that should look familiar to Haskell users. I will give a quick introduction to the Orc language, using several examples to motivate its use. Following this introduction, a monadic Haskell embedding of the major features will be presented, bringing a type system to Orc.Bio: Trevor Elliott is a member of the technical staff at Galois, Inc.  His interests center around functional programming, and the effective use of type systems.Slides are available for download.Update: the source is now available on Hackage (though changed from the version presented at this talk).

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The April 21st Galois Tech Talk will be delivered by Louis Testa, titled “Growing Software.”

• Date: Tuesday, April 21st, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: Many small software product companies start out with a technical guru who is “promoted” to the VP of engineering. Success as the head of software development depends on skills that the technical expert may not have learned. In this new role, the newly minted manager reports to the CEO, is on the executive team, has to understand and drive the overall business strategy, defines the product, works directly with customers, and still has to manage individual software developers. I wrote Growing Software to offer advice to this new manager; it covers the advice I would have appreciated when I started out as a new manager.As Growing Software covers the spectrum of topics that the small company development manager needs to know, there are too many topics to cover in one talk. This talk will provide an overview of the book, and then focus on selected topics:

• Managing a Development Team
• Product Definition
• Technology Review
• Project Management
• Internationalization

Bio: Louis Testa has a 30 year high technology career having worked for many small software companies spanning many industries: Financial, Training, Medical, Construction, Electronics Design, Electronics Test, and Integrated Circuit. He has worked as a researcher, programmer, integrated circuit designer, and has been a senior engineering manager (VP/Director) at 6 different small companies. He currently holds several software patents and has written technical papers for conferences in the U.S. and in overseas. His first book, Growing Software, was published by No Starch Press in March 2009.Louis earned his MS degree from University of California Berkeley and his BS in Engineering from California Institute of Technology (Caltech).

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The April 2nd Galois Tech Talk  will be delivered by Daniel J. Quinlan, titled “ROSE Open Compiler Infrastructure for Software Analysis, Transformation, and Optimization”.

• Date: Thursday, April 2nd, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

(NB. This seminar is on Thursday, instead of the usual Tuesday slot.)Abstract:  ROSE is a tool for building source-to-source transformation tools for the custom analysis, optimization, and transformation of large scale C, UPC, C++ and Fortran (F2003,F95,F90,F77,F66) applications, and also OpenMP.  Recent work over the last two years has added binary analysis support to ROSE (specifically support for x86, ARM, and PowerPC instruction sets and both Windows (PE, NE, LE, DOS formats)and Linux (Elf format). More recent work has added dynamic analysis support using “Intel Pin” to mix both static and dynamic analysis.  ROSE has an external community of users, developers, and collaborators and has been used in a number of research and industry tools (more information is available at www.roseCompiler.org). It has been a basis for a number of external collaborations in program optimization and cyber-security and we invite new ones.Specifically, ROSE is packaged to allow construction of custom tools by a non-compiler audience. Central to ROSE is the analysis and transformation of the Abstract Syntax Tree (as well as other graphs generated from it) and its transformation to generate new code. Research work has addressed a range of topics from optimization (loop optimization, MPI optimization, data structure optimization, automated parallelization using OpenMP, etc.) to the details of macro handling in CPP preprocessing and advanced token handling for extremely precise levels of source-to-source code regeneration and analysis of subtle details typically not possible within conventional compiler infrastructures.Ongoing research has focused on the use of ROSE within Cyber-Security research and the development of supporting program analysis and support for detection of general properties of both source code and binaries. Current work includes the representation and analysis of binaries and the leveraging of source-code based program analysis for use in binary analysis. Ongoing research work within ROSE is to present a uniform program analysis tool chain for both source code and binaries.Recent work has developed Compass, a tool built on top of ROSE.  Compass is a useful tool on its own and also a vehicle for research on the specification of code patterns (secure coding rules) and the detection of rule violations in large scale applications. This talk will present ROSE, Compass, and recent research work on shared and distributed memory parallel static analysis techniques to scale the detection of rule violations for potentially large rule sets (thousands of rules) on large-scale (many-million line) applications.  The exact same infrastructure can also be used for binary analysis, but secure code rule sets for binaries are not as well developed as for source code. This talk will outline some of the work within ROSE generally and with particular emphasis on building research collaborations.Bio: Dan Quinlan is project leader for the ROSE Project at Lawrence Livermore National Laboratory. His research is in numerous areas that intersect computer science and numerical analysis. Research interests include: semantics-based source code transformations and optimizations, C++ compiler tools/infrastructure/design, cache-based optimizations, object oriented abstractions, parallel array classes, parallel data distribution mechanisms, parallel load balancing algorithms, object-oriented numerical frameworks, parallel adaptive mesh refinement, and parallel multigrid algorithms. Quinlan earned his Ph.D. in Computational Mathematics from University of Colorado.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The March 10th Galois Tech Talks was delivered by Don Stewart on “Specialising Generators for High-Performance Monte-Carlo Simulation in Haskell.”Here are the slides.

• Date: Tuesday, March 10, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: We address the tension between software generality and performance in the domain of simulations based on Monte-Carlo methods. We simultaneously achieve generality and high performance by a novel development methodology and software architecture centred around the concept of a specialising simulator generator. Our approach combines and extends methods from functional programming, generative programming, partial evaluation, and runtime code generation. We also show how to generate parallelised simulators.We evaluated our approach by implementing a simulator for advanced forms of polymerisation kinetics. We achieved unprecedented performance, making Monte-Carlo methods practically useful in an area that was previously dominated by deterministic PDE solvers. This is of high practical relevance, as Monte-Carlo simulations can provide detailed microscopic information that cannot be obtained with deterministic solvers.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The second Galois Tech Talk, for 2009, was Isaac Potoczny-Jones (aka SyntaxNinja) on developing for the Android G1 phone. You can read the slides..

The Android G1 is a TMobile phone whose operating system, Android is based on Linux and was developed by Google. It’s a very open smart-phone platform that rivals the iPhone.While I’m no expert in Android or mobile platform development, I will discuss my experiences in Android development and demonstrate the toolchain used to develop software for the Android. I’ll outline the basic features of the platform, with a focus on the factors that make its openness so powerful:* the inter-process communications mechanism whereby applications can advertise the services they offer and other applications can take advantage of those services,* The open-source Java, Eclipse, and Linux-based toolchain,* the OpenIntents project.This will be an informal demonstration and discussion.A group of us in collaboration between the Android Password Safe project and the Openintents project have implemented a cryptography service and a keystore service which other Android applications can use to keep data and passwords safe, in a way that’s convenient for the end user.Our system allows a single password, and periodic single sign-on so that all applications can encrypt, decrypt, and store keys using the same master password that the user enters once.

• Date: Tuesday, January 20, 2008
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

This Galois Tech Talk, the first for 2009, was our very own Joe Hurd talking about package management for theories. You can read the slides

Interactive theorem has grown beyond toy examples in mathematics and program verification, as demonstrated by recent successes such as the Gonthier’s formal proof of the four colour theorem and Leroy’s verified compiler from a realistic subset of C into PowerPC assembly code. As the construction of large programs led to the development of software engineering techniques, there is now a need for theory engineering techniques to support these major verification efforts.In this talk I will present the OpenTheory project, which has defined a simple ‘article’ format to represent theories of higher order logic. Theories in article format can be written by one higher order logic theorem prover, compressed by a standalone tool, stored and read by a different theorem prover. Articles naturally support theory interpretations, which leads to more efficient developments of standard theories, and also provides one approach to handling difficult constructs such as monads without extending the underlying logic. Finally, the grand vision of the OpenTheory article repository is painted, with fully automatic installation and dependency resolution.

• Date: Tuesday, January 13, 2008
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.