How to Get More Out of Your Oracles
| Autor: | Cruz-Filipe, Luís, Larsen, Kim Skak, Schneider-Kamp, Peter |
|---|---|
| Přispěvatelé: | Ayala-Rincón, Mauricio, Muñoz, César A. |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: | |
| Zdroj: | Cruz-Filipe, L, Larsen, K S & Schneider-Kamp, P 2017, How to Get More Out of Your Oracles . in M Ayala-Rincón & C A Muñoz (eds), Proceedings of the 8th International Conference on Interactive Theorem Proving . Springer, Lecture Notes in Computer Science, vol. 10499, pp. 164-170, 8th International Conference on Interactive Theorem Proving, Brasília, Brazil, 26/09/2017 . https://doi.org/10.1007/978-3-319-66107-0_11 |
| DOI: | 10.1007/978-3-319-66107-0_11 |
| Popis: | Formal verification of large computer-generated proofs often relies on certified checkers based on oracles. We propose a methodology for such proofs, advocating a separation of concerns between formalizing the underlying theory and optimizing the algorithm implemented in the checker, based on the observation that such optimizations can benefit significantly from adequately adapting the oracle. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|