BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Generalized\, Efficient Array Decision procedures - Nikolaj Bjorne
 r - Microsoft Research
DTSTART:20091001T130000Z
DTEND:20091001T140000Z
UID:TALK20414@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* \nThe talk concentrates on a particular (newer) fe
 ature of Z3\, the decision procedure for arrays “with additional goodies
 ”. A paper on this topic will appear at FMCAD 2009\, and an accompanying
  technical report is available: http://research.microsoft.com/apps/pubs/?i
 d=102329. The theory of arrays is ubiquitous in the context of automatic s
 oftware and hardware verification and symbolic analysis. The basic array t
 heory was introduced by McCarthy and allows to symbolically representing a
 rray updates. To this date the theory of arrays itself remains fundamental
  to how modern program verification\, test-case generation\, and model-bas
 ed program tools model program heaps and higher level data-types\, such as
  sets and finite maps. We present combinatory array logic\, CAL\, using a 
 small\, but powerful core of combinators\, and reduce it to the theory of 
 uninterpreted functions. CAL allows expressing properties that go well bey
 ond the basic array theory. For example\, CAL allows some of the more comm
 on operations on sets and multi-sets. CAL does not allow expressing the id
 entity combinator I. CAL+I on the other hand allows encoding arbitrary lam
 bda terms. We provide a new efficient decision procedure for the base arra
 y theory as well as CAL. The efficient procedure serves a critical role in
  the performance of the state-of-the-art SMT solver Z3 on array formulas f
 rom applications. Note that this is joint work with Leonardo de Moura \n\n
 *Biography:*\nDr. Nikolaj Bjorner is working with Leonardo de Moura on a n
 ext generation SMT constraint solver Z3. Z3 is used for program verificati
 on and test case generation. Nikolaj is also managing the Foundations of S
 oftware Engineering group at Microsoft Research. Until 2006\, he was in th
 e Core File Systems group where he designed and implemented the core of DF
 S-R which is included as part of Windows Server 2003 R2\, Windows Live Mes
 senger (Sharing Folders)\, and Vista Meetings Space. He also designed some
  of the chunking utilities used in the remote differential compression pro
 tocol RDC. \n
LOCATION:Lecture-room large (126 seats) Microsoft Research Ltd\, Roger Nee
 dham Building\, 7 J J Thomson Avenue (Off Madingley Road)\, CB3 0FB
END:VEVENT
END:VCALENDAR