| タイトル | Deductive Evaluation: Implicit Code Verification With Low User Burden |
| 本文（外部サイト） | http://hdl.handle.net/2060/20160007713 |
| 著者（英） | Di Vito, Ben L. |
| 発行日 | 2016-01-17 |
| 言語 | eng |
| 内容記述 | We describe a framework for symbolically evaluating C code using a deductive approach that discovers and proves program properties. The framework applies Floyd-Hoare verification principles in its treatment of loops, with a library of iteration schemes serving to derive loop invariants. During evaluation, theorem proving is performed on-the-fly, obviating the generation of verification conditions normally needed to establish loop properties. A PVS-based prototype is presented along with results for sample C functions. |
| NASA分類 | Computer Programming and Software |
| レポートNO | NF1676L-22305 |
| 権利 | No Copyright |
|
