Author:Laura KovácsPublications 

EasyChair Preprint no. 4946  EasyChair Preprint no. 2468       EasyChair Preprint no. 98           
KeyphrasesAlgebraic Recurrences, automated reasoning^{3}, automated theorem prover, automated theorem proving^{2}, Avatar, AVATAR architecture, clause normal form, consequence finding, firstorder logic^{2}, firstorder theorem prover, firstorder theorem proving^{2}, FOOL, fool formula, formal verification, induction, induction with generalization, interpolation, invariant generation^{3}, loop, loop invariants, loop synthesis, next state relation, Optimization, polymorphic arrays, program analysis^{2}, program verification^{3}, Resolution Calculus, SAT solving, saturation based proof search, static analysis, structural induction, superposition, superposition reasoning, symbol elimination, symbolic computation, term algebra, termination, theorem prover, theorem proving, translation, Vampire^{3}. 
