3 citations · 6 across the 7 of their papers we have counts for
7 papers
Finding Connections via Satisfiability Solving
Clemens Eisenhofer, Michael Rawson, Laura Kovács
Commonly used proof strategies by automated reasoners organise proof search either by ordering-based saturation or by reducing goals to subgoals. In this paper, we combine these tw…
On Solving String Equations via Powers and Parikh Images
Clemens Eisenhofer, Theodor Seiser, Nikolaj S. Bjørner +1
We present a new approach for solving string equations as extensions of Nielsen transformations. Key to our work are the combination of three techniques: a power operator for strin…
Constraint Learning for Non-confluent Proof Search
Michael Rawson, Clemens Eisenhofer, Laura Kovács
Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We…
Lazy Reimplication in Chronological Backtracking
Robin Coutelier, Mathias Fleury, Laura Kovács
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is…
SAT Solving for Variants of First-Order Subsumption
Robin Coutelier, Jakob Rath, Michael Rawson +2
Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system v…
Scaling CheckMate for Game-Theoretic Security
Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel +2
We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning tech…
SAT-Based Subsumption Resolution
Robin Coutelier, Laura Kovács, Michael Rawson +1
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 sub…