2 citations · 2 across the 2 of their papers we have counts for
4 papers
Solving VeriContest with a Lean-Backed Rust Verifier
Traian Serbanuta, Jun Xu, Andrei Stefanescu +1
VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that…
Macaw: A Machine Code Toolbox for the Busy Binary Analyst
Ryan G. Scott, Brett Boston, Benjamin Davis +11
When attempting to understand the behavior of an executable, a binary analyst can make use of many different techniques. These include program slicing, dynamic instrumentation, bin…
All-Path Reachability Logic
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta +3
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path r…
A Constructor-Based Reachability Logic for Rewrite Theories
Stephen Skeirik, Andrei Stefanescu, José Meseguer
Reachability logic has been applied to rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also dis…