Author:Laura KovácsPublications 

EasyChair Preprint no. 5176  EasyChair Preprint no. 4946  EasyChair Preprint no. 2468       EasyChair Preprint no. 98           
KeyphrasesAlgebraic Recurrences, automated reasoning^{4}, automated theorem prover, automated theorem proving^{2}, Avatar, AVATAR architecture, clause normal form, consequence finding, firstorder logic^{2}, firstorder theorem prover, firstorder theorem proving^{3}, FOOL, fool formula, formal verification, induction^{2}, induction with generalization, integer induction, 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, saturation based proof search, saturationbased theorem proving, static analysis, structural induction, superposition, superposition reasoning, superposition theorem prover, symbol elimination, symbolic computation, term algebra, termination, theorem prover, theorem proving^{2}, translation, Vampire^{3}. 
