Loading...
Please wait, while we are loading the content...
Similar Documents
Software model checking without source code
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Chaki, Sagar Ivers Sr., James |
| Copyright Year | 2009 |
| Description | We present a framework, called AIR, for verifying safety properties of assembly language programs via software model checking. AIR extends the applicability of predicate abstraction and counterexample guided abstraction refinement to the automated verification of low-level software. By working at the assembly level, AIR allows verification of programs for which source code is unavailable-such as legacy and COTS software-and programs that use features-such as pointers, structures, and object-orientation-that are problematic for source-level software verification tools. In addition, AIR makes no assumptions about the underlying compiler technology. We have implemented a prototype of AIR and present encouraging results on several non-trivial examples. |
| File Size | 176666 |
| Page Count | 10 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20100024473 |
| Archival Resource Key | ark:/13960/t82k1ds3k |
| Language | English |
| Publisher Date | 2009-04-01 |
| Access Restriction | Open |
| Subject Keyword | Mathematical And Computer Sciences (general) Aircraft Safety Flight Safety Assembly Language Prototypes Program Verification Computers Compilers Ntrs Nasa Technical Reports ServerĀ (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |