Jorge A. Navas

About me

I work for Certora, where I am developing a new verification tool for Solana smart contracts. These contracts, together with their specs, are written in Rust and compiled to Solana Binary Format (sBPF), which is a Solana's custom version of eBPF. This tool uses Abstract Interpretation to translate sBPF to efficient and sound verification conditions, which in turn, are solved by SMT solvers.

Before Certora, I worked for SRI (2016-2021) and NASA (2013-2016).
Before that, I enjoyed my post-doc life at University of Melbourne (2011-2013) and National University of Singapore (2008-2011).
I got a PhD in Computer Science from the University of New Mexico in 2008, and a B.Sc in Computer Science from Technical University of Madrid in 2003.

Outside of work, I enjoy spending time with my family and running. I am from Ceuta, a beautiful Spanish city on the North African coast.

Software

• The Certora Prover : automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar.
• SeaHorn: analysis/verification framework for LLVM bitcode.
• Crab: C++ library for static analysis based on abstract interpretation.
  • Tutorial about Crab in Dagsthul (07/10/2023). The slides can be found here and the code here.
• Sea-DSA: a pointer analysis for LLVM bitcode.
• Clam: a static analyzer based on Crab and Sea-DSA for LLVM bitcode.
• PREVAIL: eBPF verifier based on Crab.
  • PREVAIL is currently used to verify eBPF programs that run on the top of Windows (see ebpf-for-windows project for more details).
  • **PREVAIL in the news**: [1],[2].
• SmartACE: A verifier of Solidity smart contracts based on SeaHorn.
  • Check out several blog posts here.
• OCCAMv2: A whole-program debloater for LLVM bitcode.
• IKOS: Inference Kernel for Open Static Analyzers. **NASA Group Achievement Award** in 2014.
• TRACER: interpolation-based symbolic execution tool for verification of C programs.
• FTCLP: interpolation-based solver for recursive Constrained Horn Clauses.
• Wrapped Interval Analysis: static analyzer of LLVM bitcode specialized for fixed-width integers.
• Revenant: string solver.
• Covenant: semi-decider for intersection of context-free languages.
• The Ciao Preprocessor : a program analyzer for debugging, verification, and optimization for the Ciao programming language.

Recent Service Activitives

• 2025: TACAS, SAS, NFM.
• 2024: PLDI, CAV, SAS.
• 2023: VMCAI, SAS, FMICS, LPAR.
• 2022: VMCAI, SAS, PLDI.

Peer-Reviewed Publications [ DBLP | Google Scholar]

1. Automatic Inference of Relational Object Invariants (PDF).
   Yusen Su, J. A. Navas, A. Gurfinkel, I. Garcia-Contreras.
   VMCAI'25.
2. Inductive Predicate Synthesis Modulo Programs (PDF).
   Scott Wesley, M. Christakis, J. A. Navas, R. Trefler, V. Wustholz, A. Gurfinkel
   ECOOP'24.
3. Efficient Modular SMT-Based Model Checking of Pointer Programs (PDF).
   I. Garcia-Contreras, A. Gurfinkel, J. A. Navas
   SAS'22.
4. Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE (PDF).
   Scott Wesley, M. Christakis, A. Gurfinkel, J. A. Navas, R. Trefler, V. Wustholz.
   VMCAI'22.
5. Compositional Verification of Smart Contracts Through Communication Abstraction (PDF).
   Scott Wesley, M. Christakis, A. Gurfinkel, J. A. Navas, R. Trefler, V. Wustholz.
   SAS'21.
6. Disjunctive Interval Analysis (PDF).
   G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
   SAS'21.
7. Abstract Interpretation of LLVM with a Region-Based Memory Model (PDF).
   A. Gurfinkel, J. A. Navas
   VSTTE'21. These are the scripts to reproduce the experimental evaluation.
8. Automated Safety Verification of Programs Invoking Neural Networks (PDF).
   M. Christakis, H. Ferit Eniser, H. Hermanns, J. Hoffmann, Y. Kothari, Jianlin Li, J. A. Navas, V. Wustholz.
   CAV'21. The code is available here, and the benchmarks here.
9. Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios (PDF).
   M. N. Mansur, B.  Mariano, M. Christakis, J. A. Navas, V. Wustholz.
   CAV'21. The code is available here.
10. A Fresh Look at Zones and Octagons (PDF).
    G. Gange, Zequn Ma, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    ACM TOPLAS Volume 43, Issue 3 September 2021.
11. Verification of an Optimized NTT Algorithm (PDF).
    J. A. Navas, B. Dutertre, I. Mason,
    VSTTE'20. The code of the verifier is available here.
12. Dissecting Widening: Separating Termination from Information (PDF).
    **Distinguished Paper Award**
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    APLAS'19.
13. Unification-based Pointer Analysis without Oversharing (PDF).
    J. Kuderski, J. A. Navas, A. Gurfinkel.
    FMCAD'19.
14. Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions (PDF).
    E. Gershuni, N. Amit, A. Gurfinkel, N. Narodytska, J. A. Navas, N. Rinetzky, L. Ryzhyk and M. Sagiv.
    PLDI'19.
15. Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime Monitoring (PDF).
    Falk Howard, Dimitra Giannakopoulou, Malte Maus, J. A. Navas.
    ISoLA'18.
16. Executable Counterexamples in Software Model Checking (PDF).
    J. Gennari, A. Gurfinkel, T. Kahsai, J. A. Navas, E. J. Schwartz.
    VSTTE'18. Video 1(3m51s)   Video 2(4m37s).
17. Verification of Fault-Tolerant Protocols with Sally (PDF).
    B. Dutertre, D. Jovanovic, J. A. Navas.
    NFM'18.
18. A Context-Sensitive Memory Model for Verification of C/C++ Programs (PDF).
    A. Gurfinkel, J. A. Navas.
    SAS'17.
19. Exploiting Sparsity in Difference-Bound Matrices (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    SAS'16.
20. An Abstract Domain of Uninterpreted Functions (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    VMCAI'16.
21. A Complete Refinement Procedure for Regular Separability of Context-Free Languages (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    TCS 2016.
22. Finding Inconsistencies in Programs with Loops (PDF).
    T. Kahsai, J. A. Navas, D. Jovanovic, M. Schäf.
    LPAR'15.
23. The SeaHorn Verification Framework (PDF).
    A. Gurfinkel, T. Kahsai, A.   Komuravelli, J. A. Navas.
    CAV'15.
24. Horn-Clauses as an Intermediate Representation for Program Analysis and Transformation (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    ICLP'15.
25. A Tool for Intersecting Context-Free Grammars and Its Applications (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    NFM'15.
26. SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (PDF).
    A. Gurfinkel, T. Kahsai, J. A. Navas.
    TACAS'15.
27. Interval Analysis and Machine Arithmetic: Why Signedness Ignorance is Bliss (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    ACM TOPLAS Volume 37, Issue 1 January 2015.
28. Analyzing array manipulating programs by program transformation (PDF).
    J. R. Cornish, G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    LOPSTR'14.
29. IKOS: A Framework for Static Analysis based on Abstract Interpretation (PDF).
    G. Brat, J. A. Navas, N. Shi, A. Venet.
    SEFM'14.
30. Verification of Programs by Combining Iterated Specialization with Interpolation (PDF).
    E. De Angelis, F. Fioravanti, J. A. Navas, M. Proietti.
    HCVS'14.
31. Abstract Interpretation over Non-Lattice Abstract Domains (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    SAS'13.
32. Unbounded Model Checking with Interpolation for Regular Language Constraints (PDF).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    TACAS'13.
33. Boosting Concolic Testing with Interpolation (PDF).
    J. Jaffar, V. Murali, J. A. Navas.
    FSE'13.
34. Failure Tabled Constraint Logic Programming by Interpolation (PDF) (PDF appendix).
    G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    ICLP'13.
35. Modelling Destructive Assignments (PDF).
    K.  Francis, J. A. Navas, P. J. Stuckey.
    CP'13.
36. Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code (PDF).
    J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    APLAS'12.
37. TRACER: A Symbolic Execution Tool for Verification (PDF).
    J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    CAV'12.
38. Path-Sensitive Backward Slicing (PDF).
    J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    SAS'12.
39. Unbounded Symbolic Execution for Program Verification (PDF).
    RV'11.
    J. Jaffar, J. A. Navas, A. E. Santosa.
40. Negative Ternary Set-Sharing (PDF).
    E. Trias, J. A. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo.
    ICLP'08.
41. User-Definable Resource Bounds Analysis for Logic Programs (PDF).
    **Test of Time Award (10 years)**
    J. A. Navas, E. Mera, P. Lopez-Garcia, M. Hermenegildo.
    ICLP'07.
42. A Flexible, (C)LP-based Approach to the Analysis of Object-Oriented Programs (PDF).
    M. Mendez-Lojo, J. A. Navas, M. Hermenegildo.
    LOPSTR'07.
43. Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode (PDF).
    M. Mendez-Lojo, J. A. Navas, M. Hermenegildo.
    BYTECODE'07.
44. Efficient top-down set-sharing analysis using cliques (PDF).
    J. A. Navas, F. Bueno, M. Hermenegildo .
    PADL'06.

Non-Peer-Reviewed Publications

• OCCAM-v2: Combining Static and Dynamic Analysis for Effective and Efficient Whole-Program Specialization (PDF).
  J. A. Navas, A. Gehani.
  Communications of the ACM Volume 66, Issue 4, pp 40–47, April 2023.
• Algorithmic Logic-Based Verification (PDF).
  A. Gurfinkel, T. Kahsai, J. A. Navas.
  ACM Special Interest Group on Logic and Computation (SIGLOG) April, 2015.

Unpublished Technical Reports

• A Partial-Order Approach to Array Content Analysis (PDF).
  G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.

Doctoral Dissertation

• J. A. Navas. Analysis and Inference of Resource Usage Information. Ph.D. Thesis,
  University of New Mexico (UNM), Department of Computer Science, August 2008.