We present VS3, a tool that automatically verifies complex properties of programs and infers maximally weak preconditions and maximally strong postconditions by leveraging the power of SMT solvers. VS3 discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user supplies VS3 with a set of predicates and invariant templates. VS3 automatically finds instantiations of the unknowns in the templates as subsets of the predicate set. We have used VS3 to automatically verify $\\forall\\exists$ properties of programs and to infer worst case upper bounds and preconditions for functional correctness.<\/p>\n","protected":false},"excerpt":{"rendered":"
We present VS3, a tool that automatically verifies complex properties of programs and infers maximally weak preconditions and maximally strong postconditions by leveraging the power of SMT solvers. VS3 discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user supplies VS3 with a set of predicates and invariant templates. VS3 automatically finds […]<\/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":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13561],"msr-publication-type":[193716],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-336467","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-algorithms","msr-locale-en_us"],"msr_publishername":"Springer-Verlag Berlin, Heidelberg","msr_edition":"CAV '09 Proceedings of the 21st International Conference on Computer Aided Verification","msr_affiliation":"","msr_published_date":"2009-06-26","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"702 - 708","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"336470","msr_publicationurl":"","msr_doi":"10.1007\/978-3-642-02658-4_58","msr_publication_uploader":[{"type":"file","title":"VS3: SMT Solvers for Program Verification","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/cav09_vs3.pdf","id":336470,"label_id":0},{"type":"file","title":"VS3: SMT Solvers for Program Verification (Slides)","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/cav09_vs3.pptx","id":336473,"label_id":0},{"type":"doi","title":"10.1007\/978-3-642-02658-4_58","viewUrl":false,"id":false,"label_id":0}],"msr_related_uploader":"","msr_attachments":[{"id":336473,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/cav09_vs3.pptx"},{"id":336470,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/cav09_vs3.pdf"}],"msr-author-ordering":[{"type":"text","value":"Saurabh Srivastava","user_id":0,"rest_url":false},{"type":"user_nicename","value":"sumitg","user_id":33755,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=sumitg"},{"type":"text","value":"Jeffrey S. Foster","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[170033],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":170033,"post_title":"VS3 (Verification and Specification using SMT Solvers)","post_name":"vs3-verification-and-specification-using-smt-solvers","post_type":"msr-project","post_date":"2008-12-01 20:42:05","post_modified":"2019-08-19 15:39:48","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/vs3-verification-and-specification-using-smt-solvers\/","post_excerpt":"SMT Solvers have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for using SMT solvers to automatically discover inductive invariants for proving given safety properties of systems. Additionally, this project also explores techniques for using SMT solvers to synthesize systems in the first place given enough specifications. Saurabh Srivastava, who is leading…","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170033"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/336467","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/336467\/revisions"}],"predecessor-version":[{"id":524453,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/336467\/revisions\/524453"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=336467"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=336467"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=336467"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=336467"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=336467"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=336467"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=336467"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=336467"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=336467"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=336467"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=336467"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=336467"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=336467"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=336467"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=336467"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=336467"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}