Viewing 0 current events matching “galois” by Date.
Sort By: Date  Event Name, Location , Default 

No events were found. 
Viewing 79 past events matching “galois” by Date.
Sort By: Date  Event Name, Location , Default 

Tuesday
Aug 19, 2008

Galois Tech Talk: Adventures in Foreign Function Interfaces – Galois, Inc Title: Adventures in Foreign Function Interfaces Speaker: Joel Stanley
Date: Tuesday, August 19th, 10.30am Location: Galois, Inc.
Abstract:
About the Galois Tech Talks. 
Tuesday
Sep 2, 2008

Galois Tech Talk: GpuGen: Bringing the Power of GPUs into the Haskell World – Galois, Inc Title: GpuGen: Bringing the Power of GPUs into the Haskell World Speaker: Sean Lee
Date: Tuesday, September 2nd.
Location: Galois, Inc.
Abstract: For the last decade, the performance of GPUs has outgrown CPUs, and their programmability has also improved to the level where they can be used fo generalpurpose computations. Nonetheless, GPU programming is still limited only to those who understand the hardware architecture and the parallel processing. This is because the current GPU programming systems are based on the specialized parallel processing model, and require lowlevel attention in many aspects such as thread launching and synchronization. The need for a programming system which provides a highlevel abstraction layer on top of the GPU programming systems without losing the performance gain arises to facilitate the use of GPUs. Instead of writing a programming system from the scratch, the development of a Haskell extension has been chosen as the ideal approach, since the Haskell community has already accumulated a significant amount of research and resources for Nested Data Parallelism, which could be adopted to provide a highlevel abstraction on GPU programming and even to broaden the applicability of GPU programming. In addition, the Foreign Function Interface of Haskell is sufficient to be the communication medium to the GPU. GpuGen is what connects these two dots: GPUs and Haskell. It compiles the collective data operations such as scan, fold, map, etc, which incur most computation cost, to the GPU. The design of the system, the structure of the GpuGen compiler, and the current development status are to be discussed in the talk. Biographical details: Sean Lee is a PhD candidate at the UNSW, Sydney, working in the Programming Languages & Systems Group. This summer he's been interning at Nvidia in Santa Clara, working on programming GPUs with Haskell. About the Galois Tech Talks. Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Tuesday
Sep 9, 2008

Galois Tech Talk: PrettyPrinting a Really Long Formula (or, "What a Mathematician Could Learn from Haskell") – Galois, Inc TITLE: PrettyPrinting a Really Long Formula (or, "What a Mathematician Could Learn from Haskell") SPEAKER: Lee Pike, R&D Engineering, Galois, Inc. DATE: Tuesday, September 9th. 10.30am LOCATION: ABSTRACT: To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport's brief paper, "How to Write a Long Formula" and "How to Write a Proof" in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification. I will describe the problem and present one particular solution, as implemented in a simple prettyprinter I've written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a "HOL Normal Form" for presenting specifications, much like BNF is used for presenting language definitions. BIOGRAPHICAL DETAILS: http://galois.com/company/people/lee_pike/ ABOUT THE GALOIS TECH TALKS. Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Monday
Sep 15, 2008

Galois Tech Talks: Leftfold enumerators  Towards a safe, expressive and efficient I/O interface for Haskell – Galois, Inc Title: Leftfold enumerators
Speaker: Johan Tibell
Date: Monday, September 15th.
Location: Galois, Inc.
Abstract:
About the Galois Tech Talks. 
Tuesday
Sep 16, 2008

Galois Tech Talk: Theorem Proving for Verification – Galois, Inc Title: Theorem Proving for Verification Speaker: John Harrison
Date: Tuesday, September 16th.
Location: Galois, Inc.
Abstract:
Biographical details:
About the Galois Tech Talks. 
Thursday
Oct 2, 2008

Galois Tech: Advanced Modeling, Design and Verification using HighLevel Synthesis – Galois, Inc Title: Bluespec: Advanced Modeling, Design and Verification using HighLevel Synthesis Speaker: Rishiyur Nikhil CTO, Bluespec, Inc. Date: Thursday, October 2nd. 10.30am Location: Galois, Inc., 421 SW 6th Ave. Suite 300, (3rd floor of the Commonwealth Building) ABSTRACT: Over the past few years, several projects in major companies have been adopting BSV (Bluespec SystemVerilog) as their nextgeneration tool of choice for IP design, modeling (for both architecture exploration and early software development), and verification enviroments. The reason for choosing BSV is its unique combination of: (1) excellent computation model for expressing complex concurrency and communication, based on atomic transactions and atomic transactional intermodule methods (2) very high level of abstraction and parameterization (principally inspired by Haskell) (3) full synthesizability, enabling execution on FPGAs, obtaining better performance (3 to 4 orders of magnitude) and scalability than software simulation at comparable levels of detail. In this presentation, I will provide a brief technical overview of BSV (points 13 above), and describe several customer projects using BSV. I will also briefly contrast BSV with other approaches to High Level Synthesis (particularly those based on C/C++/SystemC). BIOGRAPHY: Rishiyur S. Nikhil is cofounder and CTO of Bluespec, Inc., which develops tools that dramatically improve correctness, productivity, reuse and maintainability in the design, modeling and verification of digital designs (ASICs and FPGAs). The core technologies consist of a language, BSV (Bluespec SystemVerilog), which enables very abstract source descriptions based on scalable atomic transactions and extreme parameterization, and tools for highquality synthesis of BSV into RTL. Earlier, from 2000 to 2003, he led a team inside Sandburst Corp. (later acquired by Broadcom) developing Bluespec technology and contributing to 10Gb/s enterprise network chip models, designs and design tools. From 1991 to 2000 he was at Cambridge Research Laboratory (DEC/Compaq), including one and a half years as Acting Director. From 1984 to 1991 he was a professor of Computer Science and Engineering at MIT. He has led research teams, published widely, and holds several patents in functional programming, dataflow and multithreaded architectures, parallel processing, compiling, and EDA. He is a member of ACM and IFIP WG 2.8 on Functional Programming, and a Senior Member of IEEE. He received his Ph.D. and M.S.E.E. in Computer and Information Sciences from the Univ. of Pennsylvania, and his B.Tech in EE from IIT Kanpur. ABOUT THE GALOIS TECH TALKS: Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Tuesday
Oct 7, 2008

