Zobrazeno 1 - 10
of 233
pro vyhledávání: '"Kovacs, Laura"'
PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a b
Externí odkaz:
http://arxiv.org/abs/2406.04696
We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning techniques to determine whether a game-theoretic protocol model is game-th
Externí odkaz:
http://arxiv.org/abs/2403.10310
We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted first-order log
Externí odkaz:
http://arxiv.org/abs/2403.03712
Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show
Externí odkaz:
http://arxiv.org/abs/2402.19199
Publikováno v:
Automated Deduction - CADE 29. CADE 2023. Lecture Notes in Computer Science, vol 14132. Springer, Cham
We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establ
Externí odkaz:
http://arxiv.org/abs/2402.18962
Publikováno v:
Principles of Systems Design 2022, Lecture Notes in Computer Science, vol 13660. Springer, Cham
Induction in saturation-based first-order theorem proving is a new exciting direction in the automation of inductive reasoning. In this paper we survey our work on integrating induction directly into the saturation-based proof search framework of fir
Externí odkaz:
http://arxiv.org/abs/2402.18954
This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is b
Externí odkaz:
http://arxiv.org/abs/2402.17927
We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour of matrices, as we show that tree-like calculi have a number of drawba
Externí odkaz:
http://arxiv.org/abs/2402.10610
Publikováno v:
Automated Deduction -- CADE 29 (2023). Lecture Notes in Computer Science vol 14132. Springer
Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlyi
Externí odkaz:
http://arxiv.org/abs/2401.17832
Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than gene
Externí odkaz:
http://arxiv.org/abs/2310.05120