Bound Analysis of Imperative Programs with the Size-change Abstraction

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


Duration: 50:16
38 views
1

The size-change abstraction (SCA) is an important program abstraction for termination analysis, which has been successfully implemented in many tools for functional and logic programs. In this talk, I will demonstrate that SCA is also a highly effective abstract domain for the bound analysis of imperative programs. I will introduce the first algorithm for bound computation with SCA and discuss how our methodology solves the technical challenges involved in bound computation. Further I will present two program transformations - pathwise analysis and contextualization - that make our SCA-based analysis precise enough to scale to real world programs. I will demonstrate the effectiveness of our approach by experiments with our tool Loopus on the cBench benchmark.



Other Videos By Microsoft Research


2016-07-27Collecting a Heap of Shapes
2016-07-27Automatically Assessing Personality from Speech
2016-07-27Ten User Experience Best Practices for Windows Phone Application Development
2016-07-27Generalization Bounds and Consistency for Latent-Structural Probit and Ramp Loss
2016-07-27Structured Prediction in NLP: Dual Decomposition and Structured Sparsity
2016-07-27High Availability for Database Systems in Cloud Computing Environments
2016-07-27Batches: Unified and Efficient Access to RPC, WS, and SQL Services
2016-07-27Reliable Multithreading through Schedule Memoization
2016-07-27Generalized Oblivious Transfer (GOT)
2016-07-27From Contextual Search to Automatic Content Generation: Scaling Human Editorial Judgment
2016-07-27Bound Analysis of Imperative Programs with the Size-change Abstraction
2016-07-27A mobile context monitoring platform for dynamic mobile computing environments
2016-07-27Privacy Amplification and Non-Malleable Extractors Via Character Sums
2016-07-27Visualization Clusters: from Tiled Displays to Remote Visualization
2016-07-27The Median Hypothesis
2016-07-27Developing Natural Language-based Software Analyses & Tools to Expedite Software Maintenance
2016-07-27Semi-Supervised Learning for Acoustic and Prosodic Modeling in Speech Recognition
2016-07-27Code Bubbles: Making the Vision Real
2016-07-27A novel framework of effective resource management for multi-hop wireless networks
2016-07-27Trajectories and the Extended User Experience
2016-07-27Programming Devices and Services with P - Lecture 1


Tags:
microsoft research