Author:Laura Kovács

Keyphrases

Algebraic Recurrences, arithmetic, automated deduction, automated reasoning⁸, automated software verification, automated theorem prover, automated theorem proving⁴, automating induction, Avatar, AVATAR architecture, clause normal form, consequence finding, Decentralized Protocols, finite fields, first-order logic², first-order theorem prover, first-order theorem proving⁶, FOOL, fool formula, formal verification, function calls, game theory, induction⁴, induction in first-order logic, 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, polynomial arithmetic, program analysis², program synthesis², program verification³, Quantified First-Order Logic, Resolution Calculus, SAT solving, saturation³, saturation based proof search², saturation-based theorem proving, Secure Protocols, security analysis, SMT, SMT solving, software correctness, sorting algorithms, static analysis, structural induction², superposition³, superposition reasoning³, superposition theorem prover, superposition-based theorem proving, symbol elimination, symbolic computation, term algebra², termination, theorem prover, theorem proving⁴, translation, Triangular Sets, unification, Unification with Abstraction, Vampire⁴.