Tuesday
Jun232009

Tech Talk: Verifying Stream Fusion with Isabelle/HOLCF

The June 30th Galois Tech Talk will be delivered by Brian Huffman, titled “Verifying Stream Fusion with Isabelle/HOLCF”

  • Date: Tuesday, June 30th, 2009
  • Time: 10:30am - 11:30am
  • Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204
Slides from the talk.Abstract: Stream fusion is a system for removing intermediate data structures from Haskell programs that manipulate lists.  Formal verification of such libraries requires very precise modeling in a theorem prover, to avoid strictness-related bugs.In this talk I will present a formalization of the stream fusion library in Isabelle/HOLCF, a theorem proving environment designed especially for reasoning about functional programs.  I will show how to prove the correctness of various stream functions using "fixed-point induction", a powerful reasoning principle for general recursive functions.Bio: Brian Huffman is a PhD student in Computer Science at Portland State  University, working with advisor John Matthews. He studies formal reasoning with  the Isabelle theorem prover, specializing in formalized mathematics and semantics of functional languages. He is currently the maintainer of Isabelle/HOLCF, a logic for domain theory.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Tuesday
Jun162009

Tech Talk: A Newbie's Exploration of Separation Logic

The June 23rd Galois Tech Talk will be delivered by John Launchbury, titled “A Newbie's Exploration of Separation Logic.”

  • Date: Tuesday, June 23rd, 2009
  • Time: 10:30am - 11:30am
  • Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204
Abstract: I was just privileged to be in a Separation Logic Tutorial, given by its inventor, John Reynolds. Separation logic allows descriptions of storage and other resources concisely, providing a novel system for reasoning about imperative programs with shared mutable data structures. Recent years have seen a flurry of activity in Separation Logic, extending it to apply from shared-variable concurrency to permission based access control mechanisms. In this informal chalk-talk I will introduce the basics of Separation Logic, providing an overview of the fundamental notions of proof techniques.Bio: John Launchbury is the CTO of Galois, Inc. Prior to founding Galois in 1999, John conducted research and instructed in Computer Science and Engineering at the Oregon Graduate Institute School of Science and Engineering at OHSU. John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society's distinguished dissertation prize.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Tuesday
Jun092009

Tech Talk: Orc in Haskell

The June 16th Galois Tech Talk will be delivered by Trevor Elliott, titled “Orc in Haskell.”

  • Date: Tuesday, June 16th, 2009
  • Time: 10:30am - 11:30am
  • Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204
Abstract: Concurrency is difficult to realize successfully. The Orc language tackles this problem by introducing explicit concurrency as part of its core. It presents a clean, and somewhat monadic, style of programming that should look familiar to Haskell users. I will give a quick introduction to the Orc language, using several examples to motivate its use. Following this introduction, a monadic Haskell embedding of the major features will be presented, bringing a type system to Orc.Bio: Trevor Elliott is a member of the technical staff at Galois, Inc.  His interests center around functional programming, and the effective use of type systems.Slides are available for download.Update: the source is now available on Hackage (though changed from the version presented at this talk).
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Monday
Jun012009

Tech Talk: A Taste of DDT

The June 9th Galois Tech Talk will be delivered by Jim Grundy titled "A Taste of DDT."

  • Date: Tuesday, June 9th, 2009
  • Time: 10:30am - 12:00 noon
  • Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204
Abstract: DDT is a partial implementation of the directed testing approach to test generation. The presentation will likely interest you if you are interested in how directed testing works, or what it is like to use in practice.This seminar presents a rational reconstruction of an experience of using DDT to test a rather rich FIFO/list module implemented in C. The module in question is about 1500 lines of code with a dozen or so entry points. The presentation walks through the user experience of writing and running a first naïve test harness for the module, finding and correcting issues in the code, up to a final declaration of victory.The presentation is rather long, about 1.5 hours, but takes the form of a gently paced walk through a user experience, and as such is rather less taxing on the concentration that you might expect for a talk of its duration.Bio: Jim Grundy is a research scientist with Intel Corporation.  His interests include functional programming, mechanized and interactive reasoning and their application to establishing the correctness of hardware and software systems.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Friday
May152009

EDSLs for Unmanned Autonomous Verification and Validation

We have a new position paper on the use of EDSLs (LwDSLs) for verification and validation of unmanned vehicle avionics, written jointly with John van Enk of DornerWorks, recently presented at a mixed-criticality architecture conference. (Download) :: PDF

Lee Pike, Don Stewart, John Van EnkCPS Week 2009 Workshop on Mixed CriticalityRoadmap to Evolving UAV Certification

We outline a new approach to the verification and validation (V & V) of safety-critical avionics based on the use of executable lightweight domain specific languages - domain-specific languages hosted directly in an existing high-level programming language. We provide examples of LwDSLs used in industry today, and then we describe the advantages of LwDSLs in V & V. We argue the approach promises substantial automation and cost-reduction in V & V.

Click to read more ...