Directed Proof Generation for Machine Code
| العنوان: | Directed Proof Generation for Machine Code |
|---|---|
| المؤلفون: | Matt Elder, Akash Lal, Evan Driscoll, Thomas Reps, Tycho Andersen, Aditya V. Thakur, Junghee Lim, Amanda Burton |
| المصدر: | Computer Aided Verification ISBN: 9783642142949 CAV |
| بيانات النشر: | Springer Berlin Heidelberg, 2010. |
| سنة النشر: | 2010 |
| مصطلحات موضوعية: | High-level verification, Theoretical computer science, Functional verification, Software model checking, Programming language, Computer science, Local variable, Aliasing (computing), Symbolic execution, computer.software_genre, Machine code, computer, Software verification |
| الوصف: | We present the algorithms used in McVeto (Machine-Code VErification TOol), a tool to check whether a stripped machine-code program satisfies a safety property The verification problem that McVeto addresses is challenging because it cannot assume that it has access to (i) certain structures commonly relied on by source-code verification tools, such as control-flow graphs and call-graphs, and (ii) meta-data, such as information about variables, types, and aliasing It cannot even rely on out-of-scope local variables and return addresses being protected from the program's actions What distinguishes McVeto from other work on software model checking is that it shows how verification of machine-code can be performed, while avoiding conventional techniques that would be unsound if applied at the machine-code level. |
| ردمك: | 978-3-642-14294-9 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_________::813043dac87d89b1312679126e6ec509 https://doi.org/10.1007/978-3-642-14295-6_27 |
| حقوق: | OPEN |
| رقم الأكسشن: | edsair.doi...........813043dac87d89b1312679126e6ec509 |
| قاعدة البيانات: | OpenAIRE |
| ردمك: | 9783642142949 |
|---|