Synthesizing software verifiers from proof rules S Grebenshchikov, NP Lopes, C Popeea, A Rybalchenko PLDI’12, 2012 | 356 | 2012 |
Checking Beliefs in Dynamic Networks NP Lopes, N Bjørner, P Godefroid, K Jayaraman, G Varghese | 242 | 2015 |
Provably correct peephole optimizations with alive NP Lopes, D Menendez, S Nagarakatte, J Regehr Proceedings of the 36th ACM SIGPLAN Conference on Programming Language …, 2015 | 173 | 2015 |
Automatically verifying reachability and well-formedness in P4 Networks NP Lopes, N Bjørner, N McKeown, A Rybalchenko, D Talayco, ... Microsoft Research, 1-13, 2016 | 165* | 2016 |
Crystalnet: Faithfully emulating large production networks HH Liu, Y Zhu, J Padhye, J Cao, S Tallapragada, NP Lopes, ... Proceedings of the 26th Symposium on Operating Systems Principles, 599-613, 2017 | 125 | 2017 |
Scaling network verification using symmetry and surgery GD Plotkin, N Bjørner, NP Lopes, A Rybalchenko, G Varghese Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016 | 102 | 2016 |
Alive2: bounded translation validation for LLVM NP Lopes, J Lee, CK Hur, Z Liu, J Regehr Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 94 | 2021 |
Taming Undefined Behavior in LLVM J Lee, Y Kim, Y Song, CK Hur, S Das, D Majnemer, J Regehr, NP Lopes PLDI, 2017 | 89 | 2017 |
HSF (C): A Software Verifier Based on Horn Clauses: (Competition Contribution) S Grebenshchikov, A Gupta, NP Lopes, C Popeea, A Rybalchenko Tools and Algorithms for the Construction and Analysis of Systems: 18th …, 2012 | 89 | 2012 |
A design and verification methodology for secure isolated regions R Sinha, M Costa, A Lal, NP Lopes, S Rajamani, SA Seshia, K Vaswani Proceedings of the 37th ACM SIGPLAN Conference on Programming Language …, 2016 | 83 | 2016 |
Reconciling high-level optimizations and low-level code in LLVM J Lee, CK Hur, R Jung, Z Liu, J Regehr, NP Lopes Proceedings of the ACM on Programming Languages 2 (OOPSLA), 1-28, 2018 | 37 | 2018 |
Fast BGP simulation of large datacenters NP Lopes, A Rybalchenko Verification, Model Checking, and Abstract Interpretation: 20th …, 2019 | 36 | 2019 |
Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic NP Lopes, J Monteiro International Journal on Software Tools for Technology Transfer 18, 359-374, 2016 | 36 | 2016 |
Practical verification of peephole optimizations with Alive NP Lopes, D Menendez, S Nagarakatte, J Regehr Communications of the ACM 61 (2), 84-91, 2018 | 33 | 2018 |
Network verification in the light of program verification NP Lopes, N Bjørner, P Godefroid, G Varghese MSR, Rep, 2013 | 24 | 2013 |
Applying Prolog to develop distributed systems NP Lopes, JA Navarro, A Rybalchenko, A Singh Theory and Practice of Logic Programming 10 (4-6), 691-707, 2010 | 23 | 2010 |
Distributed and predictable software model checking N Lopes, A Rybalchenko Verification, Model Checking, and Abstract Interpretation, 340-355, 2011 | 19 | 2011 |
Weakest precondition synthesis for compiler optimizations NP Lopes, J Monteiro International Conference on Verification, Model Checking, and Abstract …, 2014 | 18 | 2014 |
AliveInLean: a verified LLVM peephole optimization verifier J Lee, CK Hur, NP Lopes Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019 | 14 | 2019 |
Supercharging plant configurations using Z3 N Bjørner, M Levatich, NP Lopes, A Rybalchenko, C Vuppalapati Integration of Constraint Programming, Artificial Intelligence, and …, 2021 | 11 | 2021 |