Frontiers of Computational Reasoning

Dates: 19-20 March 2009
Location: Microsoft Research Cambridge
Organizers: Peter O'Hearn, Hongseok Yang. Host: Tony Hoare
Start Time: Welcome at 09:15am on Thursday 19 March, first talk at 09:30am.

Schedule     Registration     Accomodation and Local Information

The purpose of this workshop is to bring together researchers who work on reasoning, particularly theoreticians that aim to mechanise reasoning for useful application. The sense of ``reasoning'' is intended to be broad and include, e.g., inductive and statistical reasoning as well as traditional deductive inference. The speakers are well-known researchers who have done work in such areas as machine learning, bayesian inference, information theory, inductive logic programming, abductive inference, program verification and analysis, testing, semantic web and knowledge representation, and automatic theorem proving.

Context: In a number of areas we are seeing increasing capabilities in both the speed and form of reasoning performed by computers. Automatic software verification, once but a dream, has seen dramatic advances, due to improvements in proof technology (e.g., SAT, SMT) and the use of methods from static program analysis (abstract interpretation) to discover invariants about programs. Testing is seen as another way of gaining evidence, instead of the opponent of verification, and tests and proofs cooperate. Ideas from classic knowledge representation formalisms have been reborn and extended in the formulation of new logics (description logics), and incorporated into proposals for the Semantic Web. Recent advances on reasoning about data from Information Retrieval have generated various search engines and clustering tools, which completely changed the way that people use Internet. Logic programs perform abduction and induction, as well as deduction. Proof assistants have been used to prove increasingly nontrivial theorems, both in mathematics and in system construction. AI has been revolutionized by the increased use of probability and statistical reasoning, with striking advances and numerous applications in machine learning.

Ultimate Vision: Computers as reasoners. Perhaps one day computers will be as good at reasoning as they are now at numerical calculations, high-speed communication, and high volume storage.

Financial support for the workshop has been provided by Microsoft. The workshop is partly an outgrowth of activitiy on the Verified Software Initiative and the UKCRC Grand Challenge GC6 (Dependable Systems Evolution); funding for GC6-relevant activities is also used to support the workshop.


Day 1. Thursday 19 March.

Day 2. Friday 20 March.


Attendance is free of charge. But you must register for the workshop, to let us guage numbers for lunches (etc), and because it is required by Microsoft. Registration is easy:
Click here to signal your registration
and include your name, organization, position, and address. (If that link doesn't work for you, send email to with subject line ``Attend Reasoning Workshop''.)

There is a limited amount of financial support available for PhD students who attend the workshop. It will be accessed on a first-come-first-served basis. If you would like to know more about this send an email to Peter O'Hearn with subject line ``PhD Funding, Reasoning Workshop''.

Accomodation and Local Information

Directions to Microsoft Research and other local information including taxi numbers and hotels may be found here.

We have made placed rooms at some of these hotels on provisional hold until the 18th February 2009. You can quote the indicated booking references when securing your accomodation.

Crowne Plaza Hotel Cambridge, Downing Street, Cambridge, CB2 3DT.
Tel: 0870 4009180. Email:
£140 per night bed and breakfast.
GROUP REFERENCE TO BE QUOTED: 35845720. Event Name: Microsoft

Arundel House Hotel, Chesterton Road
Cambridge, CB4 3AN
Phone Number: 01223 367701. Fax Number: 01223 367721. E-mail:
Website: £75.00 per room singles, £85.00 per room doubles. Booking reference: Micr1803

University Arms, Regent Street, Cambridge CB2 1AD
Tel: 01223 273 000. Fax: 01223 273 037. £135 per night bed and breakfast. Booking Ref: Microsoft

DoubleTree Hilton, Granta Place, Mill Lane Cambridge CB2 1RT
Telephone: 01223 259988.
£150 per night, bed and breakfast. Booking reference: MICA180309

If you have any questions concerning accomodation or other local matters please contact Rachael Billing at MSR (+44 1223 479766,