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 (slides).
• Co-chair of the 2015 edition of the SMT Workshop
• Talk on MCSAT at the 2015 edition of the SAT/SMT summer school (slides).
• 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.

1. Interpolation and Model Checking for Nonlinear Arithmetic
   Dejan Jovanović, Bruno Dutertre. In Proceedings of the 33rd Conference on Computer Aided Verification, 2021.
2. 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.
3. Formal Specification and Verification of Solidity Contracts with Events
   Ákos Hajdu, Dejan Jovanović, Gabriela Ciocarlie. In 2nd Workshop on Formal Methods for Blockchains, 2020.
4. SMT-Friendly Formalization of the Solidity Memory Model
   Ákos Hajdu, Dejan Jovanović. In Proceedings of the 29th European Symposium on Programming, 2020.
5. 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.
6. 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.
7. Verification of Fault-Tolerant Protocols with Sally
   Bruno Dutertre, Dejan Jovanović, and Jorge Navas. In Proceedings of the Tenth NASA Formal Methods Symposium, 2018.
8. 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.
9. Designing Theory Solvers with Extensions
   Andrew ReynoldsCesare Tinelli, Dejan Jovanović, Clark Barrett. In 11th International Symposium on Frontiers of Combining Systems, 2017.
10. 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.
11. Solving Nonlinear Integer Arithmetic with MCSAT
    Dejan Jovanović. In Proceedings of the 18th Conference on Verification, Model Checking, and Abstract Interpretation, 2017.
12. Property-Directed k-Induction
    Dejan Jovanović, Bruno Dutertre. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, 2016.
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. Being careful about theory combination
    Dejan Jovanović and Clark Barrett. In Formal Methods in System Design, volume 42, pages 67-90. Springer-Verlag, 2013.
22. 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.
23. 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.
24. 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.
25. 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.
26. 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.
27. Polite Theories Revisited
    Dejan Jovanović and Clark Barrett. Technical Report TR2010-922, Department of Computer Science, New York University, January 2010.
28. 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.
29. Variable Neighborhood Search for the Probabilistic Satisfiability Problem
    Dejan Jovanović, Nenad Mladenović, and Zoran Ognjanović. In Proceedings of the 6th Metaheuristics International Conference, 2005.