| The SeaHorn verification framework A Gurfinkel, T Kahsai, A Komuravelli, JA Navas Computer Aided Verification: 27th International Conference, CAV 2015, San …, 2015 | 350 | 2015 |
| TRACER: a symbolic execution tool for verification J Jaffar, V Murali, JA Navas, AE Santosa Computer Aided Verification, 758-766, 2012 | 147 | 2012 |
| User-definable resource bounds analysis for logic programs J Navas, E Mera, P López-García, MV Hermenegildo Logic Programming: 23rd International Conference, ICLP 2007, Porto, Portugal …, 2007 | 122 | 2007 |
| A flexible,(C) LP-based approach to the analysis of object-oriented programs M Méndez-Lojo, J Navas, MV Hermenegildo Logic-Based Program Synthesis and Transformation: 17th International …, 2008 | 94 | 2008 |
| Boosting concolic testing via interpolation J Jaffar, V Murali, JA Navas Proceedings of the 2013 9th Joint Meeting on Foundations of Software …, 2013 | 75 | 2013 |
| IKOS: A framework for static analysis based on abstract interpretation G Brat, JA Navas, N Shi, A Venet Software Engineering and Formal Methods: 12th International Conference, SEFM …, 2014 | 69 | 2014 |
| SeaHorn: A framework for verifying C programs (competition contribution) A Gurfinkel, T Kahsai, JA Navas Tools and Algorithms for the Construction and Analysis of Systems: 21st …, 2015 | 64 | 2015 |
| Unbounded symbolic execution for program verification J Jaffar, JA Navas, AE Santosa Runtime Verification: Second International Conference, RV 2011, San …, 2012 | 60 | 2012 |
| 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 | 59 | 2019 |
| 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 | 57 | 2009 |
| 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 |
| 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 | 36 | 2012 |
| A Context-Sensitive Memory Model for Verification of C/C++ Programs A Gurfinkel, JA Navas Static Analysis: 24th International Symposium, SAS 2017, New York, NY, USA …, 2017 | 35 | 2017 |
| An abstract domain of uninterpreted functions G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey Verification, Model Checking, and Abstract Interpretation: 17th …, 2016 | 35 | 2016 |
| Abstract interpretation over non-lattice abstract domains G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey Static Analysis: 20th International Symposium, SAS 2013, Seattle, WA, USA …, 2013 | 31 | 2013 |
| 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 | 28 | 2015 |
| Exploiting sparsity in difference-bound matrices G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey Static Analysis: 23rd International Symposium, SAS 2016, Edinburgh, UK …, 2016 | 26 | 2016 |
| Unbounded model-checking with interpolation for regular language constraints G Gange, JA Navas, PJ Stuckey, H Søndergaard, P Schachte Tools and Algorithms for the Construction and Analysis of Systems: 19th …, 2013 | 25 | 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 | 24 | 2007 |
| 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 |
Arie GurfinkelUniversity of WaterlooVerified email at uwaterloo.ca
