| Kevm: A complete formal semantics of the ethereum virtual machine E Hildenbrandt, M Saxena, N Rodrigues, X Zhu, P Daian, D Guth, ... 2018 IEEE 31st Computer Security Foundations Symposium (CSF), 204-217, 2018 | 276 | 2018 |
| KJS: a complete formal semantics of JavaScript D Park, A Stefanescu, G Roşu PLDI'15, 346-356, 2015 | 143 | 2015 |
| Semantics-based program verifiers for all languages A Stefănescu, D Park, S Yuwen, Y Li, G Roşu ACM SIGPLAN Notices 51 (10), 74-91, 2016 | 110 | 2016 |
| Natural proofs for structure, data, and separation X Qiu, P Garg, A Ştefănescu, P Madhusudan PLDI'13 48 (6), 231-242, 2013 | 102 | 2013 |
| One-path reachability logic G Rosu, A Stefanescu, S Ciobâca, BM Moore LICS'13, 358-367, 2013 | 88 | 2013 |
| Checking reachability using matching logic G Rosu, A Stefanescu OOPSLA'12, 555-574, 2012 | 85 | 2012 |
| All-path reachability logic A Ştefănescu, Ş Ciobâcă, R Mereuta, BM Moore, TF Şerbănută, G Roşu RTA-TCLA'14, 425-440, 2014 | 74 | 2014 |
| Matching logic: a new program verification approach (NIER track) G Rosu, A Stefanescu 2011 33rd International Conference on Software Engineering (ICSE), 868-871, 2011 | 72 | 2011 |
| Recursive proofs for inductive tree data-structures P Madhusudan, X Qiu, A Stefanescu POPL'12 47 (1), 123-136, 2012 | 60 | 2012 |
| From hoare logic to matching logic reachability G Roşu, A Ştefănescu FM'12, 387-402, 2012 | 51 | 2012 |
| Towards a unified theory of operational and axiomatic semantics G Roşu, A Ştefănescu ICALP'12, 351-363, 2012 | 40 | 2012 |
| A constructor-based reachability logic for rewrite theories S Skeirik, A Stefanescu, J Meseguer International Symposium on Logic-Based Program Synthesis and Transformation …, 2017 | 32 | 2017 |
| Language definitions as rewrite theories V Rusu, D Lucanu, TF Şerbănuţă, A Arusoaie, A Ştefănescu, G Roşu Journal of Logical and Algebraic Methods in Programming 85 (1), 98-120, 2016 | 20 | 2016 |
| Language definitions as rewrite theories A Arusoaie, D Lucanu, V Rusu, TF Şerbănuţă, A Ştefănescu, G Roşu WRLA'14, 97-112, 2014 | 11 | 2014 |
| MatchC: A matching logic reachability verifier using the K framework A Stefanescu Electronic Notes in Theoretical Computer Science 304, 183-198, 2014 | 8 | 2014 |
| All-path reachability logic A Stefanescu, S Ciobâca, R Mereuta, B Moore, TF Serbanuta, G Rosu arXiv preprint arXiv:1810.10826, 2018 | 7 | 2018 |
| Verified Cryptographic Code for Everybody B Boston, S Breese, J Dodds, M Dodds, B Huffman, A Petcher, ... International Conference on Computer Aided Verification, 645-668, 2021 | 2 | 2021 |
| A type system for extracting functional specifications from memory-safe imperative programs P He, E Westbrook, B Carmer, C Phifer, V Robert, K Smeltzer, ... Proceedings of the ACM on Programming Languages (PACMPL) 5 (135), 1-135, 2021 | 1 | 2021 |
| Low-Level Program Verification using Matching Logic Reachability D Guth, A Stefanescu, G Rosu Proceedings of the LICS 13, 2013 | 1 | 2013 |
| Towards a unified theory of operational and axiomatic semantics—extended abstract G Rosu, A Stefanescu Technical Repor t http://hdl. handle. net/2142/30472, Univ. of Illinois, 2012 | 1 | 2012 |
Grigore RosuUniversity of Illinois at Urbana ChampaignVerifierad e-postadress på illinois.edu
