How to Get More Out of Your Oracles.

Luís Cruz-Filipe, Kim S. Larsen, and Peter Schneider-Kamp.
In 8th International Conference on Interactive Theorem Proving (ITP), volume 10499 of Lecture Notes in Computer Science. Springer. Accepted for Publication.

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.

---

open access (157 KB)

The same as the publisher's version, when the publisher permits. Otherwise, the author's last version before the publisher's copyright; this is often exactly the same, but sometimes fonts, page numbers, figure numbers, etc. are different. It may also be a full version. However, it is safe to read this version, and at the same time cite the official version, as long as references to concrete locations, numbered theorems, etc. inside the article are avoided.

other publications

Other publications by the author.