Problem identification using program checking Original Research Article

We describe AλgoVista, a web-based search engine that assists computer scientists find algorithms and implementations that solve specific problems. AλgoVista also allows algorithm designers to advertise their results in a forum accessible to programmers and theoreticians alike. AλgoVista is not keyword based. Rather, users provide input⇒output samples that describe the behavior of their needed algorithm. This query-by-example requires no knowledge of specialized terminology—the user only needs an ability to formalize her problem. AλgoVistaʹs search mechanism is based on a novel application of program checking, a technique developed as an alternative to program verification and testing. AλgoVista operates at .