NASA Logo, National Aeronautics and Space Administration

Jorge A. Navas

I am a Research Scientist at NASA Ames Research Center working in the Robust Software Engineering Group. My employer is Stinger Ghaffarian Technologies . I got a PhD in Computer Science from The University of New Mexico (USA) in 2008.

My research area is Programming Languages, and my topics of interest include the design and implementation of practical tools for software verification, testing, and debugging in order to help programmers to make reliable and safe code.

I am currently one of the developers of IKOS (Inference Kernel for Open Static analyzers), a high-performance static analysis platform based on Abstract Interpretation which is being developed at NASA.


HCVS'14 , NSAD'14, LOPSTR'14 , LOPSTR'15.

Publications ( DBLP )

  1. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Interval Analysis and Machine Arithmetic: Why Signedness Ignorance is Bliss. To appear in TOPLAS.
  2. G. Brat, J. A. Navas, N. Shi, A. Venet.
    IKOS: A Framework for Static Analysis based on Abstract Interpretation (PDF) . In SEFM'14 .
  3. E. De Angelis, F. Fioravanti, J. A. Navas, M. Proietti,
    Verification of Programs by Combining Iterated Specialization with Interpolation (PDF) . In HCVS'14
  4. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Abstract Interpretation over Non-Lattice Abstract Domains (PDF) . In SAS'13
  5. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Unbounded Model Checking with Interpolation for Regular Language Constraints (PDF) . In TACAS'13
  6. J. Jaffar, V. Murali, J. A. Navas.
    Boosting Concolic Testing with Interpolation (PDF) . In FSE'13
  7. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Failure Tabled Constraint Logic Programming by Interpolation (PDF) (PDF appendix) . In ICLP'13
  8. K.  Francis, J. A. Navas, P. J. Stuckey.
    Modelling Destructive Assignments (PDF) . In CP'13
  9. J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code (PDF) . In APLAS'12
  10. J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    TRACER: A Symbolic Execution Tool for Verification (PDF) . In CAV'12
  11. J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    Path-Sensitive Backward Slicing (PDF) . In SAS'12
  12. J. Jaffar, J. A. Navas, A. E. Santosa.
    Unbounded Symbolic Execution for Program Verification (PDF) . In RV'11
  13. E. Trias, J. A. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo.
    Negative Ternary Set-Sharing (PDF) . In ICLP'08
  14. J. A. Navas, E. Mera, P. López-García, M. Hermenegildo.
    User-Definable Resource Bounds Analysis for Logic Programs (PDF) . In ICLP'07
  15. M. Méndez-Lojo, J. A. Navas, M. Hermenegildo.
    A Flexible, (C)LP-based Approach to the Analysis of Object-Oriented Programs (PDF) . In LOPSTR'07
  16. M. Méndez-Lojo, J. A. Navas, M. Hermenegildo.
    Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode (PDF) . In BYTECODE'07
  17. J. A. Navas, F. Bueno, M. Hermenegildo .
    Efficient top-down set-sharing analysis using cliques (PDF) . In PADL'06


  • IKOS : scalable static analysis platform based on Abstract Interpretation.
  • TRACER : interpolation-based symbolic execution tool for verification of C programs.
  • Wrapped Interval Analysis : more precise signedess-agnostic interval analysis for LLVM IR.
  • FTCLP: Failure-based Tabling interpreter for Constraint-Logic Programming based on interpolation: a solver for recursive Constrained Horn Clauses.
  • Revenant : string solver for regular languages
  • Covenant : an algorithm for intersection of context-free languages.
  • The Ciao Preprocessor : a program analyzer for debugging, verification, and optimization for the Ciao programming language.


  • COMP90053 Program Analysis and Transformation, 1st Semester 2013. The University of Melbourne, Graduate level (with H. Sondergaard and G. Gange)

Doctoral Dissertation


Intelligent Systems Division
NASA Ames Research Center
Bldg. N269, room 294
Moffett Field, CA 94035-0001
Phone: +1 650-604-4279


First Gov logo
NASA Logo -