## About me

BSc in Computer Science from the Faculty of Mathematics, University of Belgrade in 2003. PhD at NYU in 2012 (thesis) under the supervision of Clark Barrett. I was a computer scientist at the SRI computer science laboratory from 2013 to 2021. I am currently an applied scientist at Amazon Web Services. My research interests lie in the areas of formal methods, verification, logic, decision procedures, SAT and SMT solvers.

## Contact

Email: dejan.jovanovic@gmail.com

## News

- Yices2 wins 3 medals at the 2018 FLoC Olympic Games (slides)
- Best paper honorable mention for “Property-Directed k-Induction” at FMCAD 2016.
- Yices2 wins non-linear divisions of SMT-COMP 2016 (QF_{NIA,NRA,UFNIA, UFNRA}).
- Talk on SMT at the 2016 edition of the SAT/SMT/AR summer school.
- Co-chair of the 2015 edition of the SMT Workshop
- Talk on MCSAT at the 2015 edition of the SAT/SMT summer school.
- Co-organizer of the 2014 edition of the SAT/SMT summer school

## Projects

- solc-verify: A Modular Verifier for Solidity Smart Contracts.
- Sally: A model-checker for infinite-state systems.
- LibPoly: A library for advanced polynomial operations.
- Yices: SMT solver from SRI.
- CVC4: SMT solver from NYU.
- cutsat: A linear integer arithmetic solver.

## Papers

Also available at Google scholar.

**Interpolation and Model Checking for Nonlinear Arithmetic**

Dejan Jovanović, Bruno Dutertre. In*Proceedings of the 33rd Conference on Computer Aided Verification*, 2021.**Solving bitvectors with MCSAT: explanations from bits and pieces**

Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre. In*Proceedings of the 10th International Joint Conference on Automated Reasoning*, 2020.**Formal Specification and Verification of Solidity Contracts with Events**

Ákos Hajdu, Dejan Jovanović, Gabriela Ciocarlie. In*2nd Workshop on Formal Methods for Blockchains*, 2020.**SMT-Friendly Formalization of the Solidity Memory Model**

Ákos Hajdu, Dejan Jovanović. In*Proceedings of the 29th European Symposium on Programming*, 2020.**solc-verify: A Modular Verifier for Solidity Smart Contracts**

Ákos Hajdu, Dejan Jovanović. In*Proceedings of the 11th Working Conference on Verified Software: Theories, Tools, and Experiments*, 2019.**A Separation Logic with Data: Small Models and Automation**

Jens Katelaan, Dejan Jovanović, and Georg Weissenbacher. In*Proceedings of the 9th International Joint Conference on Automated Reasoning*, 2018.**Verification of Fault-Tolerant Protocols with Sally**

Bruno Dutertre, Dejan Jovanović, and Jorge Navas. In*Proceedings of the Tenth NASA Formal Methods Symposium*, 2018.**Selfless Interpolation for Infinite-State Model Checking**

Tanja Schindler, Dejan Jovanović. In*Proceedings of the 19th Conference on Verification, Model Checking, and Abstract Interpretation*, 2018.**Designing Theory Solvers with Extensions**

Andrew ReynoldsCesare Tinelli, Dejan Jovanović, Clark Barrett. In*11th International Symposium on Frontiers of Combining Systems*, 2017.**Abduction by Non-Experts**

Nikolaj Bjørner, Dejan Jovanović, Tancrède Lepoint, Philipp Rümmer, Martin Schäf. In*21st International Conference on Logic for Programming, Artificial Inelligence and Reasoning*, 2017.**Solving Nonlinear Integer Arithmetic with MCSAT**

Dejan Jovanović. In*Proceedings of the 18th Conference on Verification, Model Checking, and Abstract Interpretation*, 2017.**Property-Directed k-Induction**

Dejan Jovanović, Bruno Dutertre. In*Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design*, 2016.**Finding Inconsistencies in Programs with Loops**

