Tech talk: Designing a practical dependently typed language

Wednesday, November 11, 2015

abstract: The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In […]

Read More

Tech talk: Evidence-based Trust of Symbolic Execution-based Verification

Wednesday, August 12, 2015

abstract: Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in […]

Read More

Tech Talk: Viper: Verification Infrastructure for Permission-based Reasoning

Thursday, July 30, 2015

abstract: Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from […]

Read More

Tech talk: A Brief History of Verifiable Elections

Monday, July 27, 2015

abstract: Since the ideas were first published in 1981, verifiable election technologies have undergone decades of research successes and deployment failures. This talk will trace the history of these technologies, their evolution, and the practical challenges that they have faced. We’ll then look forward at the potential for near-term successes and the public benefits that […]

Read More

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: 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