Bio
I am a research fellow at
The University of
Melbourne working with Profs.
Peter Stuckey,
Harald Sondergaard,
and
Peter Schachte.
Before I was a postdoc at
National University of
Singapore working with Prof.
J.Jaffar .
Previously, I got my PhD in Computer Science at
University of New Mexico
under the supervision of Prof.
M. 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 involve the design and implementation of practical
tools for software verification
and program analysis.
Publications
( DBLP )
Program Verification
-
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,
J. A. Navas,
A. E. Santosa
Unbounded
Symbolic Execution for Program Verification
2nd Int. Conference on Runtime Verification
(RV'11)
Program Debugging and Understanding
-
J. Jaffar,
V. Murali,
J. A. Navas,
A. E. Santosa
Path Sensitive Backward Slicing (To appear)
19th International Static Analysis Symposium
(SAS'12)
Analysis of Logic Programs
-
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)
-
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)
Analysis of Java Bytecode
-
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)
-
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)
Software (I have developed)
-
TRACER : a interpolation-based symbolic execution tool for
verification of C programs.
Software (I have been involved)
-
The Ciao Preprocessor (A global program analyzer and static
debugger and optimizer for Ciao programming language)
Doctoral Dissertation