Temesghen Kahsai, Jorge A. Navas, Dejan Jovanović, Martin Schäf. In*Proceedings of the 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning*, 2015.**Conflict-Directed Graph Coverage**

Daniel Schwartz-Narbonne, Martin Schäf, Dejan Jovanović, Philipp Rümmer, Thomas Wies. In*Proceedings of the NASA Formal Methods Symposium*, 2015.**Template-based circuit understanding**

Adrià Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanović, Sharad Malik. In*Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design*, 2014.**A tale of two solvers: eager and lazy approaches to bit-vectors**

Liana Hadarean, Kshitij Bansal, Dejan Jovanović, Clark Barrett, Cesare Tinelli. In*Proceedings of the 26th International Conference on Computer Aided Verification*, 2014.**Safety envelope for security**

Ashish Tiwari, Bruno Dutertre, Dejan Jovanović, Thomas de Candia, Patrick D Lincoln, John Rushby, Dorsa Sadigh, Sanjit Seshia. In*Proceedings of the 3rd international conference on High confidence networked systems*, 2014.**The Design and Implementation of the Model Constructing Satisfiability Calculus**

Dejan Jovanović and Clark Barrett and Leonardo de Moura. In*Proceedings of the 13th Conference on Formal Methods in Computer-Aided Design*, 2013.**Cutting to the Chase: Solving Linear Integer Arithmetic**

Dejan Jovanović and Leonardo de Moura. In*Journal of Automated Reasoning*, volume 51, issue 1, pages 79-108. Springer-Verlag, 2013.**A Model-Constructing Satisfiability Calculus**

Leonardo de Moura and Dejan Jovanović. In*Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation*, volume 7737 of*Lecture Notes in Computer Science*, pages 1-12, 2013.**Being careful about theory combination**

Dejan Jovanović and Clark Barrett. In*Formal Methods in System Design*, volume 42, pages 67-90. Springer-Verlag, 2013.**Solving Non-Linear Arithmetic**

Dejan Jovanović and Leonardo de Moura. In*Proceedings of the 6th International Joint Conference on Automated Deduction*, volume 7364 of*Lecture Notes in Computer Science*, pages 339-354. Springer-Verlag, 2012.**Sharing is Caring: Combination of Theories**

Dejan Jovanović and Clark Barrett. In*Proceedings of the 8th International Symposium Frontiers of Combining Systems*, volume 6989 of*Lecture Notes in Computer Science*, pages 195-210. Springer-Verlag, 2011.**Cutting to the Chase: Solving Linear Integer Arithmetic**

Dejan Jovanović and Leonardo de Moura. In*Proceedings of the 23rd International Conference on Automated Deduction*, volume 6803 of*Lecture Notes in Computer Science*, pages 338-353. Springer-Verlag, 2011.**CVC4**

Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. In*Proceedings of the 23rd International Conference on Computer Aided Verification*, volume 6806 of*Lecture Notes in Computer Science*, pages 171-177. Springer-Verlag, 2011.**Polite Theories Revisited**

Dejan Jovanović and Clark Barrett. In*Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning*, volume 6397 of*Lecture Notes in Computer Science*, pages 402-416. Springer-Verlag, 2010.**Polite Theories Revisited**

Dejan Jovanović and Clark Barrett. Technical Report TR2010-922, Department of Computer Science, New York University, January 2010.**Logical Analysis of Hash Functions**

Dejan Jovanović and Predrag Janičić. In Proceedings of the 5th International Workshop*Frontiers of Combining Systems*, volume 3717 of*Lecture Notes in Computer Science*, pages 200-215. Springer-Verlag, 2005.**Variable Neighborhood Search for the Probabilistic Satisfiability Problem**

Dejan Jovanović, Nenad Mladenović, and Zoran Ognjanović. In*Proceedings of the 6th Metaheuristics International Conference*, 2005.