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.


Publications ( DBLP )

  1. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    A Tool for Intersecting Context-Free Grammars and Its Applications. To appear in NFM'15.
  2. A. Gurfinkel , T. Kahsai, J. A. Navas,
    SeaHorn: A Framework for Verifying C Programs (Competition Contribution). To appear in TACAS'15.
  3. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Interval Analysis and Machine Arithmetic: Why Signedness Ignorance is Bliss. (PDF) TOPLAS 2014.
  4. J. R. Cornish, G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Analyzing array manipulating programs by program transformation (PDF) LOPSTR'14
  5. G. Brat, J. A. Navas, N. Shi, A. Venet.
    IKOS: A Framework for Static Analysis based on Abstract Interpretation (PDF) . In SEFM'14 .
  6. E. De Angelis, F. Fioravanti, J. A. Navas, M. Proietti,
    Verification of Programs by Combining Iterated Specialization with Interpolation (PDF) . In HCVS'14
  7. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Abstract Interpretation over Non-Lattice Abstract Domains (PDF) . In SAS'13
  8. 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
  9. J. Jaffar, V. Murali, J. A. Navas.
    Boosting Concolic Testing with Interpolation (PDF) . In FSE'13
  10. 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
  11. K.  Francis, J. A. Navas, P. J. Stuckey.
    Modelling Destructive Assignments (PDF) . In CP'13
  12. 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
  13. J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    TRACER: A Symbolic Execution Tool for Verification (PDF) . In CAV'12
  14. J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    Path-Sensitive Backward Slicing (PDF) . In SAS'12
  15. J. Jaffar, J. A. Navas, A. E. Santosa.
    Unbounded Symbolic Execution for Program Verification (PDF) . In RV'11
  16. E. Trias, J. A. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo.
    Negative Ternary Set-Sharing (PDF) . In ICLP'08
  17. J. A. Navas, E. Mera, P. López-García, M. Hermenegildo.
    User-Definable Resource Bounds Analysis for Logic Programs (PDF) . In ICLP'07
  18. 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
  19. M. Méndez-Lojo, J. A. Navas, M. Hermenegildo.
    Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode (PDF) . In BYTECODE'07
  20. J. A. Navas, F. Bueno, M. Hermenegildo .
    Efficient top-down set-sharing analysis using cliques (PDF) . In PADL'06


  • SeaHorn : a verification framework for proving safety properties in C programs. News: SeaHorn has achieved 3 medals in SV-COMP'15 !
  • TRACER : interpolation-based symbolic execution tool for verification of C programs.
  • IKOS : a static analysis framework based on Abstract Interpretation for safety-critical systems.
  • Wrapped Interval Analysis : more precise signedess-agnostic interval abstract domain.
  • FTCLP: Failure-based Tabling interpreter for Constraint-Logic Programming based on interpolation: a solver for recursive Constrained Horn Clauses.
  • Revenant : a string solver.
  • Covenant : a semi-decider 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.

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 -