Proof assistants, such as Isabelle HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr's interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring experienced users' expertise to new Isabelle users.
To determine induction variables automatically, Nagashima al developed a proof strategy language |PSL| and its default proof strategy, |try_hard| for Isabelle HOL @cite_9 . |PSL| tries to identify useful arguments for the |induct| method by conducting a depth-first search. Sometimes it is not enough to pass arguments to the |induct| method, but users have to specify necessary auxiliary lemmas before applying induction. To automate such labor-intensive work, @cite_10 , a new extension to , produces many lemmas by transforming the given proof goal while trying to identify a useful one in a goal-oriented manner.
@cite_9 @cite_10
2905394895 2951079127 2962820807 1889756448
Mathematical induction lies at the heart of mathematics and computer science. However, automated theorem proving of inductive problems is still limited in its power. In this abstract, we first summarize our progress in automating inductive theorem proving for Isabelle HOL. Then, we present MiLkMaId, our approach to suggesting promising applications of mathematical induction without completing a proof search. We present PGT, a Proof Goal Transformer for Isabelle HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle's strong automation to identify and prove such conjectures. We introduce a language, PSL, designed to capture high level proof strategies in Isabelle HOL. Given a strategy and a proof obligation, PSL’s runtime system generates and combines various tactics to explore a large search space with low memory usage. Upon success, PSL generates an efficient proof script, which bypasses a large part of the proof search. We also present PSL’s monadic interpreter to show that the underlying idea of PSL is transferable to other ITPs. We present combined-case k-induction, a novel technique for verifying software programs. This technique draws on the strengths of the classical inductive-invariant method and a recent application of k-induction to program verification. In previous work, correctness of programs was established by separately proving a base case and inductive step. We present a new k-induction rule that takes an unstructured, reducible control flow graph (CFG), a natural loop occurring in the CFG, and a positive integer k, and constructs a single CFG in which the given loop is eliminated via an unwinding proportional to k. Recursively applying the proof rule eventually yields a loop-free CFG, which can be checked using SAT- SMT-based techniques. We state soundness of the rule, and investigate its theoretical properties. We then present two implementations of our technique: K-INDUCTOR, a verifier for C programs built on top of the CBMC model checker, and K-BOOGIE, an extension of the Boogie tool. Our experiments, using a large set of benchmarks, demonstrate that our k-induction technique frequently allows program verification to succeed using significantly weaker loop invariants than are required with the standard inductive invariant approach.