Verasco, a formally verified C static analyzer

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


Duration: 1:03:25
488 views
10

This talk will present the design and soundness proof of Verasco, a formally verified static analyzer for most of the ISO C99 language (excluding recursion and dynamic allocation), developed using the Coq proof assistant. Verasco aims at establishing the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. It include a memory abstract domain, an abstract domain of arithmetical symbolic equalities, an abstract domain of intervals, an abstract domain of arithmetical congruences and an octagonal abstract domain. Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.



Other Videos By Microsoft Research


2016-06-13Speaker Diarization: Optimal Clustering and Learning Speaker Embeddings
2016-06-13Multi-rate neural networks for efficient acoustic modeling
2016-06-13Unsupervised Latent Faults Detection in Data Centers
2016-06-13System and Toolchain Support for Reliable Intermittent Computing
2016-06-13Gates Foundation Presents: Crucial Areas of Fintech Innovation for the Bottom of the Pyramid
2016-06-13Social Computing Symposium 2016: Harassment, Threats, Trolling Online, Diversity in Gaming is Vital
2016-06-13Bringing Harmony Through AI and Economics
2016-06-13Approximating Integer Programming Problems by Partial Resampling
2016-06-13A Lasserre-Based (1+epsilon)-Approximation for Makespan Scheduling with Precedence Constraints
2016-06-13Towards Understandable Neural Networks for High Level AI Tasks - Part 7
2016-06-13Verasco, a formally verified C static analyzer
2016-06-13Future Microprocessors Driven by Dataflow Principles
2016-06-13Theory and Experiments on the Spontaneous Evolution of Culture
2016-06-13Single-shot error correction with the gauge color code
2016-06-13Robust Spectral Inference for Joint Stochastic Matrix Factorization and Topic Modeling
2016-06-13How Much Information Does a Human Translator Add to the Original and Multi-Source Neural Translation
2016-06-13Opportunities and Challenges in Global Network Cameras
2016-06-13Nature in the City: Changes in Bangalore over Time and Space
2016-06-13Making Small Spaces Feel Large: Practical Illusions in Virtual Reality
2016-06-13Machine Learning as Creative Tool for Designing Real-Time Expressive Interactions
2016-06-13Recent Developments in Combinatorial Optimization


Tags:
verasco
static analyzer
microsoft research
program languages and software engineering