Showing 1–7 of 7 results for author: Jovanović, D

Interpolation and Model Checking for Nonlinear Arithmetic

Authors: Dejan Jovanović, Bruno Dutertre

Abstract: We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the mo… ▽ More We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic. △ Less

Submitted 8 June, 2021; originally announced June 2021.

Comments: To be published in CAV 2021

Formal Specification and Verification of Solidity Contracts with Events

Authors: Ákos Hajdu, Dejan Jovanović, Gabriela Ciocarlie

Abstract: 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 used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source… ▽ More 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 used as an abstraction of contract execution that is relevant from the users' perspective. Users must, therefore, be able to understand the meaning and trust the validity of the emitted events. This paper presents a source-level approach for the formal specification and verification of Solidity contracts with the primary focus on events. Our approach allows specification of events in terms of the on-chain data that they track, and predicates that define the correspondence between the blockchain state and the abstract view provided by the events. The approach is implemented in solc-verify, a modular verifier for Solidity, and we demonstrate its applicability with various examples. △ Less

Submitted 20 May, 2020; originally announced May 2020.

Solving bitvectors with MCSAT: explanations from bits and pieces (long version)

Authors: Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre

Abstract: 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 of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level in… ▽ More 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 of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level interpolation for two common fragments of the theory. For full generality, explaining conflicts outside of the covered fragments resorts to local bitblasting. The approach is implemented in the Yices 2 SMT solver and we present experimental results. △ Less

Submitted 16 April, 2020; originally announced April 2020.

Comments: 24 pages, long version of IJCAR'2020 conference paper

SMT-Friendly Formalization of the Solidity Memory Model

Authors: Ákos Hajdu, Dejan Jovanović

Abstract: 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. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free f… ▽ More 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. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools. △ Less

Submitted 17 April, 2020; v1 submitted 9 January, 2020; originally announced January 2020.

Comments: Authors' manuscript. Published in P. Müller (Ed.): ESOP 2020, LNCS 12075, 2020. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-44914-8_9

Verifying Visibility-Based Weak Consistency

Authors: Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic

Abstract: Multithreaded programs generally leverage efficient and thread-safe concurrent objects like sets, key-value maps, and queues. While some concurrent-object operations are designed to behave atomically, each witnessing the atomic effects of predecessors in a linearization order, others forego such strong consistency to avoid complex control and synchronization bottlenecks. For example, contains (val… ▽ More Multithreaded programs generally leverage efficient and thread-safe concurrent objects like sets, key-value maps, and queues. While some concurrent-object operations are designed to behave atomically, each witnessing the atomic effects of predecessors in a linearization order, others forego such strong consistency to avoid complex control and synchronization bottlenecks. For example, contains (value) methods of key-value maps may iterate through key-value entries without blocking concurrent updates, to avoid unwanted performance bottlenecks, and consequently overlook the effects of some linearization-order predecessors. While such weakly-consistent operations may not be atomic, they still offer guarantees, e.g., only observing values that have been present. In this work we develop a methodology for proving that concurrent object implementations adhere to weak-consistency specifications. In particular, we consider (forward) simulation-based proofs of implementations against relaxed-visibility specifications, which allow designated operations to overlook some of their linearization-order predecessors, i.e., behaving as if they never occurred. Besides annotating implementation code to identify linearization points, i.e., points at which operations' logical effects occur, we also annotate code to identify visible operations, i.e., operations whose effects are observed; in practice this annotation can be done automatically by tracking the writers to each accessed memory location. We formalize our methodology over a general notion of transition systems, agnostic to any particular programming language or memory model, and demonstrate its application, using automated theorem provers, by verifying models of Java concurrent object implementations. △ Less

Submitted 4 November, 2019; originally announced November 2019.

solc-verify: A Modular Verifier for Solidity Smart Contracts

Authors: Ákos Hajdu, Dejan Jovanović

Abstract: 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 using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of E… ▽ More 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 using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort. △ Less

Submitted 16 March, 2020; v1 submitted 9 July, 2019; originally announced July 2019.

Comments: Authors' manuscript. Published in S. Chakraborty and J. A. Navas (Eds.): VSTTE 2019, LNCS 12031, 2020. The final publication is available at Springer via https://doi.org/10.1007/978-3-030-41600-3_11

Teaching Network Storage Technology Assessment Outcomes and Directions

Authors: Dr. V. Jovanovic, Dr. Timur Mirzoev

Abstract: The paper presents academic content, delivery and assessment mechanisms used, available resources including initial lessons from teaching Networked Storage Technology as a special topics course to students enrolled in two specific programs - IT and CS. The course is based on the EMC s vendor-neutral Storage Technology Fundamentals course. Furthermore, this manuscript provides a detailed review of… ▽ More The paper presents academic content, delivery and assessment mechanisms used, available resources including initial lessons from teaching Networked Storage Technology as a special topics course to students enrolled in two specific programs - IT and CS. The course is based on the EMC s vendor-neutral Storage Technology Fundamentals course. Furthermore, this manuscript provides a detailed review of how the course fits into our curriculum, particularly, how it helps achieving the 2008 ABET assessment requirements. △ Less

Submitted 8 April, 2014; originally announced April 2014.

Journal ref: ACM 2008, New York, NY, USA ISBN: 978-1-60558-329-7