Andrei Stefanescu

According to our database, Andrei Stefanescu authored at least 17 papers between 2011 and 2021.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2021

A type system for extracting functional specifications from memory-safe imperative programs.

Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Stefanescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic

Proc. ACM Program. Lang., 2021

Verified Cryptographic Code for Everybody.

Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, Andrei Stefanescu

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

A Constructor-Based Reachability Logic for Rewrite Theories.

Stephen Skeirik, Andrei Stefanescu, José Meseguer

Fundam. Informaticae, 2020

2019

All-Path Reachability Logic.

Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu

Log. Methods Comput. Sci., 2019

2018

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.

Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, Grigore Rosu

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2016

Toward language-independent program verification

Andrei Stefanescu

PhD thesis, 2016

Language definitions as rewrite theories.

Vlad Rusu, Dorel Lucanu, Traian-Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu

J. Log. Algebraic Methods Program., 2016

Semantics-based program verifiers for all languages.

Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

2015

KJS: a complete formal semantics of JavaScript.

Daejun Park, Andrei Stefanescu, Grigore Rosu

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

2013

Natural proofs for structure, data, and separation.

Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, Parthasarathy Madhusudan

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2013

One-Path Reachability Logic.

Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

2012

Recursive proofs for inductive tree data-structures.

Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Checking reachability using matching logic.

Grigore Rosu, Andrei Stefanescu

Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

Towards a Unified Theory of Operational and Axiomatic Semantics.

Grigore Rosu, Andrei Stefanescu

Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

From Hoare Logic to Matching Logic Reachability.

Grigore Rosu, Andrei Stefanescu

Proceedings of the FM 2012: Formal Methods, 2012

2011

MatchC: A Matching Logic Reachability Verifier Using the K Framework.

Andrei Stefanescu

Proceedings of the Second International Workshop on the K Framework and its Applications, 2011

Matching logic: a new program verification approach.

Grigore Rosu, Andrei Stefanescu

Proceedings of the 33rd International Conference on Software Engineering, 2011