{"id":189110,"date":"2013-02-26T00:00:00","date_gmt":"2013-03-01T16:34:03","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/program-analysis-and-symbol-elimination\/"},"modified":"2016-08-02T06:11:46","modified_gmt":"2016-08-02T13:11:46","slug":"program-analysis-and-symbol-elimination","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/program-analysis-and-symbol-elimination\/","title":{"rendered":"Program Analysis and Symbol Elimination"},"content":{"rendered":"<div class=\"asset-content\">\n<p>In this talk we describe how the combination of automated reasoning and symbolic<br \/>\ncomputation methods can be used  to automatically generate statements expressing<br \/>\narbitrarily complex computer program properties. The common method of the the talk<br \/>\nis our recently introduced symbol elimination method. The approach requires no<br \/>\npreliminary knowledge about program behavior, uses the power of a theorem prover<br \/>\nand\/or symbolic computation algorithms, such as Groebner basis computation,<br \/>\nand infers quantified loop invariants and interpolants. We will also present recent<br \/>\ndevelopments of symbol elimination in the Vampire theorem prover.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>In this talk we describe how the combination of automated reasoning and symbolic computation methods can be used to automatically generate statements expressing arbitrarily complex computer program properties. The common method of the the talk is our recently introduced symbol elimination method. The approach requires no preliminary knowledge about program behavior, uses the power of [&hellip;]<\/p>\n","protected":false},"featured_media":197494,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[],"msr-video-type":[206954],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-189110","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-video-type-microsoft-research-talks","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/HCCjW9tUhks\/","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/189110"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/189110\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/197494"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=189110"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=189110"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=189110"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=189110"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=189110"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=189110"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}