1 citations · 1 across the 7 of their papers we have counts for
7 papers
Tensor Seeks Layout: Formalizing Layout Selection for ML Compilers
Clemens Eisenhofer, Yuwen Jia, Daniel Kroening +1
Modern machine learning compilers select tensor memory layouts to minimize execution cost under hardware constraints. Layout selection is global: an operator may be fastest under o…
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…
PolySAT: Word-level Bit-vector Reasoning in Z3
Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann +2
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-d…
Spanning Matrices via Satisfiability Solving
Clemens Eisenhofer, Michael Rawson, Laura Kovács
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…
Automated Instantiation of Control Flow Tracing Exercises
Clemens Eisenhofer, Martin Riener
One of the first steps in learning how to program is reading and tracing existing code. In order to avoid the error-prone task of generating variations of a tracing exercise, our t…