Bio
I am a senior research fellow at
The University of
Melbourne working with
Peter Stuckey,
Harald Sondergaard,
and
Peter
Schachte.
Before I was a postdoc at
National University of
Singapore working with
Joxan Jaffar .
Previously, I got my PhD in Computer Science at
University of New Mexico
under the supervision of
Manuel Hermenegildo .
Before that I did my Bachelor in Computer Science at the
Technical University of Madrid
.
Research
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.
-
G. Gange,
J. A. Navas,
P. Schachte,
H. Sondergaard,
P. J. Stuckey,
Abstract
Interpretation over Non-Lattice Abstract Domains.
20th Static Analysis Symposium
(SAS'13)
-
G. Gange,
J. A. Navas,
P. Schachte,
H. Sondergaard,
P. J. Stuckey,
Unbounded Model Checking with Interpolation for
Regular Language Constraints.
19th Int. Conference on Tools and Algorithms for the Construction and Analysis
of Systems
(TACAS'13)
-
J. Jaffar,
V. Murali,
J. A. Navas,
Boosting Concolic Testing with Interpolation (to appear)
ACM SIGSOFT Symposium
on the Foundations of Software Engineering
(FSE'13)
-
K. Francis,
J. A. Navas,
P. J. Stuckey,
Modelling Destructive Assignments (to appear)
19th International Conference on Principles and Practice
of Constraint Progrmaming
(CP'13)
-
J. A. Navas,
P. Schachte,
H. Sondergaard,
P. J. Stuckey,
Signedness-Agnostic Program Analysis: Precise Integer
Bounds for Low-Level Code
10th Asian Symposium on Programming
Languages and Systems
(APLAS'12)
-
J. Jaffar,
V. Murali,
J. A. Navas,
A. E. Santosa
TRACER: A
Symbolic Execution Tool for Verification
24th Computer Aided Verification
(CAV'12)
-
J. Jaffar,
V. Murali,
J. A. Navas,
A. E. Santosa
Path-Sensitive Backward Slicing
19th Static Analysis Symposium
(SAS'12)
-
J. Jaffar,
J. A. Navas,
A. E. Santosa
Unbounded
Symbolic Execution for Program Verification
2nd Int. Conference on Runtime Verification
(RV'11)
-
J. A. Navas,
M. Méndez-Lojo,
M. Hermenegildo
Generic Resource Usage Bounds Analysis for
Java Bytecode
4th Workshop on Bytecode Semantics,
Verification, Analysis and
Transf.
(BYTECODE'09)
-
E. Trias,
J. A. Navas,
E. S. Ackley,
S. Forrest,
M. Hermenegildo
Negative Ternary Set-Sharing
24th International Conference on Logic Programming
(ICLP'08)
-
J. A. Navas,
E. Mera,
P. López-García,
M. Hermenegildo
User-Definable Resource Bounds Analysis
for Logic Programs
23rd
International Conference on Logic Programming
(ICLP'07)
-
M. Méndez-Lojo,
J. A. Navas,
M. Hermenegildo
A Flexible, (C)LP-based Approach to the Analysis of
Object-Oriented Programs
17th Int. Symposium on Logic-Based
Program Synthesis and Transf.
(LOPSTR'07)
-
M. Méndez-Lojo,
J. A. Navas,
M. Hermenegildo
Efficient, Parametric Fixpoint Algorithm
for Analysis of Java Bytecode
2nd Workshop on Bytecode Semantics, Verification,
Analysis and Transf.
(BYTECODE'07)
-
J. A. Navas,
F. Bueno,
M. Hermenegildo
Efficient top-down set-sharing analysis using cliques
8th Int. Symposium on Practical
Aspects of Declarative Languages
(PADL'06)
-
TRACER : a interpolation-based symbolic execution tool for
verification of C programs.
-
Revenant : a string solver for regular expressions.
-
FTCLP: a failure-based tabling interpreter for
Constraint-Logic Programming based on interpolation.
- The Ciao Preprocessor
: a program analyzer for debugging, verification, and
optimization for the Ciao programming language.
Teaching
- COMP90053 Program Analysis
and Transformation, 1st Semester 2013 (The University of
Melbourne, Graduate level)
Doctoral Dissertation
