Tech Talk: Verifying Stream Fusion with Isabelle/HOLCF

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.

Read More

Tech Talk: A Newbie’s Exploration of Separation Logic

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.

Read More

Tech Talk: Orc in Haskell

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.

Read More

Tech Talk: Growing Software

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.

Read More

Tech Talk: ROSE Open Compiler Infrastructure

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.

Read More

Galois Tech Talk: Specializing Generators for High-Performance Monte-Carlo Simulation in Haskell

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.

Read More

Tech Talk: Android G1: Experiences with an open mobile platform

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.

Read More

Tech Talk: OpenTheory: Package Management for Higher Order Logic Theories

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.

Read More

Tech Talk: Mechanically verified LISP interpreters

This week’s tech talk will be Magnus Myreen from Cambridge talking about mechanically verified Lisp interpreters. It will be held at the irregular time of 2pm, Friday Nov 14.

This talk describes work on constructing verified interpreters for a small LISP-like language using the interactive theorem prover HOL4.  The LISP interpreters have been proved correct with respect to detailed x86, ARM and PowerPC processor models (written by Sarkar, Fox and Leroy). New techniques for expressing correctness of machine code were developed, as well as new techniques for proof-producing decompilation and compilation to/from HOL4 functions. A copying garbage collector (a Cheney collector) was verified and subsequent proofs were built upon its verified specification.

Read More

Factor: an extensible interactive language

A special Galois tech talk next week, with Slava Pestov talking aboutthe Factor programming language, environment, and implementation.

Logistics

  • Thursday Oct 30, 2008, 10.30 – 11.30

Abstract

Factor is a programming language which has been in development for a little over 5 years. Factor is influenced by Forth, Lisp, Smalltalk. Factor takes the best ideas from Forth — simplicity, short, succint, code, emphasis on interactive testing, and meta-programming. Factor also brings modern high-level language features such as garbage collection, object orientation and functional programming familiar to users of languages such as Lisp, Smalltalk and Python. Finally, recognizing that no programming language is an island, Factor is portable, ships with a full-featured standard library, deploys stand-alone binaries, and interoperates with C and Objective-C.In this talk, I will give the rationale for Factor’s creation, present an overview of the language, and show how Factor can be used to solve real-world problems with a minimum of fuss. At the same time, I will emphasize Factor’s extensible syntax, meta-programming and reflection capabilities, and show that these features, which are unheard of in the world of mainstream programming languages, make programs easier to write, more robust, and fun.

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.

Read More