| The SeaHorn verification framework A Gurfinkel, T Kahsai, A Komuravelli, JA Navas International Conference on Computer Aided Verification, 343-361, 2015 | 454 | 2015 |
| TRACER: a symbolic execution tool for verification J Jaffar, V Murali, JA Navas, AE Santosa Computer Aided Verification, 758-766, 2012 | 163 | 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 | 120 | 2007 |
| 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 | 115 | 2019 |
| 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 | 103 | 2014 |
| 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 | 96 | 2007 |
| Boosting concolic testing via interpolation J Jaffar, V Murali, JA Navas Proceedings of the 2013 9th Joint Meeting on Foundations of Software …, 2013 | 85 | 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 | 72 | 2015 |
| Unbounded symbolic execution for program verification J Jaffar, JA Navas, AE Santosa Runtime Verification: Second International Conference, RV 2011, San …, 2012 | 66 | 2012 |
| 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 | 62 | 2009 |
| 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 | 44 | 2016 |
| A Context-Sensitive Memory Model for Verification of C/C++ Programs A Gurfinkel, JA Navas International Static Analysis Symposium, 148-168, 2017 | 42 | 2017 |
| 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 | 38 | 2012 |
| 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 | 37 | 2008 |
| Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE S Wesley, M Christakis, JA Navas, R Trefler, V Wüstholz, A Gurfinkel Verification, Model Checking, and Abstract Interpretation: 23rd …, 2022 | 34 | 2022 |
| 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 | 34 | 2013 |
| 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 | 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 | 30 | 2015 |
| Interval analysis and machine arithmetic: Why signedness ignorance is bliss G Gange, JA Navas, P Schachte, H Søndergaard, PJ Stuckey ACM Transactions on Programming Languages and Systems (TOPLAS) 37 (1), 1-35, 2015 | 29 | 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 | 28 | 2016 |
Arie GurfinkelUniversity of WaterlooE-mail megerősítve itt: uwaterloo.ca