Andrei Stefanescu

Publication Activity (10 Years)

Years Active: 2011-2024
Publications (10 Years): 11

Top Topics

Formal Semantics

Defeasible Logic

Propositional Theories

Closed World Assumptions

Top Venues

Proc. ACM Program. Lang.

J. Log. Algebraic Methods Program.

Publications

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