Name: #10 => Jean Yang on An Axiomatic Basis for Computer Programming
Start: 2014-11-18T19:00:00-05:00
End: 2014-11-18T22:00:00-05:00
Location: Viggle Inc

We're thrilled to have Jean Yang (http://jeanyang.com/), PhD student at MIT, presenting on An Axiomatic Basis for Computer Programming (http://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf) by C.A.R. Hoare.

Intro

Our lives now run on software. Bugs are becoming not just annoyances for software developers, but sources of potentially catastrophic failures. A careless programmer mistake could leak our social security numbers or crash our cars. While testing provides some assurance, it is difficult to test all possibilities in complex systems--and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected.

A single paper influenced much of the work towards providing these mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that 1) allows programmers to express program properties and 2) allows these properties to be automatically checked. These ideas have influenced decades of research in automated reasoning about software correctness.

In this talk, I will describe the main ideas in Hoare logic, as well as the impact of these ideas. I will talk about my personal experience using Hoare logic to verify memory guarantees in an operating system. I will also discuss takeaway lessons for working programmers.

Bio

Jean Yang (@jeanqasaur (https://twitter.com/jeanqasaur)) is a final-year PhD student at MIT. For her PhD thesis she has created Jeeves (http://projects.csail.mit.edu/jeeves/), a programming language for automatically enforcing information flow policies for security and privacy. You may be more familiar with one of her other projects, Haskell Ryan Gosling (http://haskellryangosling.tumblr.com/).

Details

This event is sponsored by The Ladders (https://www.theladders.com/) (@TheLaddersDev (https://twitter.com/theladdersdev))

http://photos3.meetupstatic.com/photos/event/9/5/9/8/600_431498296.jpeg

Doors open at 7 pm; the presentation will begin at 7:30 pm; and, yes, there will be beer, water, and pizza.

After Jean presents the paper, we will open up the floor to discussion and questions.

We hope that you'll read the paper before the meetup, but don't stress if you can't. If you have any questions, thoughts, or related information, please visit our *github-thread (https://github.com/papers-we-love/papers-we-love/issues/199)* on the matter.

Additionally, if you have any papers you want to add to the repository above (papers that you love!), please send us a pull request (https://github.com/papers-we-love/papers-we-love/pulls). Also, if you have any ideas/questions about this meetup or the Papers-We-Love org, just open up an issue.

Zeeshan Lakhani

Jeremy Heiler

Brian Bowman

Stephen Olsen

Clint Newsom

Darren Newton

Papers We Love

Technology

Computational Science and Engineering

Computer Programming

Scientific Computing

High Performance Computing

Data Science

#10 => Jean Yang on An Axiomatic Basis for Computer Programming

Viggle Inc

Share

#10 => Jean Yang on An Axiomatic Basis for Computer Programming

Papers We Love

Details

Members are also interested in