{"id":169817,"date":"2001-11-05T12:19:12","date_gmt":"2001-11-05T20:19:12","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/slam\/"},"modified":"2017-06-16T15:41:42","modified_gmt":"2017-06-16T22:41:42","slug":"slam","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/slam\/","title":{"rendered":"SLAM"},"content":{"rendered":"<p>SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine.<\/p>\n<p><span id=\"0d41d62e-96bd-442a-8b73-b0f29aba70cf\" class=\"ImageBlock fn\"><i><img decoding=\"async\" id=\"Image0d41d62e-96bd-442a-8b73-b0f29aba70cf\" class=\"alignright\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/slam-slam_metallic.gif\" alt=\"\" \/>&#8220;Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we\u2019re building tools that can do actual proof about the software and how it works in order to guarantee the reliability.&#8221;<\/i> <b>Bill Gates, April 18, 2002. <\/b><a href=\"http:\/\/www.microsoft.com\/billgates\/speeches\/2002\/04-18winhec.asp\"><b>Keynote address<\/b><\/a><b> at <\/b><a href=\"http:\/\/www.microsoft.com\/winhec\/\"><b>WinHec 2002<\/b><\/a><\/span><\/p>\n\t<div data-wp-context='{\"items\":[]}' data-wp-interactive=\"msr\/accordion\">\n\t\t\t\t\t<div class=\"clearfix\">\n\t\t\t\t<div\n\t\t\t\t\tclass=\"btn-group align-items-center mb-g float-sm-right\"\n\t\t\t\t\tdata-bi-aN=\"accordion-collapse-controls\"\n\t\t\t\t>\n\t\t\t\t\t<button\n\t\t\t\t\t\tclass=\"btn btn-link m-0\"\n\t\t\t\t\t\tdata-bi-cN=\"Expand all\"\n\t\t\t\t\t\tdata-wp-bind--aria-controls=\"state.ariaControls\"\n\t\t\t\t\t\tdata-wp-bind--aria-expanded=\"state.ariaExpanded\"\n\t\t\t\t\t\tdata-wp-bind--disabled=\"state.isAllExpanded\"\n\t\t\t\t\t\tdata-wp-class--inactive=\"state.isAllExpanded\"\n\t\t\t\t\t\tdata-wp-on--click=\"actions.onExpandAll\"\n\t\t\t\t\t\ttype=\"button\"\n\t\t\t\t\t>\n\t\t\t\t\t\tExpand all\t\t\t\t\t<\/button>\n\t\t\t\t\t<span aria-hidden=\"true\"> | <\/span>\n\t\t\t\t\t<button\n\t\t\t\t\t\tclass=\"btn btn-link m-0\"\n\t\t\t\t\t\tdata-bi-cN=\"Collapse all\"\n\t\t\t\t\t\tdata-wp-bind--aria-controls=\"state.ariaControls\"\n\t\t\t\t\t\tdata-wp-bind--aria-expanded=\"state.ariaExpanded\"\n\t\t\t\t\t\tdata-wp-bind--disabled=\"state.isAllCollapsed\"\n\t\t\t\t\t\tdata-wp-class--inactive=\"state.isAllCollapsed\"\n\t\t\t\t\t\tdata-wp-on--click=\"actions.onCollapseAll\"\n\t\t\t\t\t\ttype=\"button\"\n\t\t\t\t\t>\n\t\t\t\t\t\tCollapse all\t\t\t\t\t<\/button>\n\t\t\t\t<\/div>\n\t\t\t<\/div>\n\t\t\t\t<ul class=\"msr-accordion\">\n\t\t\t\t\t\t\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-2\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-2\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-1\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tWhat&#039;s New\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-1\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-2\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\t\t\t\t<h2>What&#8217;s New?<\/h2>\n<p><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-yogi-project\/\"><strong>Yogi<\/strong> <\/a>is now available to plug into the Static Driver Verifier Research Platform. To install SDVRP and Yogi, see this <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/yogi-readme.txt\" target=\"_self\">README<\/a>.<\/p>\n<p><strong>The Summer (2011) of SLAM saw <\/strong>two awards and a retrospective article in CACM:<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.sigplan.org\/award-pldi.htm\">Most Influential PLDI Paper award<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> for <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/portal.acm.org\/citation.cfm?doid=378795.378846\">Automatic Predicate Abstraction of C Programs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.informatik.uni-trier.de\/~ley\/db\/conf\/pldi\/pldi2001.html\">PLDI 2001<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>. The first conference paper from the SLAM project.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.cs.utah.edu\/events\/conferences\/cav2011\/\" target=\"_blank\">CAV 2011<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> Award. Citation: &#8220;The 2011 CAV Award is given to Thomas Ball and Sriram Rajamani, both at Microsoft Research, for their contributions to software model checking,specifically the development of the SLAM\/SDV software model checker that successfully demonstrated computer-aided verification techniques on real programs.&#8221;<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/portal.acm.org\/citation.cfm?doid=1965724.1965743\">A Decade of Software Model Checking with SLAM<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, V. Levin, S. K. Rajamani, Communications of the ACM, Vol. 54. No. 7, 2011, Pages 68-76<\/li>\n<\/ul>\n<p><strong>Paper<\/strong>:<\/p>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/slam-slam2_fmcad2010_final.pdf\" target=\"_self\">SLAM2: Static Driver Verification with Under 4% False Alarms<\/a>, T. Ball, E. Bounimova, R. Kumar, V. Levin, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/fmcad10.iaik.tugraz.at\/\" target=\"_blank\">FMCAD 2010<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p><strong>The Static Driver Verifier Research Platform\u00a0(SDVRP)<\/strong> is a release of SDV\/SLAM for academic research. It allows the creation and checking of API-specific rules and programs\u00a0(for general APIs and programs, not just driver APIs and drivers) and contains a repository of Boolean programs and test results.<\/p>\n<ul>\n<li><strong>To get started:<\/strong>\n<ul>\n<li>Read\u00a0the README in the tab below<\/li>\n<li>Download\/install the <a href=\"http:\/\/www.microsoft.com\/whdc\/DevTools\/WDK\/WDKpkg.mspx\" target=\"_self\">Windows 7 Driver Kit<\/a> (you will want a <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/en.wikipedia.org\/wiki\/Virtual_drive\" target=\"_blank\">virtual drive <span class=\"sr-only\"> (opens in new tab)<\/span><\/a>to install the download, as it is available only as a DVD ISO image)<\/li>\n<li>Download\/install SDVRP<\/li>\n<\/ul>\n<\/li>\n<li><strong>Slide deck.<\/strong> [<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/slam-sdvrp.ppt\" target=\"_self\">ppt<\/a>, <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/slam-sdvrp.pdf\" target=\"_self\">pdf<\/a>]<\/li>\n<li><strong>Paper<\/strong>. <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/slam-sdvrpcav2010.pdf\" target=\"_self\">The Static Driver Verifier Research Platform<\/a>, Thomas Ball, Ella Bounimova, Vladimir Levin, Rahul Kumar, Jakob Lichtenberg, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.floc-conference.org\/CAV-home.html\" target=\"_blank\">CAV 2010<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> tools paper<\/li>\n<li><strong>Questions?<\/strong> E-mail us at <a href=\"mailto:sdvrpdis@microsoft.com\">sdvrpdis@microsoft.com<\/a><\/li>\n<\/ul>\n<p><strong>Pointers in SLAM2<\/strong>. <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/axioms.submitted.pdf\" target=\"_self\">Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2<\/a>,\u00a0Thomas Ball, Ella Bounimova, Vladimir Levin, Leonardo de Moura, March 2010, MSR-TR-2010-24<\/p>\n<p><strong>Congratulations<\/strong> to the Driver Quality Team on winning a 2009 Engineering Excellence Award for &#8220;Improving Driver Quality thru Static Verification&#8221;. <i>Jon Hagen, Vlad Levin, Adam Shapiro, Donn Terry, Abdullah Ustuner. <\/i><strong>PRE<i>f<\/i>ast for Drivers<\/strong> scans the driver code for issues with concurrency, proper IRQL handling, and a host of other driver challenges. The <strong>Static Driver Verifier<\/strong> simulates a hostile environment and systematically tests all code paths, looking for driver model violations. These complementary tools provide both quick and deep driver testing. Both tools have been adopted broadly within Windows and with third-party developers through MSDN and the Windows Driver Kit.<\/p>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-4\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-4\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-3\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tStatic Driver Verifier Research Platform README\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-3\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-4\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\t\t\t\t<h2>Overview of Static Driver Verifier Research Platform<\/h2>\n<p>Static Driver Verifier (SDV) is a compile-time static verification tool, included in the Windows Driver Kit (WDK). The SDV Research Platform (SDVRP) is an extension to SDV that allows you to adapt SDV to:<\/p>\n<ul>\n<li>Support additional frameworks (or APIs) and write custom SLIC rules for this framework.<\/li>\n<li>Experiment with the model checking step.<\/li>\n<\/ul>\n<p>This file provides the following sections:<\/p>\n<ul>\n<li>Getting Started<\/li>\n<li>Documentation<\/li>\n<li>Installation Instructions<\/li>\n<\/ul>\n<p>Notice: Links in this file are relative and will only work after installation of SDVRP, when this file is opened from the Start -> All Programs -> Microsoft Static Driver Verifier folder.<\/p>\n<h2>Getting Started<\/h2>\n<ul>\n<li>Obtain and install WDK and SDVRP (See section Installation Instructions beneath).<\/li>\n<li>Understand SDV: See staticdv.chm, in particular sections &#8220;Static Driver Verifier Concepts&#8221; and the &#8220;<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/download.microsoft.com\/download\/9\/c\/5\/9c5b2167-8017-4bae-9fde-d599bac8184a\/sdv-wdm_lab.docx\">Static Driver Verifier for WDM Drivers: WHDC Lab<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>&#8221; article on the WHDC SDV web site <a href=\"http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/sdv.mspx\">http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/sdv.mspx<\/a>.<\/li>\n<li>Try the SDVRP Custom Framework. See SDVRP.docx\u2019s &#8220;Walk Through: fail_driver1&#8221;.<\/li>\n<li>Read the rest of SDVRP.docx and SLIC.docx and start experimenting on your own.<\/li>\n<\/ul>\n<h2>Documentation<\/h2>\n<p>After installation the following documents are available in the Start -> All Programs -> Microsoft Static Driver Verifier folder:<\/p>\n<ul>\n<li>README.htm: This file.<\/li>\n<li>SDVRP.docx: SDVRP Documentation. This is the primary document supporting SDVRP development; however it does not cover the details of the SLIC language, or the basic operation of SDV. These topics are covered by SLIC.docx and staticdv.chm (see beneath).<\/li>\n<li>SLIC.docx: SLIC Documentation. Syntax and semantics of SLIC, the rule specification language of SDV.<\/li>\n<li>bebop.docx: Bebop Documentation. Syntax and semantics of Boolean Programs, the internal language used for the model checking step in SDV. Instructions on how to run on the Bebeop Boolean Program Test Suite.<\/li>\n<li>staticdv.chm: SDV Documentation. This is the documentation provided with the regular version of Static Driver Verifier. It does not cover the SDVRP extensions. This document is also included in the Windows Driver Kit Documentation.<\/li>\n<li>License.rtf: License Agreement. This license is also presented during download and installation.<\/li>\n<\/ul>\n<h2>Installation Instructions<\/h2>\n<ul>\n<li>Install the WDK.\n<ul>\n<li>What: The SDVRP requires that the (freely available) Windows Driver Kit Version 7.1.0 (WDK) first be installed. The WDK contains compiler, build environment, and supporting tools that is required to use SDV.<\/li>\n<li>See <a href=\"http:\/\/www.microsoft.com\/whdc\/driver\/wdk\/\">http:\/\/www.microsoft.com\/whdc\/driver\/wdk\/<\/a> for information about obtaining the WDK. (As of this writing under: How to Get the WDK -> Microsoft Download Center).<\/li>\n<li>Recommend default selection of Features and Location.<\/li>\n<li>Notice: The WDK will be installed to &#8220;%SystemDrive%\\WinDDK\\7600.16385.1&#8221;.<\/li>\n<\/ul>\n<\/li>\n<li>Install the SDVRP.\n<ul>\n<li>What: The SDVRP contains a customized version of SDV that can be used for rule development.<\/li>\n<li>Recommend default selection of Features and Installation Path. Installation Path must be a path with no spaces in path name.<\/li>\n<li>Notice: The SDVRP will be installed to &#8220;%SystemDrive%\\WinDDK\\SDV&#8221;.<\/li>\n<\/ul>\n<\/li>\n<li>Confirm the WDK use the SDVRP version of SDV:\n<ul>\n<li>What: The WDK already has SDV available (in the &#8220;tools\\sdv&#8221; folder), but this WDK version of SDV is not useable for SDVRP work. The WDK build environment should automatically detect that SDVRP is installed and use the SDVRP version of SDV.<\/li>\n<li>Open a &#8220;Windows Win7 x86 Free Build Environment&#8221; window (from All Programs -> Windows Driver Kits -> 7600.16385.1 -> Build Environments -> Windows 7 -> x86 Free Build Environment)<\/li>\n<li>Validate that this line is printed when you start the build environment: &#8220;WARNING: Using external version of Static Driver Verifier.&#8221;<\/li>\n<li>In case of trouble you should look at the script %SystemDrive%\\WinDDK\\7600.16385.1\\bin\\setenv.bat, search for SDV.<\/li>\n<\/ul>\n<\/li>\n<li>The SDVRP is now ready for use.<\/li>\n<\/ul>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-6\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-6\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-5\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tResources\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-5\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-6\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\t\t\t\t<h2>Publications<\/h2>\n<h4>Book Chapter<\/h4>\n<ul>\n<li><a href=\"http:\/\/www.microsoft.com\/MSPress\/books\/10512.aspx\"><b><i>Developing Drivers with the Windows\u00ae Driver Foundation<\/i><\/b><\/a>, a Microsoft Press book, is now in print, including a chapter about Static Driver Verifier, which has new rules to enable analysis of drivers written against the Kernel-model Driver Framework API.<\/li>\n<\/ul>\n<h4>History<\/h4>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/springerlink.metapress.com\/content\/ek3l4u815vl3aexk\/\" target=\"_blank\">SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>,<b> <\/b>T. Ball, B. Cook, V. Levin and S. K. Rajamani, <em>Integrated Formal Methods 2004 <\/em><\/li>\n<\/ul>\n<h4>The SLAM Process<\/h4>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/doi.acm.org\/10.1145\/1217935.1217943\" target=\"_blank\">Thorough Static Analysis of Device Drivers<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani and A. Ustuner, <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cs.kuleuven.ac.be\/conference\/EuroSys2006\/\"><i>EuroSys 2006<\/i><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/doi.acm.org\/10.1145\/503272.503274\" target=\"_blank\">The SLAM Project: Debugging System Software via Static Analysis<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. K. Rajamani, <i>POPL 2002<\/i>, January 2002, pages 1-3.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/portal.acm.org\/citation.cfm?id=380932&dl=GUIDE&coll=GUIDE&CFID=17227094&CFTOKEN=26163906\" target=\"_blank\">Automatically Validating Temporal Safety Properties of Interfaces<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. K. Rajamani, <em>SPIN 2001 Workshop on Model Checking of Software, <\/em>LNCS 2057, May 2001, pp. 103-122.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/eprints.kfupm.edu.sa\/29667\/\">Checking Temporal Properties of Software with Boolean Programs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. K. Rajamani, Workshop on Advances in Verification (with CAV 2000)<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/boolean-programs-a-model-and-process-for-software-analysis\/\">Boolean Programs: A Model and Process for Software Analysis<\/a>, T. Ball, S. K. Rajamani, MSR Technical Report 2000-14.<\/li>\n<\/ul>\n<h4>SLAM Specifications<\/h4>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/slic-a-specification-language-for-interface-checking-of-c\/\">SLIC: A Specification Language for Interface Checking<\/a>, T. Ball, S. K. Rajamani, MSR-TR-2001-21.<\/li>\n<\/ul>\n<h4>Boolean Programs<\/h4>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/portal.acm.org\/citation.cfm?id=379605.379690&coll=ACM&dl=ACM&type=series&idx=SERIES118&part=series&WantType=Proceedings&title=PASTE&CFID=15151515&CFTOKEN=6184618\" target=\"_blank\">Bebop: A Path-sensitive Interprocedural Dataflow Engine<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. K. Rajamani, <i>PASTE 2001<\/i><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.springerlink.com\/content\/h437381h7n31308u\/\" target=\"_blank\">Bebop: A Symbolic Model Checker for Boolean Programs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. K. Rajamani, <em>SPIN 2000 Workshop on Model Checking of Software<\/em>, LNCS 1885, August\/September 2000, pp. 113-130.<\/li>\n<\/ul>\n<ul>\n<li><em>Predicate Abstraction of C Programs<\/em>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/portal.acm.org\/citation.cfm?id=1057387.1057391\">Polymorphic Predicate Abstraction<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, T. Millstein, S. K. Rajamani, <i>ACM TOPLAS Vol. 27, No. 2, March 2005, pages 314-343<\/i><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/portal.acm.org\/citation.cfm?id=381694.378846\" target=\"_blank\">Automatic Predicate Abstraction of C Programs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, R. Majumdar, T. Millstein, S. K. Rajamani, <i>PLDI 2001, <\/i>SIGPLAN Notices 36(5), pp. 203-213.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/portal.acm.org\/citation.cfm?id=646485.759192\" target=\"_blank\">Boolean and Cartesian Abstractions for Model Checking C Programs<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><strong>,<\/strong> T. Ball, A. Podelski, S. K. Rajamani, <i>TACAS 2001<\/i><i>, <\/i>LNCS 2031, April 2001, pp. 268-283<em>.<\/em><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/dx.doi.org\/10.1007\/11513988_5\" target=\"_blank\">Predicate Abstraction via Symbolic Decision Procedures<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, S. Lahiri, T. Ball, B. Cook, <i>CAV 2005<\/i><i>.<\/i><\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<h4>Abstraction Refinement<\/h4>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.springerlink.com\/content\/j23v3cuy91m050q7\/\" target=\"_blank\">Refining Approximations in Software Predicate Abstraction<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, B. Cook, S. Das, S. K. Rajamani. TACAS 2004.<\/li>\n<li>Generating Abstract Explanations of Spurious Counterexamples in C Programs,\u00a0T. Ball, S. K. Rajamani, MSR-TR-2002-09.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.springerlink.com\/content\/ygrv6q95uw2tdd0u\/\" target=\"_blank\">Relative Completeness of Abstraction Refinement for Software Model Checking<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, A. Podelski, S. K. Rajamani, <i>TACAS 2002<\/i><i>,<\/i> LNCS 2280, April 2002, pp. 158-172.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.springerlink.com\/content\/086whu4jlmy1tlyr\/\" target=\"_blank\">Zapato: Automatic theorem proving for predicate abstraction refinement<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, B. Cook, S. K. Lahiri and L. Zhang, Tools paper in CAV 2004<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.springerlink.com\/content\/hk552416k67w4560\/\" target=\"_blank\">Formalizing Counterexample-driven Refinement with Weakest Preconditions<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, <em>Proceedings of the NATO Advanced Study Institute on Engineering Theories of Software Intensive Systems Marktoberdorf,<\/em> Germany 3\u201315 August 2004.<\/li>\n<\/ul>\n<h4>Concurrency<\/h4>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.springerlink.com\/content\/2hgr5luqvhcmqcbk\/\" target=\"_blank\">Parameterized Verification of Multithreaded Software Libraries<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. Chaki, S. K. Rajamani,<i>TACAS 2001<\/i>, LNCS 2031, April 2001, pp. 158-173.<\/li>\n<\/ul>\n<h4>Miscellaneous<\/h4>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/doi.acm.org\/10.1145\/640128.604140\" target=\"_blank\">From Symptom to Cause: Localizing Errors in Counterexample Traces<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, M. Naik, S. K. Rajamani, <em>POPL 2003<\/em><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/2477\/24770230.htm\" target=\"_blank\">Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, S. Adams, T. Ball, M. Das, S. Lerner, S. K. Rajamani, M. Seigle, W. Weimer. <i>SAS 2002, LNCS 2477<\/i><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/springerlink.metapress.com\/openurl.asp?genre=article&issn=0302-9743&volume=2988&spage=93\" target=\"_blank\">Automatic Creation of Environment Models via Training<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, V. Levin, and F. Xie, <em>TACAS 2004<\/em><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/2102\/21020260.htm\" target=\"_blank\">The SLAM Toolkit<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, T. Ball, S. K. Rajamani<i>, <\/i><i>CAV 2001<\/i><\/li>\n<\/ul>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-8\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-8\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-7\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tNews\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-7\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-8\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\t\t\t\t<h2>News<\/h2>\n<ul>\n<li><b>Wired News: <\/b><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.wired.com\/news\/technology\/bugs\/0,2924,69375,00.html\"><b>Microsoft&#8217;s Secret Bug Squasher<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.nzz.ch\/2005\/10\/14\/em\/articleD825L.html\">Kampf dem Programmierfehlerteufel<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>SDV and PPRC tools mentioned in <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.economist.com\/science\/tq\/displayStory.cfm?story_id=1841081\">The Economist<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>From reporting of the Microsoft Research Roadshow in Silicon Valley (<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.pcmag.com\/article2\/0,4149,1033970,00.asp\"><b>PC Magazine<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a>)<\/li>\n<li>SLAM and PPRC tools featured in <b>Bill Gates<\/b>&#8216; <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/oopsla.acm.org\/\">OOPSLA 2002<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>\u00a0<a href=\"http:\/\/www.microsoft.com\/billgates\/speeches\/2002\/11-08oopsla.asp\">keynote address<\/a><\/li>\n<\/ul>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-10\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-10\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-9\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tRelated Projects\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-9\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-10\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\t\t\t\t<h2>Related Projects<\/h2>\n<ul>\n<li><b><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/the-yogi-project\/\">Yogi<\/a> <\/b>is a new abstraction-refinment engine based on test generation.<\/li>\n<li>UC Berkeley&#8217;s <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www-cad.eecs.berkeley.edu\/~rupak\/blast\/\"><b>BLAST 1.0<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Sagar Chaki&#8217;s <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www-2.cs.cmu.edu\/~chaki\/magic\/\"><b>MAGIC<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/wwwbrauer.informatik.tu-muenchen.de\/~schwoon\/\">Stefan Schwoon<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>&#8216;s <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/\" target=\"_blank\"><b>Moped<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>Georg Weissenbacher&#8217;s <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/boop.sourceforge.net\/\"><b>BOOP<\/b><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t<li class=\"m-0\" data-wp-context='{\"id\":\"accordion-content-12\"}' data-wp-init=\"callbacks.init\">\n\t\t<div class=\"accordion-header\">\n\t\t\t<button\n\t\t\t\taria-controls=\"accordion-content-12\"\n\t\t\t\tclass=\"btn btn-collapse\"\n\t\t\t\tdata-wp-bind--aria-expanded=\"state.isExpanded\"\n\t\t\t\tdata-wp-on--click=\"actions.onClick\"\n\t\t\t\tid=\"accordion-button-11\"\n\t\t\t\ttype=\"button\"\n\t\t\t>\n\t\t\t\tCollaborators\t\t\t<\/button>\n\t\t<\/div>\n\t\t<div\n\t\t\taria-labelledby=\"accordion-button-11\"\n\t\t\tclass=\"msr-accordion__content\"\n\t\t\tdata-wp-bind--inert=\"!state.isExpanded\"\n\t\t\tdata-wp-run=\"callbacks.run\"\n\t\t\tid=\"accordion-content-12\"\n\t\t>\n\t\t\t<div class=\"msr-accordion__body\">\n\t\t\t\t<h3>Co-founders<\/h3>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/tball\/\">Thomas Ball<\/a><\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/sriram\/\">Sriram K. Rajamani<\/a><\/li>\n<\/ul>\n<h3>MSR colleagues<\/h3>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/ellab\/\">Ella Bounimova<\/a><\/li>\n<li>Byron Cook<\/li>\n<\/ul>\n<h3>Windows colleagues<\/h3>\n<ul>\n<li>Nar Ganapathy<\/li>\n<li>Jakob Lichtenberg<\/li>\n<li>Rahul Kumar<\/li>\n<li>Vladimir Levin<\/li>\n<li>Con McGarvey<\/li>\n<li>Abdullah Ustuner<\/li>\n<li>Donn Terry<\/li>\n<\/ul>\n<h3>Alumni<\/h3>\n<ul>\n<li>Bohus Ondrusek<\/li>\n<\/ul>\n<h3>Visitors<\/h3>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.disi.unige.it\/person\/DelzannoG\/\">Giorgio Delzanno<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.mpi-sb.mpg.de\/~podelski\/podelski.html\">Andreas Podelski<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/wwwbrauer.informatik.tu-muenchen.de\/~schwoon\/\">Stefan Schwoon<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<h3>Interns<\/h3>\n<p>2008<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.inf.unisi.ch\/phd\/pek\/\">Edgar Pek<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>2007<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/zoo.cs.yale.edu\/~ams257\/\" target=\"_blank\">Antonios Stampoulis<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>2006<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/lal.cs.byu.edu\/source\/grad.html#rahul\">Rahul Kumar<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>2003<\/p>\n<ul>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/shuvendu\/\">Shuvendu Lahiri<\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.linkedin.com\/pub\/0\/351\/665\" target=\"_blank\">Jakob Lichtenberg<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.georg.weissenbacher.name\/\" target=\"_blank\">Georg Weissenbacher<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>2002<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.linkedin.com\/pub\/0\/351\/665\" target=\"_blank\">Jakob Lichtenberg<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/berkeley.intel-research.net\/mnaik\/\" target=\"_blank\">Mayur Naik<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>2001<b> <\/b><\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.sei.cmu.edu\/staff\/chaki\/\" target=\"_blank\">Sagar Chaki<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/verify.stanford.edu\/satyaki\/\" target=\"_blank\">Satyaki Das<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cis.ksu.edu\/~robby\/\">Robby<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.cs.virginia.edu\/~weimer\/\" target=\"_blank\">Westley Weimer<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n<p>2000<b> <\/b><\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www.cs.cmu.edu\/~chaki\/\">Sagar Chaki<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/www-cad.eecs.berkeley.edu\/~rupak\/\">Rupak Majumdar<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.cs.ucla.edu\/~todd\/\" target=\"_blank\">Todd Millstein<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n\t\t\t<\/div>\n\t\t<\/div>\n\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t<\/div>\n\t\n","protected":false},"excerpt":{"rendered":"<p>SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine. &#8220;Things like even software [&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-169817","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":"2001-11-05","related-publications":[152428,152498,152499,152713],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[302369,307343,307574,359282],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","value":"jhalleux","display_name":"Peli de Halleux","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/jhalleux\/\" aria-label=\"Visit the profile page for Peli de Halleux\">Peli de Halleux<\/a>","is_active":false,"user_id":32253,"last_first":"de Halleux, Peli","people_section":0,"alias":"jhalleux"},{"type":"user_nicename","value":"sriram","display_name":"Sriram Rajamani","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/sriram\/\" aria-label=\"Visit the profile page for Sriram Rajamani\">Sriram Rajamani<\/a>","is_active":false,"user_id":33711,"last_first":"Rajamani, Sriram","people_section":0,"alias":"sriram"},{"type":"user_nicename","value":"thoare","display_name":"Tony Hoare","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/thoare\/\" aria-label=\"Visit the profile page for Tony Hoare\">Tony Hoare<\/a>","is_active":false,"user_id":34029,"last_first":"Hoare, Tony","people_section":0,"alias":"thoare"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169817","targetHints":{"allow":["GET"]}}],"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\/169817\/revisions"}],"predecessor-version":[{"id":391145,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169817\/revisions\/391145"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=169817"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=169817"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=169817"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=169817"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=169817"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}