Jorge A. Navas

Jorge A. Navas

Senior Computer Scientist at SRI International

PhD at The University of New Mexico (USA)


Contact Info

Computer Science Lab (CSL)
SRI International
jorge.navas@sri.com
Location: 333 Ravenswood Building E, Room L264
Menlo Park (CA) USA

Research

My passion is the design and implementation of practical tools that can help programmers to make more reliable and secure code. The goal of my research is to improve the process of verifying and testing complex software systems.

Software

Actively working on

No longer working on

Publications [ DBLP | Google Scholar ]

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

Service

Doctoral Dissertation