BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From Program Logics to Program Analyses And Back - Alexey Gotsman 
 (ARG)
DTSTART:20071120T130000Z
DTEND:20071120T140000Z
UID:TALK8510@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker Alexey Gotsman\n\nIn recent years many ideas initially
  proposed in program logics have been applied to program analysis. For exa
 mple\, ideas from separation logic and its derivatives have been used to d
 esign analyses for checking a variety of properties (such as memory safety
  and noninterference) of programs with different porgramming models (such 
 as procedures and concurrency). However\, to date there has been no proper
  understanding of connections between such analyses and the logics they we
 re inspired by. In this talk I will highlight conceptual and technical con
 troversies arising from this lack of understanding. In order to resolve th
 em\, I will propose a method of co-designing logics and analyses that make
 s the connection between them explicit\, enables using results of analyses
  in interactive theorem proving or proof-carrying code systems\, and avoid
 s giving separate soundness proofs to logics and corresponding analyses. A
 s a case study\, I will consider a modular analysis for concurrent program
 s inspired by concurrent separation logic and show that establishing its u
 nderlying logic leads to an interesting mathematical challenge: it require
 s constructing a non-standard model of concurrent separation logic in whic
 h resource invariants are not required to be precise and the conjunction r
 ule does not hold. 
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR