@inproceedings{minisy2017sgy,
    author     = {Sallai, Gyula and T{\'o}th, Tam{\'a}s},
    title      = {Boosting Software Verification with Compiler Optimizations},
    year       = {2017},
    booktitle  = {Proceedings of the 24th PhD Mini-Symposium},
    location   = {Budapest, Hungary},
    publisher  = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},
    editor     = {Pataki, B\'{e}la},
    pages      = {66--69},
    doi        = {10.5281/zenodo.291903},
    isbn       = {978-963-313-243-2},

    type       = {Local event},
    url_pdf    = {minisy2017sgy.pdf},
    url_link   = {https://doi.org/10.5281/zenodo.291903},
    abstract   = {Unlike testing, formal verification can not only prove the presence of errors, but their absence as well, thus making it suitable for verifying safety-critical systems. Formal verification may be performed by transforming the already implemented source code to a formal model and querying the resulting model on reachability of an erroneous state. Sadly, transformations from source code to a formal model often yield large and complex models, which may result in extremely high computational effort for a verifier algorithm. This paper describes a workflow that provides formal verification for C programs, aided by optimization techniques usually used in compiler design in order to reduce the size and complexity of a program and thus improve the performance of the verifier.},
}

{"_id":"hg8uoTwSorLuxo9Y6","bibbaseid":"sallai-tth-boostingsoftwareverificationwithcompileroptimizations-2017","downloads":3,"creationDate":"2017-03-26T11:15:01.978Z","title":"Boosting Software Verification with Compiler Optimizations","author_short":["Sallai, G.","Tóth, T."],"year":2017,"bibtype":"inproceedings","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","bibdata":{"bibtype":"inproceedings","type":"Local event","author":[{"propositions":[],"lastnames":["Sallai"],"firstnames":["Gyula"],"suffixes":[]},{"propositions":[],"lastnames":["Tóth"],"firstnames":["Tamás"],"suffixes":[]}],"title":"Boosting Software Verification with Compiler Optimizations","year":"2017","booktitle":"Proceedings of the 24th PhD Mini-Symposium","location":"Budapest, Hungary","publisher":"Budapest University of Technology and Economics, Department of Measurement and Information Systems","editor":[{"propositions":[],"lastnames":["Pataki"],"firstnames":["Béla"],"suffixes":[]}],"pages":"66–69","doi":"10.5281/zenodo.291903","isbn":"978-963-313-243-2","url_pdf":"minisy2017sgy.pdf","url_link":"https://doi.org/10.5281/zenodo.291903","abstract":"Unlike testing, formal verification can not only prove the presence of errors, but their absence as well, thus making it suitable for verifying safety-critical systems. Formal verification may be performed by transforming the already implemented source code to a formal model and querying the resulting model on reachability of an erroneous state. Sadly, transformations from source code to a formal model often yield large and complex models, which may result in extremely high computational effort for a verifier algorithm. This paper describes a workflow that provides formal verification for C programs, aided by optimization techniques usually used in compiler design in order to reduce the size and complexity of a program and thus improve the performance of the verifier.","bibtex":"@inproceedings{minisy2017sgy,\n author = {Sallai, Gyula and T{\\'o}th, Tam{\\'a}s},\n title = {Boosting Software Verification with Compiler Optimizations},\n year = {2017},\n booktitle = {Proceedings of the 24th PhD Mini-Symposium},\n location = {Budapest, Hungary},\n publisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},\n editor = {Pataki, B\\'{e}la},\n pages = {66--69},\n doi = {10.5281/zenodo.291903},\n isbn = {978-963-313-243-2},\n\n type = {Local event},\n url_pdf = {minisy2017sgy.pdf},\n url_link = {https://doi.org/10.5281/zenodo.291903},\n abstract = {Unlike testing, formal verification can not only prove the presence of errors, but their absence as well, thus making it suitable for verifying safety-critical systems. Formal verification may be performed by transforming the already implemented source code to a formal model and querying the resulting model on reachability of an erroneous state. Sadly, transformations from source code to a formal model often yield large and complex models, which may result in extremely high computational effort for a verifier algorithm. This paper describes a workflow that provides formal verification for C programs, aided by optimization techniques usually used in compiler design in order to reduce the size and complexity of a program and thus improve the performance of the verifier.},\n}\n\n","author_short":["Sallai, G.","Tóth, T."],"editor_short":["Pataki, B."],"key":"minisy2017sgy","id":"minisy2017sgy","bibbaseid":"sallai-tth-boostingsoftwareverificationwithcompileroptimizations-2017","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/minisy2017sgy.pdf"," link":"https://doi.org/10.5281/zenodo.291903"},"metadata":{"authorlinks":{}},"downloads":3},"search_terms":["boosting","software","verification","compiler","optimizations","sallai","tóth"],"keywords":[],"authorIDs":[],"dataSources":["7MDizr2BZojXoNdPN"]}