Dejan Jovanović

Hi, I’m
Dejan.

I work on logic, software, and AI—and how they fit together. This is where I share what I’m working on.

Have a look around

About

My research focuses on automated reasoning, formal verification, logic, decision procedures, SAT and SMT solvers, and their interaction with AI.

Previously, I was an Applied Scientist at AWS (2021–2026) and a computer scientist at SRI International’s Computer Science Laboratory (2013–2021). I received my PhD in Computer Science from NYU in 2012 (thesis), advised by Clark Barrett, and my BSc in Computer Science from the Faculty of Mathematics, University of Belgrade, in 2003.

Lately

Earlier news & highlights

Projects

  • Automated Reasoning checks Formalization of natural-language policies and verification of answers in Amazon Bedrock Guardrails.
  • Zelkova Automated reasoning about AWS access-control policies.
  • 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 An SMT solver, succeeded by cvc5.
  • cutsat A linear integer arithmetic solver.

Publications

Also available on Google Scholar.

  1. Scaling Lean Theorem Proving for Real-World Code Verification
    Debargha Ganguly, Divya Raghunathan, Dejan Jovanović, Vikash Singh, Soonho Kong, Aaron Tomb, Aman Goel, Ferhat Erata, Sam Bayless. Preprint, arXiv:2610.38174, 2026.
  2. A Neurosymbolic Approach to Natural Language Formalization and Verification
    Chenyang An, Sam Bayless, Stefano Buliani, Darion Cassel, Byron Cook, Duncan Clough, Rémi Delmas, Nafi Diallo, Ferhat Erata, Nick Feng, Dimitra Giannakopoulou, Aman Goel, Aditya Gokhale, Joe Hendrix, Victor Heorhiadi, Marc Hudak, Dejan Jovanović, Andrew M. Kent, Benjamin Kiesl-Reiter, Jeffrey J. Kuna, Nadia Labai, Joseph Lilien, Divya Raghunathan, Zvonimir Rakamarić, Niloofar Razavi, Michael Tautschnig, Ali Torkamani, Nathaniel Weir, Michael W. Whalen, Jianan Yao. In Proceedings of the 38th Conference on Computer Aided Verification (CAV), 2026. Publication.
  3. Nonlinear Arithmetic with SMTLIB Division is Undecidable
    Dejan Jovanović. Preprint, arXiv:2605.26181, 2026.
  4. Projective Model Counting for IP Addresses in Access Control Policies
    Loris D’Antoni, Andrew Gacek, Amit Goel, Dejan Jovanović, Rami Gökhan Kıcı, Dan Peebles, Neha Rungta, Yasmine Sharoda, Chungha Sung. In Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 208–216, 2024. Publication.
  5. Interpolation and Model Checking for Nonlinear Arithmetic
    Dejan Jovanović, Bruno Dutertre. In Proceedings of the 33rd Conference on Computer Aided Verification, 2021.
  6. 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.
  7. Formal Specification and Verification of Solidity Contracts with Events
    Ákos Hajdu, Dejan Jovanović, Gabriela Ciocarlie. In 2nd Workshop on Formal Methods for Blockchains, 2020.
  8. SMT-Friendly Formalization of the Solidity Memory Model
    Ákos Hajdu, Dejan Jovanović. In Proceedings of the 29th European Symposium on Programming, 2020.
  9. Verifying Visibility-Based Weak Consistency
    Siddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanović. In Proceedings of the 29th European Symposium on Programming (ESOP), pages 280–307, 2020. Preprint.
  10. 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.
  11. A Separation Logic with Data: Small Models and Automation
    Jens Pagel, Dejan Jovanović, and Georg Weissenbacher. In Proceedings of the 9th International Joint Conference on Automated Reasoning, 2018.
  12. Verification of Fault-Tolerant Protocols with Sally
    Bruno Dutertre, Dejan Jovanović, and Jorge Navas. In Proceedings of the Tenth NASA Formal Methods Symposium, 2018.
  13. 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.
  14. Designing Theory Solvers with Extensions
    Andrew Reynolds, Cesare Tinelli, Dejan Jovanović, Clark Barrett. In 11th International Symposium on Frontiers of Combining Systems, 2017.
  15. 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 Intelligence and Reasoning, 2017.
  16. Solving Nonlinear Integer Arithmetic with MCSAT
    Dejan Jovanović. In Proceedings of the 18th Conference on Verification, Model Checking, and Abstract Interpretation, 2017.
  17. LibPoly: A Library for Reasoning about Polynomials
    Dejan Jovanović, Bruno Dutertre. In Proceedings of the 15th International Workshop on Satisfiability Modulo Theories (SMT), pages 28–39, 2017.
  18. An MCSAT Treatment of Bit-Vectors
    Stéphane Graham-Lengrand, Dejan Jovanović. In Proceedings of the 15th International Workshop on Satisfiability Modulo Theories (SMT), pages 89–100, 2017.
  19. Property-Directed k-Induction
    Dejan Jovanović, Bruno Dutertre. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, 2016.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. Being careful about theory combination
    Dejan Jovanović and Clark Barrett. In Formal Methods in System Design, volume 42, pages 67-90. Springer-Verlag, 2013.
  29. 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.
  30. 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.
  31. 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.
  32. 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.
  33. 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.
  34. Polite Theories Revisited
    Dejan Jovanović and Clark Barrett. Technical Report TR2010-922, Department of Computer Science, New York University, January 2010.
  35. 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.
  36. Variable Neighborhood Search for the Probabilistic Satisfiability Problem
    Dejan Jovanović, Nenad Mladenović, and Zoran Ognjanović. In Proceedings of the 6th Metaheuristics International Conference, 2005.

Get in touch