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.

Publications [ DBLP | Google Scholar ]

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


  • SeaHorn : a verification framework for LLVM-based languages. News: SeaHorn won 3 medals in SV-COMP'15 !
  • Crab : a language-agnostic framework for abstract interpretation built on the top of IKOS .
  • Crab-LLVM : a static analyzer for LLVM-based languages. Crab-LLVM is currently integrated in SeaHorn .
  • TRACER : interpolation-based symbolic execution tool for verification of C programs.
  • FTCLP (Failure-based Tabling interpreter for Constraint-Logic Programming): an interpolation-based solver for recursive Constrained Horn Clauses.
  • Wrapped Interval Analysis : an interval abstract domain for fixed-width integers.
  • 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.


Doctoral Dissertation


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


First Gov logo
NASA Logo -