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.

Publications [ DBLP | Google Scholar ]

  1. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    An Abstract Domain of Uninterpreted Functions. In VMCAI'16 .
  2. T. Kahsai, J. A. Navas, D. Jovanovic, M. Schaf
    Finding Inconsistencies in Programs with Loops. In LPAR'15 .
  3. A. Gurfinkel , T. Kahsai, A.   Komuravelli, J. A. Navas,
    The SeaHorn Verification Framework (PDF) . In CAV'15.
  4. 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.
  5. 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.
  6. A. Gurfinkel , T. Kahsai, J. A. Navas,
    Algorithmic Logic-Based Verification (PDF) . In ACM Special Interest Group on Logic and Computation (SIGLOG) April, 2015.
  7. A. Gurfinkel , T. Kahsai, J. A. Navas,
    SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (PDF) . In TACAS'15.
  8. 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.
  9. 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
  10. G. Brat, J. A. Navas, N. Shi, A. Venet.
    IKOS: A Framework for Static Analysis based on Abstract Interpretation (PDF) . In SEFM'14 .
  11. E. De Angelis, F. Fioravanti, J. A. Navas, M. Proietti,
    Verification of Programs by Combining Iterated Specialization with Interpolation (PDF) . In HCVS'14
  12. G. Gange, J. A. Navas, P. Schachte, H. Sondergaard, P. J. Stuckey.
    Abstract Interpretation over Non-Lattice Abstract Domains (PDF) . In SAS'13
  13. 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
  14. J. Jaffar, V. Murali, J. A. Navas.
    Boosting Concolic Testing with Interpolation (PDF) . In FSE'13
  15. 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
  16. K.  Francis, J. A. Navas, P. J. Stuckey.
    Modelling Destructive Assignments (PDF) . In CP'13
  17. 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
  18. J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    TRACER: A Symbolic Execution Tool for Verification (PDF) . In CAV'12
  19. J. Jaffar, V. Murali, J. A. Navas, A. E. Santosa.
    Path-Sensitive Backward Slicing (PDF) . In SAS'12
  20. J. Jaffar, J. A. Navas, A. E. Santosa.
    Unbounded Symbolic Execution for Program Verification (PDF) . In RV'11
  21. E. Trias, J. A. Navas, E. S. Ackley, S. Forrest, M. Hermenegildo.
    Negative Ternary Set-Sharing (PDF) . In ICLP'08
  22. J. A. Navas, E. Mera, P. López-García, M. Hermenegildo.
    User-Definable Resource Bounds Analysis for Logic Programs (PDF) . In ICLP'07
  23. 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
  24. M. Méndez-Lojo, J. A. Navas, M. Hermenegildo.
    Efficient, Parametric Fixpoint Algorithm for Analysis of Java Bytecode (PDF) . In BYTECODE'07
  25. 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.
  • Crab : a language-agnostic engine for abstract interpretation.
  • Crab-LLVM : a static analyzer based on Crab for LLVM-based languages. Crab-LLVM is 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 -