Thursday
Feb282013

Tech Talk: Parametricity, Quotient types, and Theorem transfer

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Parametricity, Quotient types, and Theorem transfer

speaker: Brian Huffman

time: Tuesday, 05 March 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

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 Wadler-style "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 types-as-binary-relations, 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.

bio:

Brian Huffman is a recent PhD graduate from the Department of Computer Science at Portland State University, now at Galois after completing a postdoc at the Technical University of Munich. He has been an avid Haskell programmer since 2001, and has contributed to the development of the Isabelle interactive theorem prover since 2005, with an emphasis on tools for verifying lazy functional programs. Several of Brian's formalizations can be found online at the Archive of Formal Proofs.

Wednesday
Feb062013

Tech Talk: Automatic Function Annotations for Hoare Logic

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Automatic Function Annotations for Hoare Logic

speaker: Daniel Matichuk

time: Tuesday, 12 February 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

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 side-condition 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.

bio:

Daniel Matichuk obtained his B.Sc. in Honors Computer Science from the University of Alberta, Canada in 2011 and has since been working at NICTA in Sydney as a Research Engineer. He will soon be starting his PhD at NICTA and the University of New South Wales. His recent work was aiding in the noninterference proof for the seL4 microkernel and he is interested in maintenance and refactoring in large formal proofs.

Thursday
Nov292012

Tech Talk: Computers and privacy, ACLU of Oregon discusses their 2013 agenda

(There is no need to pre-register for the talk.)

title: Computers and privacy, ACLU of Oregon discusses their 2013 agenda

speaker: Becky Straus

time: Tuesday, 4 December 2012, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Efforts at the federal level to pass laws like the Stop Online Piracy Act (SOPA) and the Cyber Intelligence Sharing and Protection Act (CISPA) have attracted widespread attention and criticism, and rightly so. But Washington, D.C. is far from the only place that officials are making decisions that impact the privacy and free speech rights. State and local officials are jumping into the fray as well, passing laws or creating policies that have immediate impact without the spotlight that accompanies federal action. The fact is that privacy laws have failed to keep up with emerging technologies. This presentation will survey several areas where state and local officials in Oregon have recently been active, including reviewing policies on automated license plate recognition, surveillance cameras, and use of domestic drones. We will discuss how the ACLU of Oregon has been involved and what is on our agenda for the upcoming 2013 state legislative session.

bio:

Becky Straus is the legislative director for the American Civil Liberties Union of Oregon. She joined the staff in 2011 and directs ACLU’s advocacy and lobbying efforts before the Oregon Legislature and coordinates ACLU testimony before public bodies on the full range of civil liberties and civil rights issues in Oregon. She is also ACLU’s primary lobbyist on City of Portland matters.

Friday
Oct122012

2012 Bike Commute Challenge

Galois once again participated in the annual September Bike Commute Challenge, which promotes biking to work via a friendly competition.

Galois had a 33.13% commute rate in September. 14 employees made 146 bike commutes for a total of about 1,400 miles. This year's commute rate is a company record:

  • 2007: 17.1%
  • 2008: 22.9%
  • 2009: 15.2%
  • 2010: 26.4%
  • 2011: 29.1%
  • 2012: 33.1%

According to the Commute Challenge's final results, Galois placed 21st out of 242 teams in the Business and Non-Profits with 25-99 Employees category.

The Galois offices are located in downtown Portland, OR, which Bicycling magazine named America's Best Bike City. Galois encourages use of public and active transportation by providing bike racks and a shower room in our office. Our location is directly on two of Portland's light-rail lines and only a couple blocks from two others.

Tuesday
Oct092012

Tech Talk: Towards a Formally Verified Component Platform

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Towards a Formally Verified Component Platform

speaker: Matthew Fernandez

time: Tuesday, 16 October 2012, 10:30am

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:
In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening 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. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based 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.

bio: Matthew is a current PhD student at NICTA and the University of New South Wales, Australia. His research interests include kernel design, compilers, component systems and compiler implementation. His current work is aiming to provide formal guarantees for a component-based development environment on the seL4 microkernel.

Page 1 ... 5 6 7 8 9 ... 49 Next 5 Entries »