1 citations · 1 across the 2 of their papers we have counts for
5 papers
Formal Specification and Verification of Solidity Contracts with Events
Ákos Hajdu, Dejan Jovanović, Gabriela Ciocarlie
Events in the Solidity language provide a means of communication between the on-chain services of decentralized applications and the users of those services. Events are commonly us…
Solving bitvectors with MCSAT: explanations from bits and pieces (long version)
Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre
We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension…
SMT-Friendly Formalization of the Solidity Memory Model
Ákos Hajdu, Dejan Jovanović
Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model…
Verifying Visibility-Based Weak Consistency
Siddharth Krishna, Michael Emmi, Constantin Enea +1
Multithreaded programs generally leverage efficient and thread-safe concurrent objects like sets, key-value maps, and queues. While some concurrent-object operations are designed t…
solc-verify: A Modular Verifier for Solidity Smart Contracts
Ákos Hajdu, Dejan Jovanović
We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions…