Approximate computing is an emerging area for trading off the accuracy of an application for improved performance, lower energy costs, and tolerance to unreliable hardware. However, developers must ensure that the leveraged approximations do not introduce significant, intolerable divergence from the reference implementation, as specified by several established robustness criteria. In this work, we show the application of automated differential verification towards verifying relative safety, accuracy, and termination criteria for a class of program approximations. We use mutual summaries to express relative specifications for approximations, and SMT-based invariant inference to automate the verification of such specifications. We perform a detailed feasibility study showing promise of applying automated verification to the domain of approximate computing in a cost-effective manner.<\/p>\n","protected":false},"excerpt":{"rendered":"
Approximate computing is an emerging area for trading off the accuracy of an application for improved performance, lower energy costs, and tolerance to unreliable hardware. However, developers must ensure that the leveraged approximations do not introduce significant, intolerable divergence from the reference implementation, as specified by several established robustness criteria. In this work, we show […]<\/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":"","msr-author-ordering":[],"msr_publishername":"Springer","msr_publisher_other":"","msr_booktitle":"NASA Formal Methods Symposium (NFM '16)","msr_chapter":"","msr_edition":"","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"","msr_page_range_start":"","msr_page_range_end":"","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"NASA Formal Methods Symposium (NFM '16)","msr_doi":"","msr_arxiv_id":"","msr_mag_id":"","msr_other_authors":"","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_release_tracker_id":"","msr_highlight_type":"","msr_date_display_format":"","msr_main_download_label":"","msr_external_link_label":"","msr_doi_label":"","msr_published_date":"2016-06-24","msr_startdate":"","msr_presentation_date":"","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_year":2016,"msr_month":6,"msr_day":24,"msr_microsoftintellectualproperty":true,"msr_pub_id":"","msr_publication_uploader":[{"type":"file","title":"nfm2016-approximate","label_id":243132,"id":242543,"viewUrl":"https:\/\/find.codeghost.online\/en-us\/research\/wp-content\/uploads\/2016\/06\/nfm2016-approximate.pdf"}],"msr_related_uploader":[],"msr_original_fields_of_study":[],"msr_s2_paper_id":"","msr_s2_pdf_url":"","msr_citation_count_updated":"","msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13560],"msr-publication-type":[193716],"msr-publisher":[],"msr-publication-cta":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-242537","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"Springer","msr_edition":"","msr_affiliation":"","msr_published_date":"2016-06-24","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"NASA Formal Methods Symposium (NFM '16)","msr_pages_string":"","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":"","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"nfm2016-approximate","label_id":243132,"id":242543,"viewUrl":"https:\/\/find.codeghost.online\/en-us\/research\/wp-content\/uploads\/2016\/06\/nfm2016-approximate.pdf"}],"msr_related_uploader":[],"msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[],"msr-author-ordering":[],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[144812],"msr_project":[170570],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":170570,"post_title":"SymDiff: Differential Program Verifier","post_name":"symdiff-differential-program-verifier","post_type":"msr-project","post_date":"2010-10-14 00:25:14","post_modified":"2022-05-03 00:14:51","post_status":"publish","permalink":"https:\/\/find.codeghost.online\/en-us\/research\/project\/symdiff-differential-program-verifier\/","post_excerpt":"SymDiff is a tool for performing differential program verification. Differential program verification concerns with specifying and proving interesting properties over program differences, as opposed to the program itself. Such properties include program equivalence, but can also capture more general differential\/relational properties. SymDiff provides a specification language to state such differential (two-program) properties using the concept of mutual summaries that can relate procedures from two versions. It also provides proof system for checking such differential specifications…","_links":{"self":[{"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170570"}]}}]},"_links":{"self":[{"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/242537","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":2,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/242537\/revisions"}],"predecessor-version":[{"id":411776,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/242537\/revisions\/411776"}],"wp:attachment":[{"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/media?parent=242537"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=242537"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=242537"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=242537"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=242537"},{"taxonomy":"msr-publication-cta","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-cta?post=242537"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=242537"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=242537"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=242537"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=242537"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=242537"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=242537"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=242537"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/find.codeghost.online\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=242537"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}