BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:Bottom-up formalization of the ARM architecture - 
 Alastair Reid\, Principal Engineer\, R&amp\;D\, AR
 M Ltd
DTSTART:20120221T130000Z
DTEND:20120221T140000Z
UID:TALK35075AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/35075
DESCRIPTION:Many formal descriptions of processors start with 
 a blank sheet of paper: the authors are free to us
 e any notation and formalisms they wish in creatin
 g their specification.\nThis talk will explore a d
 ifferent approach: working with existing specifica
 tions and the data mining\, engineering and social
  engineering steps needed to develop an accessible
  formal specification that can be widely used both
  by those with formal methods experience and those
  with none.
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:William Denman
END:VEVENT
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:A Proposed Framework for Analysing Security Ceremo
 nies - Jean Martina (Federal University of Santa C
 atarina / Brazil)
DTSTART:20120228T130000Z
DTEND:20120228T140000Z
UID:TALK35575AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/35575
DESCRIPTION:The concept of ceremony as an extension to network
  and security protocols was introduced by Ellison.
  No methods or tools to check correctness or the p
 roperties in such ceremonies are currently availab
 le. The applications for security ceremonies are v
 ast and ll gaps left by strong assumptions in sec
 urity protocols\, like provisioning of cryptograph
 ic keys or correct human interaction. Moreover\, n
 o tools are available to check how knowledge is di
 stributed among human peers and in their interacti
 on with other humans and computers in these scenar
 ios. The key component in this paper is the formal
 isation of human knowledge distribution in securit
 y ceremonies. By properly enlisting human expectat
 ions and interactions in security protocols\, we c
 an minimise the ill-described assumptions we usual
 ly see failing. Taking such issues into account\nw
 hen designing or verifying protocols can help us t
 o better  understand where protocols are more pron
 e to break due to human constraints.
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:William Denman
END:VEVENT
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:Extending deforestation using function invention -
  Will Sonnex (University of Cambridge)
DTSTART:20120306T130000Z
DTEND:20120306T140000Z
UID:TALK36225AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/36225
DESCRIPTION:We present a technique to perform fully automated 
 ML program simplifications beyond that possible th
 rough ordinary deforestation. Our implementation c
 an so far do simplifications such as "length (reve
 rse xs) => length2 xs" and "reverse (xs ++ [n]) =>
  n : reverse2 xs"\, where "length2" and "reverse2"
  are newly invented functions which are alpha-equa
 l to our original "length" and "reverse" functions
 . \n\nThough not yet implemented we believe our te
 chnique can be extended to perform "tree-sort xs =
 > insert-sort xs"\, where "tree-sort = flatten . b
 uild" and "insert-sort" is generated by our method
 . Since our theorem prover "Zeno":http://www.haske
 ll.org/haskellwiki/Zeno has a fully automated proo
 f of the correctness of "insert-sort"\, this would
  give us a fully automated proof of the correctnes
 s of "tree-sort".
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:William Denman
END:VEVENT
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:Title to be confirmed - Magnus Myreen (University 
 of Cambridge)
DTSTART:20120313T130000Z
DTEND:20120313T140000Z
UID:TALK35579AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/35579
DESCRIPTION:Abstract not available
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:William Denman
END:VEVENT
END:VCALENDAR