1 citations · 1 across the 3 of their papers we have counts for
3 papers
Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved. We study this proble…
CAPRI: Contract-Aware Proof Repair for Isabelle
Jim Woodcock, Gabriel Leite, Augusto Sampaio +1
We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM change…
Demystification and Near-perfect Estimation of Minimum Gas Limit and Gas Used for Ethereum Smart Contracts
Danilo Rafael de Lima Cabral, Pedro Antonino, Augusto Sampaio
The Ethereum blockchain has a \emph{gas system} that associates operations with a cost in gas units. Two central concepts of this system are the \emph{gas limit} assigned by the is…