Abstract
Automatic verification by means of extended static checking (ESC) has seen some success in industry and academia due to its lightweight and easyto- use nature. Unfortunately, ESC comes at a cost: A host of logical and practical completeness and soundness issues. Interactive verification technology, on the other hand, is usually complete and sound, but requires a large amount of mathematical and practical expertise. Most programmers can be expected to use automatic, but not interactive, verification. The focus of this proposal is to integrate these two approaches into a single theoretical and practical framework, leveraging the benefits of each approach. © IFIP International Federation for Information Processing 2008.
Cite
CITATION STYLE
Kiniry, J. R., Chalin, P., Hurlin, C., Breunesse, C. B., Charles, J., Cok, D., … Tinelli, C. (2008). Integrating static checking and interactive verification: Supporting multiple theories and provers in verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4171 LNCS, pp. 153–160). https://doi.org/10.1007/978-3-540-69149-5_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
