Dr Jorge Navas Laserna

  • Room: Level: 08 Room: 8.14
  • Building: Doug McDonell Building
  • Campus: Parkville

Research interests

  • Programing Languages in the area of program analysis, software verification, and automatic testing

Personal webpage

http://www.clip.dia.fi.upm.es/~jorge

Biography

Jorge A. Navas is currently a Research Scientist at NASA Ames Research Center. He received a Bachelor in Computer Science from Technical University of Madrid, Spain (2003) and a PhD in Computer Science from the University of New Mexico, USA in 2008. After graduation, he held post-doc positions at National University of Singapore (2008-2011) and The University of Melbourne (2011-2013). Jorge's primary research areas are programming languages, program analysis, software verification and testing. His work has been published in top conferences such as CAV, TACAS, SAS, FSE, and ICLP.

Recent publications

  1. Gange, G.; Navas, JA.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. A tool for intersecting context-free grammars and its applications. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer International Publishing. 2015, Vol. 9058, pp. 422-428. DOI: 10.1007/978-3-319-17524-9_31
  2. Cornish, JRM.; Gange, G.; Navas, JA.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. Analyzing Array Manipulating Programs by Program Transformation. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer International Publishing. 2015, Vol. 8981, pp. 3-20. DOI: 10.1007/978-3-319-17822-6_1
  3. Gange, G.; Navas Laserna, J.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. Horn Clauses As an Intermediate Representation for Program Analysis and Transformation. Theory and Practice of Logic Programming. Cambridge University Press. 2015, Vol. 15, Issue 4-5, pp. 526-542. DOI: 10.1017/S1471068415000204
  4. Gange, G.; Navas, JA.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss. ACM Transactions on Programming Languages and Systems. Association for Computing Machinery. 2015, Vol. 37, Issue 1, pp. 1:1-1:35. DOI: 10.1145/2651360
  5. Gange, G.; Navas, JA.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. Abstract Interpretation over Non-Lattice Abstract Domains. Static Analysis. Springer Berlin Heidelberg. 2013, Vol. 7935, pp. 6-24. DOI: 10.1007/978-3-642-38856-9_3
  6. Jaffar, J.; Murali, V.; Navas, JA. Boosting Concolic Testing via Interpolation. Proceedings of the 2013 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE). ACM Press. 2013, pp. 48-58. DOI: 10.1145/2491411.2491425
  7. Gange, G.; Navas, JA.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. Failure tabled constraint logic programming by interpolation. Theory and Practice of Logic Programming. CAMBRIDGE UNIV PRESS. 2013, Vol. 13, Issue 4-5, pp. 593-607. DOI: 10.1017/S1471068413000379
  8. Francis, K.; Navas, JA.; Stuckey, PJ. Modelling Destructive Assignments. Principles and Practice of Constraint Programming. Springer Verlag. 2013, Vol. 8124, pp. 315-330. DOI: 10.1007/978-3-642-40627-0_26
  9. Gange, G.; Navas, JA.; Stuckey, PJ.; Sondergaard, H.; Schachte, P. Unbounded model-checking with interpolation for regular language constraints. Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg. 2013, Vol. 7795, pp. 277-291. DOI: 10.1007/978-3-642-36742-7_20
  10. Jaffar, J.; Murali, V.; Navas, JA.; Santosa, A. Path-Sensitive Backward Slicing. Lecture Notes in Computer Science. Springer-Verlag Heidelberg. 2012, Vol. 7460.
  11. Navas, JA.; Schachte, P.; Sondergaard, H.; Stuckey, PJ. Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code. APLAS 2012: Proceedings of the 10th Asian Symposium on Programming Languages and Systems. Springer Berlin Heidelberg. 2012, Vol. 7705, pp. 115-130. DOI: 10.1007/978-3-642-35182-2_9
  12. Jaffar, J.; Murali, V.; Navas, JA.; Santosa, AE. TRACER: A symbolic execution tool for verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 2012, Vol. 7358 LNCS, pp. 758-766. DOI: 10.1007/978-3-642-31424-7_61
  13. Jaffar, J.; Navas, J.; Santosa, A. Unbounded Symbolic Execution for Program Verification. Lecture Notes in Computer Science. Springer-Verlag Heidelberg. 2012, Vol. 7186, pp. 758-766.