University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Model Checking: Reasoning about Parameterized Loop Programs sans Loop Invariants

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Model Checking: Reasoning about Parameterized Loop Programs sans Loop Invariants

Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

VSO2 - Verified software

We consider the class of programs with sequentially composed and/or nested loops, where the iteration count of each loop depends on a (set of) parameters.  Examples of such programs include those that manipulate data structures of parametric sizes, or iteratively compute scalar functions of the parameters.  Properties of such programs can often be expressed as parameterized Hoare triples, where the pre- and post-conditions depend on the same parameters on which the loop iteration bounds depend.  We present a technique called generalized full-program induction for reasoning about a large class of such programs that bypass the need for generating loop invariants for each loop.  This approach effectively shifts the granularity of inductive reasoning from individual loops to the entire program comprised of possibly many loops.  

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

ssb Type the title of a new list here Common Room (First Floor) David Attenborough Building, University of Cambridge Pembroke St, Cambridge CB2 3QZ

Other talks

Tea and Coffee Break TBC Genomic Medicine CPC Cambridge RNA Club - IN PERSON TOWARD AFFORDABLE PREVENTIVE HEALTHCARE: How basic science addresses grand challenges Christmas Social Evening & Annual General Meeting
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity