Andrei Stefanescu

23 papers A* 5A 3B 1C 1Journal 7Unranked 5
YearRankTypeTitle / Venue / Authors
2024 J jnl
Macaw: A Machine Code Toolbox for the Busy Binary Analyst.
CoRR
Ryan G. Scott, Brett Boston, Benjamin Davis, Iavor S. Diatchki, Mike Dodds, Joe Hendrix, Daniel Matichuk, Kevin Quick, Tristan Ravitch, Valentin Robert, Benjamin Selfridge, Andrei Stefanescu, Daniel Wagner, Simon Winwood
2021 J jnl
A type system for extracting functional specifications from memory-safe imperative programs.
Proc. ACM Program. Lang.
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
2021 — conf
Verified Cryptographic Code for Everybody.
CAV (1)
Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, Andrei Stefanescu
2020 J jnl
A Constructor-Based Reachability Logic for Rewrite Theories.
Fundam. Informaticae
Stephen Skeirik, Andrei Stefanescu, José Meseguer
2019 J jnl
All-Path Reachability Logic.
Log. Methods Comput. Sci.
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
2018 J jnl
All-Path Reachability Logic.
CoRR
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
2018 A conf
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.
CSF
Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, Grigore Rosu
2017 C conf
A Constructor-Based Reachability Logic for Rewrite Theories.
LOPSTR
Stephen Skeirik, Andrei Stefanescu, José Meseguer
2017 J jnl
A Constructor-Based Reachability Logic for Rewrite Theories.
CoRR
Stephen Skeirik, Andrei Stefanescu, José Meseguer
2016 J jnl
Language definitions as rewrite theories.
J. Log. Algebraic Methods Program.
Vlad Rusu, Dorel Lucanu, Traian-Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu
2016 A conf
Semantics-based program verifiers for all languages.
OOPSLA
Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu
2016 — —
Toward language-independent program verification
Andrei Stefanescu
2015 A* conf
KJS: a complete formal semantics of JavaScript.
PLDI
Daejun Park, Andrei Stefanescu, Grigore Rosu
2014 — conf
All-Path Reachability Logic.
RTA-TLCA
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
2014 — conf
Language Definitions as Rewrite Theories.
WRLA
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu
2013 A* conf
Natural proofs for structure, data, and separation.
PLDI
Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, Parthasarathy Madhusudan
2013 A* conf
One-Path Reachability Logic.
LICS
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore
2012 A conf
Checking reachability using matching logic.
OOPSLA
Grigore Rosu, Andrei Stefanescu
2012 B conf
From Hoare Logic to Matching Logic Reachability.
FM
Grigore Rosu, Andrei Stefanescu
2012 A* conf
Recursive proofs for inductive tree data-structures.
POPL
Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu
2012 — conf
Towards a Unified Theory of Operational and Axiomatic Semantics.
ICALP (2)
Grigore Rosu, Andrei Stefanescu
2011 — conf
MatchC: A Matching Logic Reachability Verifier Using the K Framework.
K
Andrei Stefanescu
2011 A* conf
Matching logic: a new program verification approach.
ICSE
Grigore Rosu, Andrei Stefanescu