DJ

Dejan Jovanović

0000-0001-8906-7874

cs.LOcs.PLcs.SEcs.AIcs.CLcs.DScs.LGcs.SC

On Valency

published · living versions

W_etmeccs6·v1 · currentpublished

Scaling Lean Theorem Proving for Real-World Code Verification

with Debargha Ganguly, Divya Raghunathan, Vikash Singh, Soonho Kong +4

1 version

Preprints & journals

7 papers in the corpus · 2019–2026

Nonlinear Arithmetic with SMTLIB Division is Undecidable2605.26181v3 · Dejan Jovanovic2026 · 0 citationsarXiv

A Neurosymbolic Approach to Natural Language Formalization and Verification2511.09008v2 · Chenyang An, Sam Bayless, Stefano Buliani et al.2025 · 1 citationarXiv

Interpolation and Model Checking for Nonlinear Arithmetic2106.04340v1 · Dejan Jovanovi'c, Bruno Dutertre2021 · 4 citationsarXiv

Formal Specification and Verification of Solidity Contracts with Events2005.10382v1 · 'Akos Hajdu, Dejan Jovanovi'c, Gabriela Ciocarlie2020 · 6 citationsarXiv

Solving bitvectors with MCSAT: explanations from bits and pieces (long version)2004.07940v1 · St'ephane Graham-Lengrand, Dejan Jovanovi'c, Bruno Dutertre2020 · 1 citationarXiv

SMT-Friendly Formalization of the Solidity Memory Model2001.03256v2 · 'Akos Hajdu, Dejan Jovanovi'c2020 · 30 citationsarXiv

Verifying Visibility-Based Weak Consistency1911.01508v1 · Siddharth Krishna, Michael Emmi, Constantin Enea et al.2019 · 9 citationsarXiv

Career total: 47 works. 7 are in this corpus.

Profile built from the corpus for this byline.

Author records are still filling in while the Hub is in alpha. If this is your page, you'll be able to claim it soon. Spot a mistake? Tell us.