Verasco, a formally verified C static analyzer

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


Duration: 1:03:25
51 views
2

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-22Provable Algorithms for Learning Neural Networks
2016-06-22Towards Understandable Neural Networks for High Level AI Tasks
2016-06-22Welcome and Keynote - Geoff Bilder, Director of Strategic Initiatives at CrossRef
2016-06-22Symposium: Brains, Minds and Machines - Surya Ganguli
2016-06-22Symposium: Deep Learning - Xiaogang Wang
2016-06-22Oral Session: Interactive Control of Diverse Complex Characters with Neural Networks
2016-06-22Oral Session: Solving Random Quadratic Systems of Equations-Nearly as Easy as Solving Linear Systems
2016-06-22Towards Understandable Neural Networks for High Level AI Tasks - Part 7
2016-06-22The Once and Future Internet
2016-06-22The First Order World of Galton-Watson Trees
2016-06-22Verasco, a formally verified C static analyzer
2016-06-22Symposium: Deep Learning - Max Jaderberg
2016-06-22Satisfiability of Ordering CSPs Above Average Is Fixed-Parameter Tractable
2016-06-22Symposium: Deep Learning - Harri Valpola
2016-06-22Machine Learning as Creative Tool for Designing Real-Time Expressive Interactions
2016-06-22Symposium: Deep Learning - Sergey Ioffe
2016-06-22Multi-rate neural networks for efficient acoustic modeling
2016-06-22Robust Spectral Inference for Joint Stochastic Matrix Factorization and Topic Modeling
2016-06-22Computational Limits in Statistical Inference: Hidden Cliques and Sum of Squares
2016-06-22Extreme Classification: A New Paradigm for Ranking & Recommendation
2016-06-22A Lasserre-Based (1+epsilon)-Approximation for Makespan Scheduling with Precedence Constraints


Tags:
microsoft research
algorithms