BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Constraint-Programming Framework For Bounded Program Verificatio
 n - Helene Collavizza (Ecole Polytechnique Universitaire de Nice Sophia An
 tipolis)
DTSTART:20080311T130000Z
DTEND:20080311T140000Z
UID:TALK9888@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker: Helene Collavizza\n\nIn this talk\, we will present a
  framework for verifying the conformity of a program with its specificatio
 n using constraint programming. This framework uses constraints to represe
 nt sets of memory stores and explores execution paths over these constrain
 t stores. The input program is\npartially correct if each constraint store
  produced by constraint-based execution implies the postcondition. One mai
 n benefit of this approach is that it does not\nexplore spurious execution
  paths as it incrementally prunes paths by an early detection of inconsist
 ent constraint stores. We will present the approach\, then introduce const
 raint programming\, and then illustrate the\nframework on a number of exam
 ples to highlight its functionalities and give some preliminary performanc
 e results.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR