Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1394157, author = {Štill, Vladimír and Ročkai, Petr and Barnat, Jiří}, address = {Neuveden}, booktitle = {IEEE International Conference on Software Quality, Reliability and Security - QRS 2017}, doi = {http://dx.doi.org/10.1109/QRS.2017.15}, keywords = {C++; Exceptions; Verification; Testing; Model Checking; DIVINE}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Neuveden}, isbn = {978-1-5386-0592-9}, pages = {54-64}, publisher = {IEEE}, title = {Using Off-the-Shelf Exception Support Components in C++ Verification}, url = {http://ieeexplore.ieee.org/document/8009908/}, year = {2017} }
TY - JOUR ID - 1394157 AU - Štill, Vladimír - Ročkai, Petr - Barnat, Jiří PY - 2017 TI - Using Off-the-Shelf Exception Support Components in C++ Verification PB - IEEE CY - Neuveden SN - 9781538605929 KW - C++ KW - Exceptions KW - Verification KW - Testing KW - Model Checking KW - DIVINE UR - http://ieeexplore.ieee.org/document/8009908/ L2 - http://ieeexplore.ieee.org/document/8009908/ N2 - An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language. Our implementation consists of 2 parts: an implementation of the 'libunwind' platform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions. ER -
ŠTILL, Vladimír, Petr ROČKAI a Jiří BARNAT. Using Off-the-Shelf Exception Support Components in C++ Verification. Online. In \textit{IEEE International Conference on Software Quality, Reliability and Security - QRS 2017}. Neuveden: IEEE, 2017, s.~54-64. ISBN~978-1-5386-0592-9. Dostupné z: https://dx.doi.org/10.1109/QRS.2017.15.
|