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.
Integrating static checking and interactive verification: Supporting multiple theories and provers in verification / Kiniry, J. R.; Chalin, P.; Hurlin, C.; Breunesse, C. -B.; Charles, J.; Cok, D.; Jacobs, B.; Poll, E.; Ranise, S.; Schubert, A.; Tinelli, C.. - 4171:(2008), pp. 153-160. (Intervento presentato al convegno 1st IFIP TC 2/WG 2.3 Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2005 tenutosi a Zurich, che nel 2005) [10.1007/978-3-540-69149-5_17].
Integrating static checking and interactive verification: Supporting multiple theories and provers in verification
Ranise S.;
2008-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
