[Note the Friday date, instead of the usual Tuesday slot.]The November 13th Galois Tech Talk will be delivered by Rod Chapman, titled “Hoare-Logic – fiddly details and small print.”
- Date: Friday, November 13th, 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: Hoare’s “assignment axiom” is noted for its simplicity and elegance, which seems to suggest that practical implementations are somehow “easy”. This talk will focus on our experience with SPARK – a programming language and toolset whose principal design goal is the provision of a sound Hoare-style verification system. I will concentrate on the “small print” and various fiddly (but essential) langauge features, such as volatility, I/O, dealing with commercial compilers, soundness and so on, that make the system much harder to implement than you might think.Bio: Rod Chapman is a Principal Engineer with Praxis, specializing in the design and implementation of safety and security-critical systems. He currently leads the development of the SPARK language and its associated analysis tools.Rod is a well-known conference speaker and has presented papers, tutorials, and workshops at many international events including SSTC, NSA HCSS, SIGAda, Ada-Europe and the Society of Automotive Engineers (SAE) World Congress. In addition to SPARK, Rod has been the key contributor to many of Praxis’ major projects such as SHOLIS, MULTOS CA, Tokeneer and Software verification tools. He received a MEng in Computer Systems and Software Engineering and a DPhil in Computer Science from the University of York, England, in 1991 and 1995 respectively. He is a Chartered Engineer, a Fellow of the British Computer Society, and also an SEI-Certified PSP Instructor.
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.