Joint forces for memory safety checking revisited

We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2020-04, Vol.22 (2), p.115-133
Main Authors: Chalupa, Marek, Strejček, Jan, Vitovská, Martina
Format: Article
Language:English
Subjects:
Computer Science
Instruments
Program verification (computers)
Safety
Slicing
Software Engineering
Software Engineering/Programming and Operating Systems
Spin 2018
Theory of Computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43
cites cdi_FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43
container_end_page 133
container_issue 2
container_start_page 115
container_title International journal on software tools for technology transfer
container_volume 22
creator Chalupa, Marek
Strejček, Jan
Vitovská, Martina
description We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic , which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact of particular components.
doi_str_mv 10.1007/s10009-019-00526-2
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_journals_2268840564</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>2268840564</sourcerecordid><originalsourceid>FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43</originalsourceid><addsrcrecordid>eNp9kLtOxDAQRS0EEsvCD1BFojb4EXviEq14aiUaqK1kYi9ZSLLYWaT8PQ5B0FHMo7j3zugQcs7ZJWcMrmLqzFDGUzElNBUHZMFzKamAAg5_dzDH5CTGLWMcNJgF4Y990w2Z7wO6OI2sdW0fxiyW3g1jhq8O35pukwX32cRmcPUpOfLle3RnP3NJXm5vnlf3dP1097C6XlOU3AxUqhpKD4gCjAftqjK9oHQhFRNYGeMU5LWvJFcCVY5Cg_eVLgXwCrHCXC7JxZy7C_3H3sXBbvt96NJJK4QuipwpPanErMLQxxict7vQtGUYLWd2QmNnNDahsd9orEgmOZtiEncbF_6i_3F9AdPJZeo</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>2268840564</pqid></control><display><type>article</type><title>Joint forces for memory safety checking revisited</title><source>Springer Link</source><creator>Chalupa, Marek ; Strejček, Jan ; Vitovská, Martina</creator><creatorcontrib>Chalupa, Marek ; Strejček, Jan ; Vitovská, Martina</creatorcontrib><description>We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic , which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact of particular components.</description><identifier>ISSN: 1433-2779</identifier><identifier>EISSN: 1433-2787</identifier><identifier>DOI: 10.1007/s10009-019-00526-2</identifier><language>eng</language><publisher>Berlin/Heidelberg: Springer Berlin Heidelberg</publisher><subject>Computer Science ; Instruments ; Program verification (computers) ; Safety ; Slicing ; Software Engineering ; Software Engineering/Programming and Operating Systems ; Spin 2018 ; Theory of Computation</subject><ispartof>International journal on software tools for technology transfer, 2020-04, Vol.22 (2), p.115-133</ispartof><rights>Springer-Verlag GmbH Germany, part of Springer Nature 2019</rights><rights>International Journal on Software Tools for Technology Transfer is a copyright of Springer, (2019). All Rights Reserved.</rights><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43</citedby><cites>FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43</cites><orcidid>0000-0001-5873-403X</orcidid></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27923,27924</link.rule.ids></links><search><creatorcontrib>Chalupa, Marek</creatorcontrib><creatorcontrib>Strejček, Jan</creatorcontrib><creatorcontrib>Vitovská, Martina</creatorcontrib><title>Joint forces for memory safety checking revisited</title><title>International journal on software tools for technology transfer</title><addtitle>Int J Softw Tools Technol Transfer</addtitle><description>We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic , which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact of particular components.</description><subject>Computer Science</subject><subject>Instruments</subject><subject>Program verification (computers)</subject><subject>Safety</subject><subject>Slicing</subject><subject>Software Engineering</subject><subject>Software Engineering/Programming and Operating Systems</subject><subject>Spin 2018</subject><subject>Theory of Computation</subject><issn>1433-2779</issn><issn>1433-2787</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2020</creationdate><recordtype>article</recordtype><recordid>eNp9kLtOxDAQRS0EEsvCD1BFojb4EXviEq14aiUaqK1kYi9ZSLLYWaT8PQ5B0FHMo7j3zugQcs7ZJWcMrmLqzFDGUzElNBUHZMFzKamAAg5_dzDH5CTGLWMcNJgF4Y990w2Z7wO6OI2sdW0fxiyW3g1jhq8O35pukwX32cRmcPUpOfLle3RnP3NJXm5vnlf3dP1097C6XlOU3AxUqhpKD4gCjAftqjK9oHQhFRNYGeMU5LWvJFcCVY5Cg_eVLgXwCrHCXC7JxZy7C_3H3sXBbvt96NJJK4QuipwpPanErMLQxxict7vQtGUYLWd2QmNnNDahsd9orEgmOZtiEncbF_6i_3F9AdPJZeo</recordid><startdate>20200401</startdate><enddate>20200401</enddate><creator>Chalupa, Marek</creator><creator>Strejček, Jan</creator><creator>Vitovská, Martina</creator><general>Springer Berlin Heidelberg</general><general>Springer Nature B.V</general><scope>AAYXX</scope><scope>CITATION</scope><scope>3V.</scope><scope>7SC</scope><scope>7XB</scope><scope>8AL</scope><scope>8AO</scope><scope>8FD</scope><scope>8FE</scope><scope>8FG</scope><scope>8FK</scope><scope>8G5</scope><scope>ABJCF</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>ARAPS</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>GNUQQ</scope><scope>GUQSH</scope><scope>HCIFZ</scope><scope>JQ2</scope><scope>K7-</scope><scope>L6V</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope><scope>M0N</scope><scope>M2O</scope><scope>M7S</scope><scope>MBDVC</scope><scope>P5Z</scope><scope>P62</scope><scope>PADUT</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>PTHSS</scope><scope>Q9U</scope><orcidid>https://orcid.org/0000-0001-5873-403X</orcidid></search><sort><creationdate>20200401</creationdate><title>Joint forces for memory safety checking revisited</title><author>Chalupa, Marek ; Strejček, Jan ; Vitovská, Martina</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2020</creationdate><topic>Computer Science</topic><topic>Instruments</topic><topic>Program verification (computers)</topic><topic>Safety</topic><topic>Slicing</topic><topic>Software Engineering</topic><topic>Software Engineering/Programming and Operating Systems</topic><topic>Spin 2018</topic><topic>Theory of Computation</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Chalupa, Marek</creatorcontrib><creatorcontrib>Strejček, Jan</creatorcontrib><creatorcontrib>Vitovská, Martina</creatorcontrib><collection>CrossRef</collection><collection>ProQuest Central (Corporate)</collection><collection>Computer and Information Systems Abstracts</collection><collection>ProQuest Central (purchase pre-March 2016)</collection><collection>Computing Database (Alumni Edition)</collection><collection>ProQuest Pharma Collection</collection><collection>Technology Research Database</collection><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>ProQuest Central (Alumni) (purchase pre-March 2016)</collection><collection>Research Library (Alumni Edition)</collection><collection>Materials Science &amp; Engineering Collection</collection><collection>ProQuest Central (Alumni Edition)</collection><collection>ProQuest Central</collection><collection>Advanced Technologies &amp; Aerospace Collection</collection><collection>ProQuest Central Essentials</collection><collection>AUTh Library subscriptions: ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>ProQuest Central Student</collection><collection>Research Library Prep</collection><collection>SciTech Premium Collection (Proquest) (PQ_SDU_P3)</collection><collection>ProQuest Computer Science Collection</collection><collection>Computer Science Database</collection><collection>ProQuest Engineering Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><collection>Computing Database</collection><collection>Research Library</collection><collection>Engineering Database</collection><collection>Research Library (Corporate)</collection><collection>Advanced Technologies &amp; Aerospace Database</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Collection</collection><collection>Research Library China</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>Engineering Collection</collection><collection>ProQuest Central Basic</collection><jtitle>International journal on software tools for technology transfer</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Chalupa, Marek</au><au>Strejček, Jan</au><au>Vitovská, Martina</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Joint forces for memory safety checking revisited</atitle><jtitle>International journal on software tools for technology transfer</jtitle><stitle>Int J Softw Tools Technol Transfer</stitle><date>2020-04-01</date><risdate>2020</risdate><volume>22</volume><issue>2</issue><spage>115</spage><epage>133</epage><pages>115-133</pages><issn>1433-2779</issn><eissn>1433-2787</eissn><abstract>We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic , which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact of particular components.</abstract><cop>Berlin/Heidelberg</cop><pub>Springer Berlin Heidelberg</pub><doi>10.1007/s10009-019-00526-2</doi><tpages>19</tpages><orcidid>https://orcid.org/0000-0001-5873-403X</orcidid></addata></record>
fulltext fulltext
identifier ISSN: 1433-2779
ispartof International journal on software tools for technology transfer, 2020-04, Vol.22 (2), p.115-133
issn 1433-2779
1433-2787
language eng
recordid cdi_proquest_journals_2268840564
source Springer Link
subjects Computer Science
Instruments
Program verification (computers)
Safety
Slicing
Software Engineering
Software Engineering/Programming and Operating Systems
Spin 2018
Theory of Computation
title Joint forces for memory safety checking revisited
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-08T12%3A38%3A57IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Joint%20forces%20for%20memory%20safety%20checking%20revisited&rft.jtitle=International%20journal%20on%20software%20tools%20for%20technology%20transfer&rft.au=Chalupa,%20Marek&rft.date=2020-04-01&rft.volume=22&rft.issue=2&rft.spage=115&rft.epage=133&rft.pages=115-133&rft.issn=1433-2779&rft.eissn=1433-2787&rft_id=info:doi/10.1007/s10009-019-00526-2&rft_dat=%3Cproquest_cross%3E2268840564%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c319t-35d7af7cc279f76eba1435683502cb99e574dfb3152c54c267ffb6a271bccbc43%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=2268840564&rft_id=info:pmid/&rfr_iscdi=true