2 citations · 3 across the 4 of their papers we have counts for
6 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…
Asynchronous Muddy Children Puzzle (work in progress)
Dafina Trufaş, Ioan Teodorescu, Denisa Diaconescu +2
In this work-in-progress paper we explore using the recently introduced VLSM formalism to define and reason about the dynamics of agent-based systems. To this aim we use VLSMs to f…
From Hybrid Modal Logic to Matching Logic and Back
Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă
Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provid…
Operational semantics and program verification using many-sorted hybrid modal logic
Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta
We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our f…
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 many-sorted polyadic modal logic
Ioana Leustean, Natalia Moanga, Traian Florin Serbanuta
This paper presents a many-sorted polyadic modal logic that generalizes some of the existing approaches. The algebraic semantics has led us to a many-sorted generalization of boole…