Model Checking: Reasoning about Parameterized Loop Programs sans Loop Invariants

Add to your list(s) Download to your calendar using vCal

• Supratik Chakraborty (Indian Institute of Technology)
• Friday 22 July 2022, 09:30-10:15
• Seminar Room 2, Newton Institute.

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:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 2, Newton Institute
• bld31

Note that ex-directory lists are not shown.