Author:Laura Kovács

Keyphrases

Algebraic Recurrences, automated deduction, automated reasoning⁷, automated theorem prover, automated theorem proving², Avatar, AVATAR architecture, clause normal form, consequence finding, first-order logic², first-order theorem prover, first-order theorem proving⁵, FOOL, fool formula, formal verification, induction⁴, induction with generalization, inductive benchmarks, Inductive data types, integer induction, integers, interpolation, invariant generation³, linear arithmetic, loop, loop invariants, loop synthesis, next state relation, Optimization, polymorphic arrays, program analysis², program synthesis, program verification³, Quantified First-Order Logic, Resolution Calculus, SAT solving, saturation², saturation based proof search², saturation-based theorem proving, SMT, static analysis, structural induction², superposition², superposition reasoning³, superposition theorem prover, symbol elimination, symbolic computation, term algebra², termination, theorem prover, theorem proving³, translation, Vampire⁴.