Generalized, Efficient Array Decision procedures

Add to your list(s) Download to your calendar using vCal

• Nikolaj Bjorner - Microsoft Research
• Thursday 01 October 2009, 14:00-15:00
• Lecture-room large (126 seats) Microsoft Research Ltd, Roger Needham Building, 7 J J Thomson Avenue (Off Madingley Road), CB3 0FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: The talk concentrates on a particular (newer) feature 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/?id=102329. The theory of arrays is ubiquitous in the context of automatic software and hardware verification and symbolic analysis. The basic array theory was introduced by McCarthy and allows to symbolically representing array updates. To this date the theory of arrays itself remains fundamental to how modern program verification, test-case generation, and model-based 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 beyond the basic array theory. For example, CAL allows some of the more common operations on sets and multi-sets. CAL does not allow expressing the identity combinator I. CAL +I on the other hand allows encoding arbitrary lambda terms. We provide a new efficient decision procedure for the base array 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 from applications. Note that this is joint work with Leonardo de Moura

Biography: Dr. Nikolaj Bjorner is working with Leonardo de Moura on a next generation SMT constraint solver Z3. Z3 is used for program verification and test case generation. Nikolaj is also managing the Foundations of Software Engineering group at Microsoft Research. Until 2006, he was in the Core File Systems group where he designed and implemented the core of DFS -R which is included as part of Windows Server 2003 R2, Windows Live Messenger (Sharing Folders), and Vista Meetings Space. He also designed some of the chunking utilities used in the remote differential compression protocol RDC .

This talk is part of the Microsoft Research Cambridge, general interest public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Centre for Health Leadership and Enterprise
• Chris Davis' list
• Featured lists
• Featured talks
• Guy Emerson's list
• Interested Talks
• Lecture-room large (126 seats) Microsoft Research Ltd, Roger Needham Building, 7 J J Thomson Avenue (Off Madingley Road), CB3 0FB
• Major Public Lectures in Cambridge
• Microsoft Research Cambridge, public talks
• Neurons, Fake News, DNA and your iPhone: The Mathematics of Information
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• custom
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.