Följ
Andrei Stefanescu
Andrei Stefanescu
Research Engineer, Galois Inc
Verifierad e-postadress på stefanescu.io - Startsida
Titel
Citeras av
Citeras av
År
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
2762018
KJS: a complete formal semantics of JavaScript
D Park, A Stefanescu, G Roşu
PLDI'15, 346-356, 2015
1432015
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
1102016
Natural proofs for structure, data, and separation
X Qiu, P Garg, A Ştefănescu, P Madhusudan
PLDI'13 48 (6), 231-242, 2013
1022013
One-path reachability logic
G Rosu, A Stefanescu, S Ciobâca, BM Moore
LICS'13, 358-367, 2013
882013
Checking reachability using matching logic
G Rosu, A Stefanescu
OOPSLA'12, 555-574, 2012
852012
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
742014
Matching logic: a new program verification approach (NIER track)
G Rosu, A Stefanescu
2011 33rd International Conference on Software Engineering (ICSE), 868-871, 2011
722011
Recursive proofs for inductive tree data-structures
P Madhusudan, X Qiu, A Stefanescu
POPL'12 47 (1), 123-136, 2012
602012
From hoare logic to matching logic reachability
G Roşu, A Ştefănescu
FM'12, 387-402, 2012
512012
Towards a unified theory of operational and axiomatic semantics
G Roşu, A Ştefănescu
ICALP'12, 351-363, 2012
402012
A constructor-based reachability logic for rewrite theories
S Skeirik, A Stefanescu, J Meseguer
International Symposium on Logic-Based Program Synthesis and Transformation …, 2017
322017
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
202016
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
112014
MatchC: A matching logic reachability verifier using the K framework
A Stefanescu
Electronic Notes in Theoretical Computer Science 304, 183-198, 2014
82014
All-path reachability logic
A Stefanescu, S Ciobâca, R Mereuta, B Moore, TF Serbanuta, G Rosu
arXiv preprint arXiv:1810.10826, 2018
72018
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
22021
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
12021
Low-Level Program Verification using Matching Logic Reachability
D Guth, A Stefanescu, G Rosu
Proceedings of the LICS 13, 2013
12013
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
12012
Systemet kan inte utföra åtgärden just nu. Försök igen senare.
Artiklar 1–20