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

Model Checking: Reasoning about Parameterized Loop Programs sans Loop Invariants

Add to your list(s) 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity