Author:Laura KovácsPublications 

EasyChair Preprint no. 12145  EasyChair Preprint no. 12142  EasyChair Preprint no. 10632  EasyChair Preprint no. 10853    EasyChair Preprint no. 10223  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, arithmetic, automated deduction, automated reasoning^{8}, automated software verification, automated theorem prover, automated theorem proving^{4}, automating induction, Avatar, AVATAR architecture, clause normal form, consequence finding, Decentralized Protocols, finite fields, firstorder logic^{2}, firstorder theorem prover, firstorder theorem proving^{6}, FOOL, fool formula, formal verification, function calls, game theory, induction^{5}, induction in firstorder logic, 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, polynomial arithmetic, program analysis^{2}, program synthesis^{3}, program verification^{3}, Quantified FirstOrder Logic, recursion, Reducibility constraints, redundancy, Resolution Calculus, SAT solving, saturation^{5}, saturation based proof search^{2}, saturationbased theorem proving, Secure Protocols, security analysis, SMT, SMT solving, software correctness, sorting algorithms, static analysis, structural induction^{2}, superposition^{5}, superposition reasoning^{3}, superposition theorem prover, superpositionbased theorem proving, symbol elimination, symbolic computation, term algebra^{2}, termination, theorem prover, theorem proving^{5}, translation, Triangular Sets, unification, Unification with Abstraction, Vampire^{4}. 
