{"id":170031,"date":"2008-12-01T20:34:07","date_gmt":"2008-12-01T20:34:07","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/speed-symbolic-timespace-bound-analysis\/"},"modified":"2019-08-19T15:40:50","modified_gmt":"2019-08-19T22:40:50","slug":"speed-symbolic-timespace-bound-analysis","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/speed-symbolic-timespace-bound-analysis\/","title":{"rendered":"SPEED (Symbolic Resource Time\/Space Bounds Analysis)"},"content":{"rendered":"<h1>Introduction<\/h1>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"alignleft\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2016\/01\/speed-symbolic-timespace-bound-analysis-241x300.gif\" alt=\"\" width=\"95\" height=\"118\" \/>Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause before shipping). The SPEED project attempts to address these limitations by static estimation of symbolic computational complexity of programs. It builds over recent advances in static program analysis, which has traditionally been used for checking correctness as opposed to measuring performance.<\/p>\n<p>Computing symbolic complexity bounds is a challenging problem since such bounds for even simple sequential programs are usually disjunctive, non-linear, and involve numerical properties of heaps. Sometimes even proving termination is hard (Remember halting problem is undecidable!), and computing bounds ought to be a harder problem. The SPEED tool implements several algorithmic techniques for statically estimating the worst-case symbolic computational complexity of procedures in terms of their scalar inputs and user-defined quantitative functions of input data-structures (such as length of a list, or height of a tree). It attempts to generate complexity bounds that are usually precise not only in terms of the computational complexity, but also in terms of the constant factors.<\/p>\n<p>Such automatically generated bounds are very useful for early detection of egregious performance problems in large modular codebases that are constantly being changed by multiple developers who make heavy use of code written by others without a good understanding of their implementation complexity.<\/p>\n\t\t\t<div class=\"moray-accordion\" data-show=\"false\">\n\t\t\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t\t<div\n\t\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\t\trole=\"group\"\n\t\t\t\t\t\tdata-mount=\"collapse-controls\"\n\t\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t\t\tdata-target=\"#accordion-1\">\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"expand\" type=\"button\" data-bi-cN=\"Expand all\">Expand all<\/button>\n\t\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t\t<button class=\"btn btn-link m-0\" aria-disabled=\"false\" aria-pressed=\"false\" data-action=\"collapse\" type=\"button\" data-bi-cN=\"Collapse all\">Collapse all<\/button>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t<ul class=\"accordion\" id=\"accordion-1\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t<li class=\"m-0\">\n\t\t\t<h4 class=\"accordion-header\">\n\t\t\t\t<button\n\t\t\t\t\tclass=\"btn btn-collapse m-0\"\n\t\t\t\t\ttype=\"button\"\n\t\t\t\t\tdata-mount=\"collapse\"\n\t\t\t\t\tdata-target=\"#collapse-2\"\n\t\t\t\t\taria-expanded=\"false\"\n\t\t\t\t\taria-controls=\"collapse-2\">\n\t\tPeople Involved\t\t\t\t<\/button>\n\t\t\t<\/h4>\n\t\t\t<div class=\"collapse\" id=\"collapse-2\">\n\t\t\t\t<div class=\"accordion-body\">\n\t\t\t\t\t\t\t\t\t\t<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cse.iitb.ac.in\/~bhargav\/\">Bhargav Gulavani<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (IIT Bombay)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cse.iitk.ac.in\/\">Sagar Jain<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (UC Berkeley)<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.cl.cam.ac.uk\/~ejk39\/\">Eric Koskinen<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> (University of Cambridge)<\/li>\n<li>Florian Zuleger (TU Darmstadt)<\/li>\n<\/ul>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t<\/li>\n\t\t\t\t\t\t\t\t\t<\/ul>\n\t\t<\/div>\n\t\t\n","protected":false},"excerpt":{"rendered":"<p>Introduction Performance measurement of software is a critical component of software development. Performance is traditionally measured using profiling, which is often too little (only certain inputs are profiled) or too late (to make requisite changes to address the root cause before shipping). The SPEED project attempts to address these limitations by static estimation of symbolic [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170031","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-12-01","related-publications":[158296,335945,336362,336410,336503,336542,359375,157213],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Sumit Gulwani","user_id":33755,"people_section":"Group 1","alias":"sumitg"}],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170031"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170031\/revisions"}],"predecessor-version":[{"id":604431,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170031\/revisions\/604431"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170031"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170031"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170031"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170031"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170031"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}