Author:Laura KovácsPublications 

EasyChair Preprint no. 9606  EasyChair Preprint no. 9217  EasyChair Preprint no. 8182  EasyChair Preprint no. 6513  EasyChair Preprint no. 5531  EasyChair Preprint no. 5176  EasyChair Preprint no. 4946  EasyChair Preprint no. 2468       EasyChair Preprint no. 98           
KeyphrasesAlgebraic Recurrences, automated deduction, automated reasoning^{7}, automated theorem prover, automated theorem proving^{2}, Avatar, AVATAR architecture, clause normal form, consequence finding, firstorder logic^{2}, firstorder theorem prover, firstorder theorem proving^{5}, FOOL, fool formula, formal verification, induction^{4}, induction with generalization, inductive benchmarks, Inductive data types, integer induction, integers, interpolation, invariant generation^{3}, linear arithmetic, loop, loop invariants, loop synthesis, next state relation, Optimization, polymorphic arrays, program analysis^{2}, program synthesis, program verification^{3}, Quantified FirstOrder Logic, Resolution Calculus, SAT solving, saturation^{2}, saturation based proof search^{2}, saturationbased theorem proving, SMT, static analysis, structural induction^{2}, superposition^{2}, superposition reasoning^{3}, superposition theorem prover, symbol elimination, symbolic computation, term algebra^{2}, termination, theorem prover, theorem proving^{3}, translation, Vampire^{4}. 