Galois Tech Talk: The Future of Cabal (Haskell package management) – Galois, Inc Duncan Coutts, from WellTyped (http://welltyped.com), will be giving a tech talk tomorrow about the technical direction of Cabal, Haskell package infrastructure, and the problems of managing very large amounts of Haskell code. ... TITLE: The Future of Cabal  "A language for build systems" and "Constraint solving problems in package deployment" SPEAKER: Duncan Coutts, WellTyped, LLP DATE: Tuesday, Oct 7, 2008 10.30am LOCATION: Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon ABSTRACT: This will be an informal talk and discussion on two topics:
Build systems are easy to start but hard to get right. We'll take the view of a language designer and look at where our current tools fall down in terms of safety/correctness and expressiveness. We'll then consider some very early ideas about what a build system language should look like and what properties it should have. Currently this takes the form of a design for a build DSL embedded in Haskell.
We are all familiar, at least peripherally, with package systems. Every Linux distribution has a notion of packages and most have high level tools to automate the installation of packages and all their dependencies. What is not immediately obvious is that the problem of resolving a consistent set of dependencies is hard, indeed it is NPcomplete. It is possible to encode 3SAT or Sudoku as a query on a specially crafted package repository. We will look at this problem in a bit more detail and ask if the right approach might be to apply our knowledge about constraint solving rather than the current adhoc solvers that most real systems use. My hope is to provoke a discussion about the problem. We can concentrate on one topic or the other depending on peoples interest. ABOUT THE GALOIS TECH TALKS: Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Tuesday
Oct 14, 2008

Galois Tech Talk: Type Correct Changes, A Safe Approach to Version Control Implementation – Galois, Inc Next week's tech talk, a special treat, with Jason Dagit (aka. lispy on haskell) dropping by to talk about using GADTs to clean up darcs' patchtheory implementation. TITLE: Type Correct Changes A Safe Approach to Version Control Implementation speaker: Jason Dagit LOCATION: Galois, Inc. 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building) Portland, Oregon ABSTRACT: This will be a talk about Darcs and type safe manipulations of changes: Darcs is based on a data model, known as Patch Theory, that sets it apart from other version control systems. The power of this data model is that it allows Darcs to manage significant complexity with a relatively straightforward user interface. We show that Generalized Algebraic Data Types (GADTs) can be used to express several fundamental invariants and properties derived from Patch Theory. This gives our compiler, GHC, a way to statically enforce our adherence to the essential rules of our data model. Finally, we examine how these techniques can improve the quality of the darcs codebase in practice. PRESENTER: Jason Dagit graduated from Oregon State University with B.S. degrees in Computer Science and Mathematics. He is currently employed at PTV America while completing his Masters degree at Oregon State under coadvisors Dr. David Roundy and Dr. Martin Erwig. During his time in graduate school he has studied both usability and programming languages. He participated in the 2007 Google Summer of Code where he worked under Dr. Roundy to improve Darcs conflict handling. ABOUT THE GALOIS TECH TALKS: Galois (http://galois.com) 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. If you're planning to attend, dropping a note to [email protected] is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Thursday
Oct 30, 2008

Galois Tech Talk: Slava Pestov on the Factor programming language – Galois, Inc 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 metaprogramming. Factor also brings modern highlevel 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 fullfeatured standard library, deploys standalone binaries, and interoperates with C and ObjectiveC. 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 realworld problems with a minimum of fuss. At the same time, I will emphasize Factor’s extensible syntax, metaprogramming 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. Biography:
. 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. If you're planning to attend, dropping a note to d...@galois.com is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Tuesday
Jan 13, 2009

Galois Tech Talk: OpenTheory, Package Management for Higher Order Logic Theories – Galois, Inc PRESENTATION Title: OpenTheory: Package Management for Higher Order Logic Theories Speaker: Joe Hurd, Galois, Inc. Abstract: 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. ABOUT THE GALOIS TECH TALKS: Galois (http://galois.com) 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. If you're planning to attend, dropping a note to donsATgaloisDOTcom is appreciated, but not required. If you're interested in giving a talk, we're always looking for new speakers. 
Tuesday
Jan 20, 2009

Galois Tech Talk: Android G1: Experiences with an open mobile platform – Galois, Inc The next Galois Tech Talk, #2 for 2009, will be Isaac PotocznyJones (aka SyntaxNinja) on developing for the Android G1 phone.
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. 
Friday
Sep 18, 2009

Building Systems That Enforce Measurable Security Goals – Galois, Inc The next talk in the Galois Tech Seminar series: [Note the Friday date, instead of the usual Tuesday slot!]
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/09/10/jaegermeasurablesecurit/ An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Tuesday
Oct 6, 2009

Galois Tech Talk: Roll Your Own Test Bed for Embedded RealTime Protocols: A Haskell Experience – Galois, Inc The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/09/29/pikehaskell0/ Abstract: We present by example a new application domain for functional languages: emulators for embedded realtime protocols. As a casestudy, we implement a simple emulator for the Biphase Mark Protocol, a physicallayer network protocol in Haskell. The surprising result is that a pure functional language with no builtin notion of time is extremely wellsuited for constructing such emulators. Furthermore, we use Haskell’s propertychecker QuickCheck to automatically generate realtime parameters for simulation. We also describe a novel use of QuickCheck as a probability calculator for reliability analysis. Bio: Lee Pike is a member of the technical staff at Galois. Previously, he was a research scientist with the NASA Langley Formal Methods Group, primarily involved in the SPIDER project. His research interests include applying formal methods to safetycritical and securitycritical applications, with a focus on industrialscale endeavors. An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Tuesday
Oct 13, 2009

Galois Talk: Constructing a Universal Domain for reasoning about Haskell Datatypes – Galois, Inc The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/06/huffmanuniversal/ An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Tuesday
Oct 20, 2009

Galois Talk: Writing Linux Kernel Modules with Haskell – Galois, Inc The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/13/haskellkernelmodules/ An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Tuesday
Oct 27, 2009

Galois Talk: How to choose between a screwdriver and a drill – Galois, Inc The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/20/crenshawsimplex/ An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Tuesday
Nov 3, 2009

Galois Talk: Testing FirstOrderLogic Axioms in AutoCert – Galois, Inc The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/10/28/ahnautocert/ An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Friday
Nov 13, 2009

Galois Talk: HoareLogic – fiddly details and small print – Galois, Inc [NB. This talk is on Friday, instead of the usual Tuesday slot.] The next talk in the Galois Tech Seminar series:
For details (including an abstract and speaker bio), please see our blog post: http://www.galois.com/blog/2009/11/04/chapmanhoare/ An RSVP is not required; but feel free to drop a line to [email protected] if you've any questions or comments. Levent Erkok 
Tuesday
Dec 15, 2009

Galois Tech Talk: Beautiful Differentiation – Galois, Inc The December 15th Galois Tech Talk will be delivered by John Launchbury. He will present Conal Elliott’s 2009 ICFP paper entitled Beautiful Differentiation for those of us who were not able to attend this wonderful talk inperson. 
Tuesday
Feb 2, 2010

Galois Tech Talk: "An Introduction to the Maude Formal Tool Environment" – Galois, Inc Hello, The next Galois Tech Talk will be "An Introduction to the Maude Formal Tool Environment", presented by Joe Hendrix on Tuesday, February 2nd, at 10:30am. For more details, please visit: http://www.galois.com/blog/2010/01/29/techtalkanintroductiontothemaudeformaltoolenvironment/ Hope to see you there! Iavor 
Tuesday
May 18, 2010

Galois Tech Talk: Developing Good Habits for BareMetal Programming – Galois, Inc presenter: Mark Jones abstract: Developers of systems software must often deal with lowlevel and performancecritical details that are hard to address in highlevel 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 bitlevel and memorybased 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. 
Monday
May 24, 2010

Galois Tech Talk: The L4.verified Project – Galois, Inc The L4.verified Project Presented by Dr. Gerwin Klein. Last year, the NICTA L4.verifed project produced a formal machinechecked 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. 
Tuesday
Jun 8, 2010

Galois Tech Talk: LargeScale Static Analysis at Mozilla – Galois, Inc presenter: Taras Glek abstract: A competitive browser market requires fastpaced 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. 
Tuesday
Jun 15, 2010

Galois Tech Talk: Introducing WellFounded Recursion – Galois, Inc Introducing WellFounded Recursion Eric Mertens Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of wellfounded 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. 
Friday
Jul 9, 2010

Galois Tech Talk: Requirements and Performance of Data Intensive, Irregular Applications – Galois, Inc Requirements and Performance of Data Intensive, Irregular Applications Dr. John Feo 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 battlespace 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, integerbased 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 largescale floating point intensive simulations are inadequate, and more suitable highend 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. 
Tuesday
Aug 17, 2010

Galois Tech talk: Computers As We Don’t Know Them – Galois, Inc Computers As We Don’t Know Them Christof Teuscher, PhD 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 longterm 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. Selfassembled nanoscale cellular automata (CAs) and random boolean networks (RBNs) will serve as a simple showcase. I will also present the efforts underway to selfassemble massivescale nanowirebased interconnect fabrics for spatial computers and what the challenges are in terms of computations and communication in such a nonclassical system. 
Tuesday
Aug 24, 2010

Galois Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving – Galois, Inc abcBridge: Functional interfaces for AIGs and SAT solving Edward Z. Yang SAT solvers are perhaps the most underutilized hightech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NPcomplete problems in time for lunch, and there are many, many practical problem domains which involve NPcomplete 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 typesafe interface for building and manipulating andinverter graphs. We hope to release abcBridge soon as open source. 
Tuesday
Oct 12, 2010

Galois Tech Talk: Application of Computer Algebra Techniques in Verification of Galois Field Multipliers: Potential + Challenges – Galois, Inc Presented by Priyank Kalla. Applications in Cryptography require multiplication and exponentiation operations to be performed over Galois fields GF(2^k). Therefore, there has been quite an interest in the hardware design and optimization of such multipliers. This has led to impressive advancements in this area — such as the use of composite field decomposition techniques, use of Montgomery multiplication, among others. My research group has recently begun investigations in the verification of such Galois Field multipliers. Unfortunately, the wordlength (k) in such multipliers can be very large: typically, k = 256. Due to such large wordlengths, verification techniques based on decision diagrams, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques, mainly Groebner bases theory, to tackle this problem. In this talk, we will see why Groebner bases techniques look promising, while at the same time also studying the challanges that have to be overcome. 
Friday
Oct 22, 2010

Galois Tech Talk: Databases are Categories 2: Refinements and Extensions. – Galois, Inc presenter: David Spivak About five months ago I gave a talk here at Galois called “Databases are categories.” The basic idea was that a database schema can be represented as a category C and its states can be represented as functors C–>Set. In this talk I’ll refine that notion a bit, explaining that schemas are better represented as sketches. I’ll also show how, within this model one can: deal with incomplete data; incorporate typing and calculated fields; and perform queries, define views, and migrate data between disparate schemas. That is, I’ll try to show that the categorical approach handles everything one might hope it would. Finally, I’ll discuss a linguistic version of categories, called “ologs,” and show how they may help to democratize information storage. 
Tuesday
Nov 9, 2010

Galois Tech Talk: Copilot: A Hard RealTime Runtime Monitor – Galois, Inc Presented by Lee Pike. We address the problem of runtime monitoring for hard realtime programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a streambased dataflow language that generates small constanttime and constantspace C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying realtime operating system. This talk will include fun pictures and videos. 
Tuesday
Nov 16, 2010

Galois Tech talk: Formal Methods Applied to Control Software – Galois, Inc speaker: Alwyn Goodloe Critical cyberphysical systems, such as avionics, typically have one or more components that control the behavior of dynamical physical systems. The design of such control systems is well understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the FramaC tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers. 
Tuesday
Nov 30, 2010

Galois Tech Talk: The Rubinius Virtual Machine – Galois, Inc Presented by Brian Ford Ruby is a highly dynamic, stronglytyped programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single inheritance, mixins, and syntax features like omission of parentheses that make it wellsuited for embedded domainspecific languages. Ruby was popularized by the Ruby on Rails web development framework. The Rubinius project began as an implementation of the Ruby programming language roughly following the design of the Smalltalk80 virtual machine described in the Blue book (“Smalltalk80: the language and its implementation” by Adele Goldberg and David Robson). We have extended the initial implementation based on modern research in virtual machines, garbage collectors, and justintime (JIT) compilers. Rubinius currently features a stackoriented opcode virtual machine, generational garbage collector, and LLVMbased JIT compiler. Most of the Ruby core library and the bytecode compiler are written in Ruby. We will examine the main features of Rubinius and take a deeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load, startup, and suitability for using Rubinius in Android phones. If there is time and interest, we will discuss implementing programming languages besides Ruby on Rubinius. 
Galois Tech Talk: The Rubinius Virtual Machine – Galois, Inc Presented by Brian Ford Ruby is a highly dynamic, stronglytyped programming language created by Yukihiro Matsumoto in 1993 and first released in 1995. It borrows from Smalltalk, Lisp, and Perl. Ruby has single inheritance, mixins, and syntax features like omission of parentheses that make it wellsuited for embedded domainspecific languages. Ruby was popularized by the Ruby on Rails web development framework. The Rubinius project began as an implementation of the Ruby programming language roughly following the design of the Smalltalk80 virtual machine described in the Blue book (“Smalltalk80: the language and its implementation” by Adele Goldberg and David Robson). We have extended the initial implementation based on modern research in virtual machines, garbage collectors, and justintime (JIT) compilers. Rubinius currently features a stackoriented opcode virtual machine, generational garbage collector, and LLVMbased JIT compiler. Most of the Ruby core library and the bytecode compiler are written in Ruby. We will examine the main features of Rubinius and take a deeper dive into some aspects of the virtual machine and JIT compiler. We will also look at possible future work to address memory load, startup, and suitability for using Rubinius in Android phones. If there is time and interest, we will discuss implementing programming languages besides Ruby on Rubinius. 

Tuesday
Jan 11, 2011

Galois Tech Talk: Controlflow Graph Guided Exploration in DDT – Galois, Inc Presented by Rebekah Leslie. The existing implementation of DDT uses a depthfirst search algorithm to drive the exploration of new paths for testing. This algorithm provides full coverage of the program under test, but is limited by the fact that the number of paths increases exponentially with the size of the program. By employing the controlflow graph information of the program under test, we can direct the testing process towards program paths that contain unvisited points and therefore obtain full branch coverage in a smaller number of tests than would be required by the original depthfirst search algorithm. We will present two uses of controlflow graph information in DDT. The first use is a refinement of depthfirst search where controlflow graph information is used to prune the search space to eliminate unnecessary tests. The second use is in the context of a prioritized workqueue that forms the basis for a variety of sophisticated search algorithms that exploit different heuristics. 
Tuesday
Jan 25, 2011

Galois tech talk: Program Inconsistency Detection using Weakest Preconditions – Galois, Inc Presented by Aaron Tomb. Many tools exist to automate the search for defects in software source code. However, many of these tools have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior  often a collection of independent assertions sprinkled throughout the program. Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bugfinding rather than verification. In this dissertation, we describe an inconsistency detection analysis that subsumes previous work and is instead based on the foundation of the weakest precondition calculus. We have applied our analysis to a large body of widelyused opensource software, and found a number of bugs. 
Tuesday
Feb 1, 2011

Galois Tech talk: Verifying seL4based Systems – Galois, Inc Presented by Simon Winwood. In 2009 the NICTA L4.verified project completed the machinechecked correctness proof of the seL4 microkernel. The natural next step is then to use this verified kernel to construct verified systems. In this talk I give an overview of the ongoing work into systems verification in the Trustworthy Embedded Systems project. In particular, I will focus on the use of access control results to reason about the properties of systems in the presence of large untrusted components, such as a Linux kernel. 
Monday
Feb 7, 2011

Galois Tech talk: The Strategy Challenge in Computer Algebra – Galois, Inc Presented by Grant Passmore. In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: userspecifiable adaptations of general reasoning mechanisms reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different. In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worstcase doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one? The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification toolchains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions). 
Tuesday
Feb 15, 2011

Galois Tech Talk: Faster Persistent Data Structures Through Hashing – Galois, Inc Presented by Johan Tibell. The most commonly used map (dictionary) data type in Haskell is implemented using a size balanced tree. While size balanced trees provide good asymptotic performance, their real world performance is not stellar, especially when used with keys which are expensive to compare, such as strings. In this talk we will look at two different map implementations that use hashing to achieve better real world performance. The implementations have different performance characteristics: one provides very fast lookups while the other trades better insert performance for somewhat slower lookups. I will describe the design of these data structures and show some early benchmark results. 
Tuesday
Feb 22, 2011

Galois tech talk: Engineers Without Borders – Galois, Inc Presented by Rachel Lanigan. Engineers Without Borders USA is a fastgrowing national nonprofit impacting developing communities around the world. EWB provides an opportunity for engineering students and professionals to use their skills to develop sustainable, appropriate technologies for specific applications, to help meet the basic needs of people. Our programs typically start with a focus on providing water and sanitation, but often move into other areas depending on the needs of the people. There is a role for everyone at EWB, from engineers to public health professionals. Rachel will give a background on EWB, our local chapter, and how to get involved. 
Tuesday
Mar 15, 2011

Galois Tech Talk: Haskell And The Social Web – Galois, Inc Presented by Philip Weaver. Janrain offers user management services that include single signon, social login, and profile storage. We have recently begun using Haskell extensively to implement our products, and would like to share what the experience has been like. In this talk we will give a technical demonstration of Capture, whose backend is written in Haskell, discuss some of the implementation details of Capture, and look at some of the joys and pitfalls that we experienced. 
Tuesday
Apr 12, 2011

Galois Tech Talk: The OpenTheory Standard Theory Library – Galois, Inc Presented by Joe Hurd. Interactive theorem proving is tackling ever larger formalization and verification projects, and there is a critical need for theory engineering techniques to support these efforts. One such technique is crossprover package management, which has the potential to simplify the development of logical theories and effectively share theories between different theorem prover implementations. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. What is currently missing is a standard theory library that can serve as a published contract of interoperability and contain proofs of basic properties that would otherwise appear in many theory packages. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages. 
Tuesday
Apr 19, 2011

Galois Tech Talk: Using RNA MVX Shared Memory Pools to Improve LargeMemory Workloads and Storage Performance – Galois, Inc Presented by Jim Snow. RNA Networks is a software company focused on providing the next generation storage cache solution that addresses performance deficiencies and the rising cost of storage for virtual environments. Our software solution utilizes compute resources (DRAM and flash) as a distributed clustered cache moving 'active' data off of the storage tier and into the compute tier translating to significant performance gains with no additional investment in hardware resources. RNA's MVX technology is based on a distributed shared memory core that leverages RDMA fabrics and allows for a unified and flexible namespace that can scale proportionally to meet any performance or capacity need. In this presentation we'll discuss the core architecture and how this can be leveraged to both reduce the cost of high end storage and meet high performance storage objectives. 
Tuesday
May 10, 2011

Galois Tech Talk: Empirical Sampling With Haskell – Galois, Inc Presented by Chad Scherrer. Sampling from a large discrete distribution is a common problem in statistics. In this talk, we'll consider a realworld situation where the properties of the distribution cause common approaches to break down, and we'll arrive at a Haskellbased solution that fixes the problem. 
Friday
Jun 3, 2011

(Friday) Galois Tech talk: Building an OpenSource Autonomous QuadCopter – Galois, Inc Presented by Nicholas Begley, Dave Dung Anh, James Heilinger, Alec Rasmussen, and Mark Theuson. It's a bird! It's a plane! No, it's an opensource autonomous quadcopter. In collaboration with the Portland State University Electrical and Computer Engineering Dept., Galois mentored a Spring semester Senior Capstone Project to build an ArduCopter. The ArduCopter is based on the Arduino opensource hardware platform, and includes infrared sensors (collision avoidance), sonar and barometer (altitude hold), GPS (location), magnetometer (direction), and gyro (stabilization). This talk will include a description of the ArduCopter and it's operation, including the trials and tribulations of building and testing one. Of course, the talk will include cool videos. 
Tuesday
Jul 12, 2011

Galois tech talk: Parallel Kinduction based Model Checking – Galois, Inc Presented by Temesghen Kahsai. We give an overview of a parallel kinductionbased model checking architecture for verifying safety properties of synchronous systems. The architecture, which is strictly messagebased, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic kinduction. A first level of parallelism is introduced in the kinduction procedure itself by executing the base and the inductive steps concurrently. A second level of parallelism allows the addition of one or more independent processes that incrementally generate invariants for the system being verified. The invariants are fed to the kinduction loop as soon as they are produced and used to strengthen the induction hypothesis. This architecture allows the verification of multiple properties in an incremental fashion. Specifically, the outcome of a property  valid or invalid  is communicated to the user as soon as the result is known. Moreover, verified valid properties are added as invariants in the model checking procedure to aid the verification of the remaining properties. We provide experimental evidence that this incremental and parallel architecture significantly speeds up the verification of safety properties. Additionally, due to the automatic invariant generation, it also considerably increases the number of provable safety properties. 
Tuesday
Jul 19, 2011

Galois tech talk: Combining Denotational and Operational Semantics for Scalable Proof Development – Galois, Inc Presented by Adam Foltzer. Interpreters offer a convenient and intuitive way for programmers to reason about language behavior through denotational semantics. However in a setting like Coq, where all recursive functions must provably terminate, it is impossible to write interpreters for nonterminating languages. The standard alternative is to inductively define operational semantics, but this can yield proofs that are difficult to automate, particularly in the presence of changing language features. This talk presents a combined approach, where an interpreter is used in combination with operational semantics to prove type preservation of a small functional language. To demonstrate the scalability of the Coq development, let expressions and a pair types will be added and preservation will be proved again with only one extra line of proof script. This technique and development are adapted from Greg Morrisett's lectures at the 2011 Oregon Programming Languages Summer School, and are available at his web site. 
Wednesday
Aug 10, 2011

Galois tech talk: A MultiEncoding Approach for LTL Symbolic Satisfiability Checking – Galois, Inc Presented by Kristin Rozier Formal behavioral specifications written early in the systemdesign process and communicated across all design phases have been shown to increase the efficiency, consistency, and quality of the system under development. To prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. Our focus here is on specifications expressed in linear temporal logic (LTL). We introduce a novel encoding of symbolic transitionbased Buchi automata and a novel, ``sloppy,'' transition encoding, both of which result in improved scalability. We also define novel BDD variable orders based on tree decomposition of formula parse trees. We describe and extensively test a new multiencoding approach utilizing these novel encoding techniques to create 30 encoding variations. We show that our novel encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Details can be found here: http://ti.arc.nasa.gov/profile/kyrozier/. 
Tuesday
Aug 16, 2011

Tech Talk: Backtoback talks on Haskell and Embedded Systems – Galois, Inc Presented by Sebastian Niller and Nis N. Wegmann 1title: Translation of Functionally Embedded Domainspecific Languages With Static Type Preservation by using Witnesses abstract: Static type preservation automatically guarantees typecorrectness of an embedded domainspecific language (eDSL) by tying its type system to that of the hostlanguage. Not only does this obviate the need for a custom type checker, it also preserves typecorrectness during code transformations and optimizations, and simplifies and increases the efficiency of interpreters. When implementing a translator from a source DSL with type preservation to a target DSL, the commonly chosen approach requires the incorporation of extensions in the source DSL specific to the target DSL, which, in cases where multiple backends are required, obfuscates the source DSL and decreases the overall modularity. We show that by using witnesses, a technique which facilitates the construction of typelevel proofs, we can effectively cope with this issue and implement translators without extending the source DSL. We have applied our approach on Copilot, a Haskellembedded domain specific language for runtime monitoring of hard realtime distributed systems, and used it for implementing two backends targeting the Haskellembedded languages Atom and SBV. Our approach restrains to the Haskell 2010 Standard except for existentially and universally quantified types. 2title: From HighLevel Languages to Monitoring FaultTolerant Hardware: CaseStudies of Runtime Verification Using Copilot abstract: Failures of hard realtime systems can be caused by systematic faults in software and hardware, as well as by random hardware faults, and faults due to wear out of hardware components. Even if monitoring software is proven to comply to its specification, there is no guarantee that failing underlying hardware does not affect the monitors themselves. An application of distributed Copilot monitors to a redundant airspeed measurement system is presented. We show the use of monitors enables the system to withstand benign and Byzantine hardware and software faults. The second part of the talk presents current work using Copilot to monitor the MAVLink protocol in flight of a subscale model of an Edge 540T aircraft. 
Tuesday
Aug 23, 2011

Tech Talk: Modular verification of preemptive OS kernels – Galois, Inc Presented by Alexey Gotsman Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling being implemented correctly, and in a preemptive kernel, the correctness of the scheduler is interdependent with the correctness of the code it schedules. This interdependency is even stronger in mainstream kernels, such as Linux, FreeBSD or XNU, where the scheduler and processes interact in complex ways. In this talk I will present the first logic that is able to decompose the verification of preemptive multiprocessor kernel code into verifying the scheduler and the rest of the kernel separately, even in the presence of complex interdependencies between the two components present in mainstream kernels. This is joint work with Hongseok Yang (University of Oxford, UK). 
Tuesday
Aug 30, 2011

Galois Tech Talk: Leveraging Emerging Storage Functionality for New Security Services – Galois, Inc Presented by Kevin Butler The complexity of modern operating systems makes securing them a challenging problem. However, changes in the computing model, such as the rise of cloud computing and smarter peripherals, have presented opportunities to reconsider system architectures, as we move from traditional "stovepipe" computing to distributed systems. In particular, we can build trustworthy components that act to provide security in complex systems. This talk discusses how new disk architectures may be exploited to aid the protection of systems by acting as policy decision and enforcement points. We prototype disks that enforce data immutability at the block level on critical system data, preventing malicious code from inserting itself into system configuration and boot files. We then examine how storage may be used to ensure the integrity state of hosts prior to allowing access to data, and how such a design improves the security of portable storage devices. Using continual measurements of system state, we show through formal reasoning that such a device enforces guarantees that data is read and written while the host is in a good state. Finally, we discuss some recent initiatives to assure the identity of the host and identify future directions for exploring the interface between storage and operating system security. 
Thursday
Nov 10, 2011

Galois Tech Talk: Enforcing Security Policies with a MILS Architecture – Galois, Inc Presented by Dylan McNamee. This talk is an introduction to the MILS (Multiple Independent Layers of Security) architecture, motivated by the challenge of enforcing various kinds of security policies. I'll describe the goals of policy enforcement, traditional means of implementing security enforcement mechanisms, and the emerging MILS architecture for enforcing policies with high assurance. 
Thursday
Nov 17, 2011

Galois Tech Talk: Candid experiences from a hardware startup – Galois, Inc Presented by Eric Migicovsky. Hardware is hard. At least that's what people always say. Building a hardware startup requires a broad base of technical knowledge, from electronics and manufacturing experience to aesthetic and interface design. But Eric Migicovsky chose to start a hardware company after graduating from engineering because he wanted to see something he designed become a physical reality. inPulse is a $150 hackable Bluetooth smartwatch. It connects to your smartphone and displays notifications like incoming emails, calls, and calendar alerts right on your wrist. After launching an SDK, 3rd party developers have started to create apps for inPulse. In his talk, Eric will share some honest stories and anecdotes from various stages of product development. He'll also talk about the costs, timeframes and failure modes of hardware startups. 
Thursday
Dec 15, 2011

Galois Tech Talk: Frenetic: A Network Programming Language – Galois, Inc Presented by Nate Foster. The languages used to program networks today lack modern features. Programming them is a complicated task, and outages and infiltrations are frequent. We believe it is time to develop NETWORK PROGRAMMING LANGUAGES with the following essential features:
The Frenetic language addresses these challenges in the context of OpenFlow networks. It combines a streaming declarative query sublanguage and a functional reactive sublanguage that, together, provide many of the features listed above. Our implementation handles many lowlevel packetprocessing details and keeps traffic in the "fast path" whenever possible. 
Tuesday
Jan 10, 2012

Galois Tech Talk (1 of 3 next week!): Formalizing Haskell 98 in the K Semantic Framework – Galois, Inc Presented by David Lazar Formal semantics is notoriously hard. The K semantic framework (http://kframework.org/) is a system that makes the task of formally defining programming languages easy and practical. The primary goals of the K framework are modularity, expressivity, and executability. Adding a new language feature to a K definition does not require you to revisit and modify existing semantic rules. The K framework is able to concisely capture the semantics of nondeterminism and concurrency. Each K definition automatically yields an interpreter for the language so that the definition can be tested for correctness. These features made it possible to develop a complete formal semantics of the C language in K. The first half of the talk will be an overview of the K semantic framework. We'll discuss the merits of the framework using the K definition of a complex toy language as a guiding example. The second half of the talk will focus on a workinprogress formalization of Haskell 98 in K. We'll look at the challenges of formalizing Haskell and the applications of this work. 
Wednesday
Jan 11, 2012

Galois Tech Talk (2 of 3 next week!): Modelbased Code Generation and Debugging of Concurrent Programs – Galois, Inc Presented by Borzoo Bonakdarpour. Design and implementation of distributed systems often involve many subtleties due to their complex structure, nondeterminism, and low atomicity as well as occurrence of unanticipated physical events such as faults. Thus, constructing correct distributed systems has always been a challenge and often subject to serious errors. We propose a method for generating distributed implementations from highlevel componentbased models that only employ simple synchronization primitives. The method is a sequence of three transformations preserving observational equivalence: (1) A transformation from a global state to a partial state model, (2) a transformation which replaces multiparty strong synchronization primitives in atomic components by pointtopoint send/receive primitives based on asynchronous message passing, and (3) a final transformation to concrete distributed implementation based on platform and architecture. We study the properties of different transformations, in particular, performance criteria such as degree of parallelism and overhead for coordination. The second part of the talk will focus on an automated technique for optimal instrumentation of multithreaded programs for debugging and testing of concurrent data structures. We define a notion of observability that enables debuggers to trace back and locate errors through dataflow instrumentation. Observability in a concurrent program enables a debugger to extract the value of a set of desired variables through instrumenting another (possibly smaller) set of variables. We formulate an optimization problem that aims at minimizing the size of the latter set. Our experimental results on popular concurrent data structures (e.g., linked lists and redblack trees) show significant performance improvement in optimallyinstrumented programs using our method as compared to adhoc overinstrumented programs. 
Thursday
Jan 12, 2012

Galois Tech Talk (3/3 next week!): On deadlock verification in microarchitectural models of communication fabrics. – Galois, Inc Presented by Julien Schmaltz. Communication fabrics constitute an important challenge for the design and verification of multicore architectures. To enable their formal analysis, microarchitectural models have been proposed as an efficient abstraction capturing the highlevel structure of designs. Microarchitectural models also include a representation of the protocols using the communication fabrics. This combination of different aspects in a single model is crucial for deadlock verification. Deadlocks emerge or are prevented in this combination: a system with a deadlockfree communication network combined with a deadlockfree protocol may have deadlocks or a system with a network with deadlocks combined with a deadlockfree protocol may be deadlockfree. This combination also makes the verification problem more complicated. We will present an algorithm for efficient deadlock verification in microarchitectural models. We will discuss the limitations of this approach and point to future research direction. An important future application of our methodology is the verification of cache coherency at the level of microarchitectures. 
Monday
Feb 6, 2012

Galois Tech Talk: Efficient Implementation of Property Directed Reachability – Galois, Inc Presented by Alan Mishchenko. Last spring, in March 2010, Aaron Bradley published the first truly new bitlevel symbolic model checking algorithm since Ken McMillan’s interpolation based model checking procedure introduced in 2003. Our experience with the algorithm suggests that it is stronger than interpolation on industrial problems, and that it is an important algorithm to study further. In this paper, we present a simplified and faster implementation of Bradley’s procedure, and discuss our successful and unsuccessful attempts to improve it. 
Friday
May 11, 2012

Galois Tech Talk: An Analysis of Analysis – Galois, Inc Presented by Charles Parker A basic problem in computer science is binary classification, in which an algorithm applies a binary label to data based on the presence or absence of some phenomenon. Problems of this type abound in areas as diverse as computational biology, multimedia indexing, and anomaly detection. Evaluating the performance of a binary labeling algorithm is itself a complex task, often based on a domaindependent notion of the relative cost of "false positives" versus "false negatives". As these costs are often not available to researchers or engineers, a number of methods are used to provide a costindependent analysis of performance. In this talk, I will examine a number of these methods both theoretically and experimentally. The presented results suggest a set of best practices for evaluating binary classification algorithms, while questioning whether a costindependent analysis is even possible. 
Tuesday
Jun 5, 2012

Why Do Airplanes Crash? Building an OpenSource Aircraft Sensor System – Galois, Inc Presented by Chris Andrew, Kayla Seliner, Mark Craig, and Trang Nguyen. On October 7, 2008, the flight control system of Qantas flight 72 malfunctioned without warning. The failure caused the aircraft to violently pitch down with an acceleration of 0.8g, pitching passengers and crew into the roof of the cabin resulting in many injuries. In the investigation that followed, the malfunction was attributed to a software problem in the Air Data Inertial Reference Unit. These units are utilized on all modern passenger jets, but are proprietary devices not open to public scrutiny. This capstone project develops an open source Air Data Inertial Reference Unit using four redundant Arduino boards each with a microcontroller, 3D gyroscope and accelerometer. Faults are injected into the system through software and outputs are monitored over serial ports allowing the user to test effectiveness of faulttolerant algorithms to mask fail silent and byzantine faults in the sensors. Failures in ADIRU systems are usually complex in nature and arise under very anomalous circumstances suggesting that faulttolerant system design could benefit from the diverse testing and evaluation that can occur in an open source community. This project demonstrates the low entrycost to building a faulttolerant system for opensource design and experimentation. 
Thursday
Jun 28, 2012

Galois Tech Talk: Programming with Narrowing – Galois, Inc Presented by Sergio Antoy from Portland State University. In this talk, I will introduce narrowing, the characterizing feature of functional logic programming, from the programmer's viepoint. Narrowing promotes nondeterminism and it enables computing with incomplete or unknown information. After a short and informal presentation of Curry, the leading functional logic language, I will discuss a few examples showing that narrowing and its associated nondeterminism support programming at a very high level of abstraction. 
Thursday
Aug 2, 2012

Galois Tech Talk: Comprehensive Analysis of the Android Ecosystem – Galois, Inc Presented by Iulian Neamtiu. The relative novelty and rapid evolution pace of the Android ecosystem (platform, vendorinstalled apps and thirdparty apps) means both the platform and apps receive little scrutiny. Hence there is a need for tools that assess, monitor and verify all components of the Android ecosystem. This lack of tools and scrutiny is particularly problematic when combined with the open nature of Google Play, the main app distribution channel. In the first part of this talk we will focus on multilayer profiling of Android apps using ProfileDroid, a tool and framework we developed at UC Riverside. ProfileDroid is useful for a variety of Android app analyses, from performance to usability to security. ProfileDroid monitors and correlates the behavior of an app at four layers: (a) static, or app specification (b) user interaction, (c) operating system, and (d) network layer. Using ProfileDroid on 27 free and paid Android apps, we have revealed: (a) discrepancies between the app specification and app execution, (b) free versions of apps could end up costing more than their paid counterparts, due to an order of magnitude increase in traffic, (c) most network traffic is not encrypted, (d) apps communicate with many more sources than users might expect. In the second part of the talk we will present results from our longterm permission evolution study of the Android ecosystemplatform and 237 appsover three years. We found that the platform has increased the number of dangerous permissions and does not move towards finergrained permissions, and that app developers do not follow the principle of least privilege. We will also briefly discuss our efforts with static information flow tracking for Android apps, as well as building a logandreplay system for Android. 
Tuesday
Aug 28, 2012

Galois Tech Talk: Abstract "Anything": Theory and Proof Reuse via DTP – Galois, Inc Presented by Larry Diehl. Many advanced branches of mathematics involve structures that abstract over well known specific instances, e.g. abstract algebraic structures, equivalence relations, various orders, category theoretic structures, etc. In typed functional programming (e.g. with type classes in Haskell), encoding such structures amounts to enforcing the definition of elements and operations for a particular structure instance on one hand, and being able to use said elements and operations in generic definitions on the other hand. With Dependently Typed Programming (DTP) we can go one step further and define propositions/properties for abstract structures, and subsequently require proofs in particular instances. This talk will tell the story of how examples of particular instances inspire an abstract definition (including its propositional properties), how to then instantiate the original concrete examples in the new abstract definition, and finally create further abstract definitions that depend on previously defined ones. Emphasis will be given on how easily concrete proofs can be used as evidence for abstract propositions, and how proofs about abstract structures parameterized by other abstract structures may reuse their proofs (similar to the more common concept of reusing operations in subsequent abstract definitions). The talk will use Agda as its demonstration language, but proofs will mostly be in the form of equational reasoning that should look familiar to the nonexpert. 
Thursday
Aug 30, 2012

Galois Tech Talk: Formal Verification of Monad Transformers – Galois, Inc Presented by Brian Huffman. We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with firstclass type constructors, firstclass polymorphism, or type quantification; instead, we rely on a domaintheoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes. 
Tuesday
Oct 16, 2012

Galois Tech Talk: Towards a Formally Verified Component Platform – Galois, Inc Presented by Matthew Fernandez. In safety and securitycritical environments software failures that are acceptable in other contexts may have expensive or even lifethreatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Componentbased development has the potential to lower the cost of systemwide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a componentbased development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation. 
Tuesday
Feb 12, 2013

Galois Tech Talk: Automatic Function Annotations for Hoare Logic – Galois, Inc Presented by Daniel Matichuk. Formal verification can provide a high degree of assurance for critical software, but can come at the cost of large artefacts that must be maintained alongside it. When using an interactive theorem prover, these artefacts take the form of large, complex proofs where the ability to reuse and maintain them becomes paramount. I will present my work on a function annotation logic, which is an extension to Hoare logic that allows reasoning on intermediate program states to be easily reused. Program functions are annotated with properties as a sidecondition of existing proofs. These annotations can reduce the proof burden substantially when subsequent program properties need to be shown. Implemented in Isabelle, it is shown to be practically useful by greatly simplifying cases where existing proofs contained largely duplicated reasoning. 
Tuesday
Mar 5, 2013

Galois Tech Talk: Parametricity, Quotient types, and Theorem transfer – Galois, Inc Presented by Brian Huffman. A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadlerstyle "free theorems" about a polymorphic function from its type; e.g. rev :: [a] > [a] must satisfy map f (rev xs) = rev (map f xs). In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using typesasbinaryrelations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types. 
Tuesday
Mar 12, 2013

Galois Tech Talk: Inferring Phylogenies Using Evolutionary Algorithms – Galois, Inc Presented by Erlend Hamberg. An important problem in genetics is phylogenetic inference: Coming up with good hypotheses for the evolutionary relationship between species – usually represented as a “family tree”. As the amount of molecular data (e.g. DNA sequences) quickly grows, efficient algorithms become increasingly important to analyze this data. A maximumlikelihood approach with models for nucleotide evolution allows us to use all the sequence data, but is a computationally expensive approach. The number of possible trees also grows rapidly as we include more species. It is therefore necessary to use heuristic search methods to find good hypotheses for the “true” tree. Evolutionary algorithms (EA) is a class of such search/optimization algorithms that has been shown to perform well in other areas where the search space is large and irregular. I will explain my approach and my findings from using an evolutionary algorithm for inferring phylogenies from molecular data. 
Tuesday
Apr 9, 2013

Galois Tech Talk: Introducing HERMIT: A Plugin for Transforming GHC Core Language Programs – Galois, Inc Presented by Andrew Farmer. The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks, leaving the programmer to do them by hand. This talk introduces HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. The talk will explore design choices in HERMIT, demonstrate its use on examples, and seek input for further development and case studies. 
Tuesday
Apr 30, 2013

Galois Tech Talk: Hardware Security's Hierarchy of Attacks – Galois, Inc Presented by Joe FitzPatrick. Generally, there is a very low barrier to entry when it comes to software or networkbased attacks due to the fact that actual costs are minimal and most resources are readily available. This does mean that it's generally much easier to attack the software of a system than the hardware, but unfortunately that also leads to overconfidence in, as well as misplaced trust in hardware. There is a clear 'hierarchy of attacks' in the hardware world. There are costs, often significant, involved in acquiring your hardware 'target' which might be damaged or destroyed in the process. There are a number of useful tools that cost anywhere from a few dollars to a few million dollars. I'll give a couple examples of what's possible within budgets of $100, $10,000, and $1,000,000. I'll point out how many capabilities are much more accessible than most assume, and how vulnerable to sub$100 attacks most of our 'secure' hardware really is. 
Tuesday
Jun 4, 2013

Pi in the Sky: How Computer Vision can give a Quadcopter Autonomous Flight – Galois, Inc Five students in PSU’s Electrical and Computer Engineering Senior Capstone sequence want to show you what they’ve created: an inexpensive computer vision system for a quadcopter running on a Raspberry Pi board. One might be surprised how simple it is to code a decent object tracking algorithm using opensource software, and how difficult it is to keep a quadcopter from crashing into the wall in the debug stage. This talk should appeal to the RC hobbyist, the embedded systems programmer, and anyone interested in the art of computer vision. The presentation will include video footage of what these students have accomplished and how they pulled it off. 
Friday
Jun 14, 2013

Galois Tech Talk: Noninterference and Binary Correctness of seL4 – Galois, Inc Presented by Gerwin Klein and Thomas Sewell. This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code. The first part of the talk presents a new noninterference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain. The binary proof addresses the compilercorrectness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assemblylike programs powered by modern SMT solvers. We cover the previouslyverified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1. 
Tuesday
Jun 25, 2013

Galois Tech Talk: The ConstrainedMonad Problem – Galois, Inc Presented by Neil Sculthorpe. In Haskell, there are many data types that would form monads were it not for the presence of typeclass constraints on the operations on that data type. This is a frustrating problem in practice, because there is a considerable amount of support and infrastructure for monads that these data types cannot use. This talk will demonstrate that a monadic computation can be restructured into a normal form such that the standard monad class can be used. The technique is not specific to monads  it can also be applied to other structures, such as applicative functors. One significant use case for this technique is Domain Specific Languages, where it is often desirable to compile a deep embedding of a computation to some other language, which requires restricting the types that can appear in that computation. 
Tuesday
Jul 2, 2013

Galois tech talk: SMACCMPilot: flying quadcopters using new techniques for embedded programming – Galois, Inc Presented by Pat Hickey. At Galois, we're building critical flight control software using new software methods for embedded systems programming. We will show how we used new domainspecific languages which permit lowlevel hardware manipulation while still providing guarantees of type and memory safety. The flagship application for these new languages is called SMACCMPilot, a clean slate design of quadcopter flight control software built on opensource hardware. This talk will introduce our new software methods and show how we built SMACCMPilot to be high assurance without sacrificing programmer productivity. 
Tuesday
Jul 16, 2013

Galois Tech Talk: Mod your Android – Galois, Inc Presented by Jesse Hallett. Take control of your hardware by installing an open build of Android. Get root access and extend the life of your device. Learn about what is involved in installing a thirdparty OS on your phone or tablet. 
Monday
Jul 29, 2013

Galois tech talk: Typedirected compilation in the wild: Haskell and Core – Galois, Inc Academic papers often describe typed calculi, but it is rare to find one in a production compiler. Indeed, I think the Glasgow Haskell Compiler (GHC) may be the only production compiler in the world that really has a remorselessly staticallytyped intermediate language, informally called "Core", or (when writing academic papers) the more respectablesounding "System FC". As real compilers go, GHC's Core language is tiny: it is a slight extension of System F, with letrec, data types, and case expressions. Yet all of Haskell (now a bit of a monster) gets translated into it. In the last few years we have added one new feature to Core, namely typed (but erasable) coercions that witness type equalities, which turn Core into a particular kind of proofcarrying code. This single addition has opened the door to a range of sourcelanguage extensions, such as GADTs and type families. In this talk I'll describe Core, and how it has affected GHC's development over the last two decades, concentrating particularly on recent developments, coercions, evidence, and type families. To test your mettle I hope to end up with the problem we are currently wrestling with: proving consistency of a nonterminating rewrite system with nonleftlinear rules. 
Thursday
Sep 12, 2013

(Galois Tech Talk) New Directions in Random Testing: from Mars Rovers to JavaScript Engines – Galois, Inc Presented by Alex Groce. One of the most effective ways to test complex language implementations, file systems, and other critical systems software is random test generation. This talk will cover a number of recent results that show howdespite the importance of handtooled random test generators for complex testing targets there are methods that can be easily applied in almost any setting to greatly improve the effectiveness of random testing. Surprisingly, giving up on potentially finding any bug with every test makes it possible to find more bugs over all. The practical problem of finding distinct bugs in a large set of randomly generated tests, where the frequency of some bugs may be orders of magnitude higher than other bugs, is also open to non adhoc methods. 
Friday
Sep 20, 2013

Galois Tech Talk: Chris Anderson on Using Drones in Agriculture – Galois, Inc Small unmanned aircraftmore often called dronesare set to make a big impact on agriculture. You already know about military drones operating overseas, and perhaps you've even seen recreational drones starring in youtube videos, but as the FAA begins permitting commercial use of unmanned aircraft in 2015, you'll see drones replacing all sorts of roles that used to require a manned aircraft, and taking on new roles made possible by their low cost, versatility, and safety. Chris Anderson will speak about the upcoming role of drones in agriculture, a field Chris says "is a big data problem without the big data." Chris will describe how farmers can will drones to curb plant disease, conserve water, and reduce pesticide and fertilizer use. He'll discuss the challenges ahead to integrate air vehicle systems with sensors, specialized cameras, and data processing. 
Tuesday
Oct 22, 2013

Galois Tech Talk: Programming Diversity – Galois, Inc presented by: Ashe Dryden abstract: It's been scientifically proven that more diverse communities and workplaces create better products and the solutions to difficult problems are more complete and diverse themselves. Companies are struggling to find adequate talent. So why do we see so few women, people of color, and LGBTQ people at our events and on the about pages of our websites? Even more curiously, why do 60% of women leave the tech industry within 10 years? Why are fewer women choosing to pursue computer science and related degrees than ever before? Why have stories of active discouragement, dismissal, harassment, or worse become regular news? In this talk we’ll examine the causes behind the lack of diversity in our communities, events, and workplaces. We’ll discuss what we can do as community members, event organizers, and coworkers to not only combat this problem, but to encourage positive change by contributing to an atmosphere of inclusivity. bio: Ashe Dryden is an indie ruby developer living in Madison, WI. She's been involved with the web in some form or another over the course of the past 12 years. Ashe is an outspoken educator for diversity, inclusiveness, and empathy. She's currently writing a book on increasing diversity within companies, as well as working on a video series and site to serve as a resource to people who want to get involved. When she isn't discussing technology or it’s intersection with culture, she's cycling, tweeting, playing board games, debating the social implications of Star Trek episodes, being that awkward girl at the party, and waiting for her next burrito fix. 
Wednesday
Jun 11, 2014

Portland Novice Programmers Monthly Meetup – Galois, Inc Small presentation on the Meetup idea and values at 5:45pm by Tyler Zika. Socializing, forming Master Mind groups, coding, and brainstorming from 67pm. Bring your laptop if you want to show what you are working on or you'd like some help. Another small presentation. Topic and speaker TBA for remainder of Meetup. RSVP on meetup.com site. Please and thank you. Happy Coding! 