Tech talk: Effective Verification of Low-Level Software with Nested Interrupts

Tuesday, July 28, 2015

abstract: Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent […]

Read More

Tech talk: An Overview of Emerging Cybersecurity Policy and Law

Tuesday, June 30, 2015

slides: goo.gl/MtQmas abstract: Why is cybersecurity such a hard problem? The US government, its citizens, and the organizations that write software are all on the same team, but in many cases, our interests are just not aligned. For instance, there have been endless political and social disagreements about the best way to share cyber threat […]

Read More

Tech talk: The CH2O project: making sense of the C standard

Thursday, June 18, 2015

abstract: CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent. There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and […]

Read More

Tech talk: High Tech Amateur Rockets at PSAS

Tuesday, April 14, 2015

abstract: Portland State Aerospace Society (PSAS) is a student aerospace engineering project at Portland State University. We’re building ultra-low-cost, open source rockets that feature some of the most sophisticated amateur rocket avionics systems anywhere. Learn some of the history of the group, why steering a rocket is very, very hard, and what we’re doing to […]

Read More

Tech talk: From Haskell to Hardware via CCCs

Tuesday, April 07, 2015

abstract: For the last several years, speed improvements in computing come mainly from increasing parallelism. Imperative programming, however, makes parallelization very difficult due to the many possible dependencies implied by effects. For decades, pure functional programming has held the promise of parallel execution while retaining the very simple semantics that enables practical, rigorous reasoning. This […]

Read More

Tech Talk: Rust, its FFI, and PAM

Tuesday, March 24, 2015

abstract: Jesse has been using Rust to write a PAM module. He will tell us about what he has learned about working with Rust, and about getting Rust’s lifetime-checking to mesh with external C functions. bio: Jesse Hallett is a research engineer at Galois. He has extensive experience in web and high-level programming; but has […]

Read More

Tech Talk: Dependently typed functional programming in Idris, 3 of 3

Thursday, January 22, 2015

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, […]

Read More

Tech Talk: Dependently typed functional programming in Idris, 2 of 3

Tuesday, January 20, 2015

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, […]

Read More

Tech Talk: Dependently typed functional programming in Idris, 1 of 3

Thursday, January 15, 2015

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, […]

Read More