Tech Talk: A Newbie’s Exploration of Separation Logic

  • Date  Time
  • Speaker
  • Location

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.