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 Laserna J, Schachte P, Sondergaard H, Stuckey P. A tool for intersecting context-free grammars and its applications. 7th NASA Formal Methods Symposium (NFM). Springer International Publishing. 2015, Vol. 9058. Editors: Havelund K, Holzmann G, Joshi R. DOI: 10.1007/978-3-319-17524-9_31
  2. Cornish JR, Gange G, Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. Analyzing Array Manipulating Programs by Program Transformation. 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR). Springer International Publishing. 2015, Vol. 8981. Editors: Proietti M, Seki H. DOI: 10.1007/978-3-319-17822-6_1
  3. Gange G, Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. Horn Clauses As an Intermediate Representation for Program Analysis and Transformation. 31st International Conference on Logic Programming (ICLP) Co-located with the 21st International Conference on Principles and Practice of Constraint Programming (CP). Cambridge University Press. 2015, Vol. 15, Issue 4-5. DOI: 10.1017/S1471068415000204
  4. Gange G, Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. 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. DOI: 10.1145/2651360
  5. Gange G, Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. Abstract Interpretation over Non-Lattice Abstract Domains. 20th Static Analysis Symposium. Springer Verlag. 2013, Vol. 7935. Editors: Logozzo F, Fahndrich M. DOI: 10.1007/978-3-642-38856-9_3
  6. Jaffar J, Murali V, Navas Laserna J. Boosting Concolic Testing via Interpolation. 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. DOI: 10.1145/2491411.2491425
  7. Gange G, Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. Failure tabled constraint logic programming by interpolation. 29th International Conference on Logic Programming ICLP. Cambridge University Press. 2013, Vol. 13, Issue 4-5. DOI: 10.1017/S1471068413000379
  8. Francis K, Navas Laserna J, Stuckey P. Modelling Destructive Assignments. 19th International Conference on Principles and Practice of Constraint Programming. Springer Verlag. 2013. Editors: Schulte C. DOI: 10.1007/978-3-642-40627-0_26
  9. Gange G, Navas Laserna J, Stuckey P, Sondergaard H, Schachte P. Unbounded model-checking with interpolation for regular language constraints. 19th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer Verlag. 2013, Vol. 7795. Editors: Piterman N, Smolka SA. DOI: 10.1007/978-3-642-36742-7_20
  10. Jaffar J, Murali V, Navas Laserna J, Santosa A. Path-Sensitive Backward Slicing. Lecture Notes in Computer Science. Springer-Verlag Heidelberg. 2012, Vol. 7460.
  11. Navas Laserna J, Schachte P, Sondergaard H, Stuckey P. Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code. 10th Asian Symposium on Programming Languages and Systems (APLAS). Springer Verlag. 2012, Vol. 7705. Editors: Jhala R, Igarashi A. DOI: 10.1007/978-3-642-35182-2_9
  12. Jaffar J, Murali V, Navas Laserna J, Santosa AE. TRACER: A symbolic execution tool for verification. Computer Aided Verification. Springer Verlag. 2012, Vol. 7358 LNCS. DOI: 10.1007/978-3-642-31424-7_61
  13. Jaffar J, Navas Laserna J, Santosa A. Unbounded Symbolic Execution for Program Verification. Lecture Notes in Computer Science. Springer-Verlag Heidelberg. 2012, Vol. 7186.