Publications (5)
Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
Thomas Ball, Nikolaj S. Bjørner, Ashley J. Chen +6
Security bugs and trapdoors in smart contracts have been impacting the Ethereum community since its inception. Conceptually, the 1.45-million Ethereum's contracts form a single "gi…
Can We Count on LLMs? The Fixed-Effect Fallacy and Claims of GPT-4 Capabilities
Thomas Ball, Shuo Chen, Cormac Herley
In this paper we explore evaluation of LLM capabilities. We present measurements of GPT-4 performance on several deterministic tasks; each task involves a basic calculation and tak…
Monotonically controlled integrals
Thomas Ball, David Preiss
The monotonically controlled integral defined by Bendová and Malý, which is equivalent to the Denjoy-Perron integral, admits a natural parameter thereby leading to the who…
Symbolic Automata: -Regularity Modulo Theories
Margus Veanes, Thomas Ball, Gabriel Ebner +1
Symbolic automata are finite state automata that support potentially infinite alphabets, such as the set of rational numbers, generally applied to regular expressions/languages ove…
Predicate Abstraction via Symbolic Decision Procedures
Shuvendu K. Lahiri, Thomas Ball, Byron Cook
We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predica…