BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Model Checking: Reasoning about Parameterized Loop Programs sans L
 oop Invariants - Supratik Chakraborty (Indian Institute of Technology)
DTSTART:20220722T083000Z
DTEND:20220722T091500Z
UID:TALK176267@talks.cam.ac.uk
DESCRIPTION:We consider the class of programs with sequentially composed a
 nd/or nested loops\, where the iteration count of each loop depends on a (
 set of) parameters.&nbsp\; Examples of such programs include those that ma
 nipulate data structures of parametric sizes\, or iteratively compute scal
 ar functions of the parameters.&nbsp\; Properties of such programs can oft
 en be expressed as parameterized Hoare triples\, where the pre- and post-c
 onditions depend on the same parameters on which the loop iteration bounds
  depend.&nbsp\; We present a technique called generalized full-program ind
 uction for reasoning about a large class of such programs that bypass the 
 need for generating loop invariants for each loop.&nbsp\; This approach ef
 fectively shifts the granularity of inductive reasoning from individual lo
 ops to the entire program comprised of possibly many loops.\n&nbsp\;
LOCATION:Seminar Room 2\, Newton Institute
END:VEVENT
END:VCALENDAR