| The SeaHorn verification framework A Gurfinkel, T Kahsai, A Komuravelli, JA Navas International Conference on Computer Aided Verification, 343-361, 2015 | 307 | 2015 |
| TRACER: a symbolic execution tool for verification J Jaffar, V Murali, JA Navas, AE Santosa Computer Aided Verification, 758-766, 2012 | 140 | 2012 |
| User-definable resource bounds analysis for logic programs J Navas, E Mera, P López-García, MV Hermenegildo International Conference on Logic Programming, 348-363, 2007 | 118 | 2007 |
| A flexible,(C) LP-based approach to the analysis of object-oriented programs M Méndez-Lojo, J Navas, MV Hermenegildo International Symposium on Logic-Based Program Synthesis and Transformation …, 2007 | 93 | 2007 |
| Boosting concolic testing via interpolation J Jaffar, V Murali, JA Navas Proceedings of the 2013 9th Joint Meeting on Foundations of Software …, 2013 | 70 | 2013 |
| SeaHorn: A framework for verifying C programs (competition contribution) A Gurfinkel, T Kahsai, JA Navas International Conference on Tools and Algorithms for the Construction and …, 2015 | 62 | 2015 |
| Unbounded symbolic execution for program verification J Jaffar, JA Navas, AE Santosa International Conference on Runtime Verification, 396-411, 2011 | 59 | 2011 |
| User-definable resource usage bounds analysis for Java bytecode J Navas, M Méndez-Lojo, MV Hermenegildo Electronic Notes in Theoretical Computer Science 253 (5), 65-82, 2009 | 58 | 2009 |
| IKOS: A framework for static analysis based on abstract interpretation G Brat, JA Navas, N Shi, A Venet International Conference on Software Engineering and Formal Methods, 271-277, 2014 | 57 | 2014 |
| Simple and precise static analysis of untrusted linux kernel extensions E Gershuni, N Amit, A Gurfinkel, N Narodytska, JA Navas, N Rinetzky, ... Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019 | 45 | 2019 |
| Safe upper-bounds inference of energy consumption for Java bytecode applications J Navas, M Méndez-Lojo, MV Hermenegildo Proceedings of The Sixth NASA Langley Formal Methods Workshop, 2008 | 39 | 2008 |
| An abstract domain of uninterpreted functions G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey International Conference on Verification, Model Checking, and Abstract …, 2016 | 31 | 2016 |
| Abstract interpretation over non-lattice abstract domains G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey International Static Analysis Symposium, 6-24, 2013 | 31 | 2013 |
| Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code JA Navas, P Schachte, H Søndergaard, PJ Stuckey Programming Languages and Systems, 115-130, 2012 | 31 | 2012 |
| A Context-Sensitive Memory Model for Verification of C/C++ Programs A Gurfinkel, JA Navas International Static Analysis Symposium, 148-168, 2017 | 29 | 2017 |
| Horn clauses as an intermediate representation for program analysis and transformation G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey Theory and Practice of Logic Programming 15 (4-5), 526-542, 2015 | 25 | 2015 |
| Exploiting sparsity in difference-bound matrices G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey International Static Analysis Symposium, 189-211, 2016 | 24 | 2016 |
| Unbounded model-checking with interpolation for regular language constraints G Gange, JA Navas, PJ Stuckey, H Søndergaard, P Schachte International Conference on Tools and Algorithms for the Construction and …, 2013 | 24 | 2013 |
| Failure tabled constraint logic programming by interpolation G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey Theory and Practice of Logic Programming 13 (4-5), 593-607, 2013 | 23 | 2013 |
| An efficient, parametric fixpoint algorithm for analysis of Java bytecode M Méndez, J Navas, MV Hermenegildo Electronic Notes in Theoretical Computer Science 190 (1), 51-66, 2007 | 22 | 2007 |
Arie GurfinkelUniversity of WaterlooVerified email at uwaterloo.ca
