Automatically proving the termination of C programs

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=Vu1hNtkecgY


Duration: 1:06:08
121 views
2

In this talk I will discuss Terminator, the first known automatic program termination proven to support large programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers. Terminator is based on a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. Additionally, to increase the proof power, Terminator computes inductive invariants of the program when checking the lemmas that imply termination. The talk will close with results from recent experiments with Terminator on dispatch routines from Windows device drivers. This is joint work with Andreas Podelski and Andrey Rybalchenko.



Other Videos By Microsoft Research


2016-09-06Sensor Networks Workshop 05 - Environmentally Immersive Programming
2016-09-06Sensor Networks Workshop 05 - Sensor Networks and Ubiquitous Computing
2016-09-06Sensor Networks Workshop 05 - Second Generation Sensor Querying
2016-09-06Sensor Networks Workshop 05 - Life Under Your Feet: Using WSN in Soil Ecology
2016-09-06Sensor Networks Workshop 05 - Embedded Networked Sensing Redux
2016-09-06Towards Expressive and Scalable Publish/Subscribe    
2016-09-06Extending the Internet Architecture to Sensor Networks: Some Open Questions
2016-09-06India's Emerging Competitiveness
2016-09-06Towards a Service-Oriented Architecture for Reconfigurable Networked Embedded Sensor Systems
2016-09-06Extracting Product Features and Opinions from Reviews
2016-09-06Automatically proving the termination of C programs
2016-09-06From Dust to Doctors: Wireless Sensor Networks for Medical Applications     
2016-09-05Interactive Machine Learning: Leveraging Human Intelligence
2016-09-05Sound Transaction-based Reduction without Cycle Detection
2016-09-05SSCLI RFP II Capstone Workshop ΓÇô Aspect.NET - An Aspect-Oriented Programming Tool for .NET
2016-09-05SSCLI RFP II Capstone Workshop ΓÇô Typed Compilation of .NET Common Intermediate Language
2016-09-05SSCLI RFP II Capstone Workshop - A Hardware-Based CIL-Machine
2016-09-05Static Analysis for Identifying and Allocating Clusters of Immortal Objects
2016-09-05SSCLI RFP II Capstone Workshop - Parallel, Real-Time Garbage Collection in Rotor
2016-09-05SSCLI RFP II Capstone Workshop - Xtatic: Native XML Processing for C#
2016-09-05SSCLI RFP II Capstone Workshop - The Grid-Occam Project


Tags:
microsoft research