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

Software

  • 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.

Service

Doctoral Dissertation

Contact

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

Email: jorge.a.navaslaserna@nasa.gov


First Gov logo
NASA Logo - nasa.gov