Author:Laura Kovács

Keyphrases

Algebraic Recurrences, arithmetic², automated deduction, automated inductive reasoning, automated reasoning¹⁵, automated software verification², automated theorem prover, automated theorem provers, automated theorem proving⁶, automating induction, Avatar, AVATAR architecture, Benchmarks², blockchain protocols, clause normal form, consequence finding, Decentralized Protocols, decision procedure, Descision Procedure, finite fields, first-order logic², first-order theorem prover, first-order theorem proving⁹, FOOL, fool formula, formal methods, formal models, formal verification, function calls, Game-theoretic security, game theory³, Higher order moments, Hyperproperties², incentive compatibility, induction⁶, induction in first-order logic, induction with generalization, inductive benchmarks, Inductive data types, integer induction, integers, interactive theorem proving, interpolation, invariant generation³, invariant synthesis, Lean 4, LIA, linear arithmetic⁴, LIRA², literal selection², logic, logic and types, loop, loop invariants, loop synthesis, LRA, martingale, model checking², Modeling Template, next state relation, Optimization, optional stopping, polymorphic arrays, polynomial arithmetic, Presburger arithmetic, probabilistic programs, program analysis², program synthesis³, program verification⁴, Protocol Modeling, protocol verification, Quantified First-Order Logic, quantifier elimination², real arithmetic², recursion, recursive programs, Reducibility constraints, redundancy³, Resolution Calculus, rewriting, SAT solving, saturation⁶, saturation based proof search², saturation-based theorem proving, Secure Protocols, Security, security analysis, simplification, SMT⁷, SMT solving², software correctness, software verification², sorting algorithms², static analysis, structural induction², superposition⁸, superposition-based theorem proving, superposition calculus, superposition reasoning³, superposition theorem prover, symbol elimination, symbolic computation, term algebra², termination, theorem prover, theorem proving⁵, translation, Triangular Sets, unification, Unification with Abstraction, Vampire⁴, virtual substitution.