Certification of Automated Termination Proofs
FroCos, pp. 148-162, 2007.
automated termination proofsdeep embeddingsformal methodformal guaranteedecision procedureMore(7+)
Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can checkthe soundness of a proof, they lack automation. Regarding automated tools, one sti...More
Full Text (Upload PDF)
PPT (Upload PPT)