5 citations · 17 across the 11 of their papers we have counts for
13 papers
The Formalization of two Computational Models in Dafny
Ştefan Ciobâc\b{a}, Diana-Elena Gratie, Dragoş-Irinel Rotariu
We describe the formalization in Dafny of two computational models, Turing Machines and the Lambda Calculus. We present several application of the formalizations: machine proofs of…
Formalizing the Omega Test in Dafny
Ariadna Brănici-Faraon, Ştefan Ciobâcă, Diana-Elena Gratie
We present a formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representat…
The Design of an Interactive Proof Mode for Dafny
Ştefan Ciobâcă, K. Rustan M. Leino, Ştefan-Alexandru Mercaş +1
We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype…
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu +4
We introduce SCIO*, a formally secure compilation framework for statically verified partial programs performing input-output (IO). The source language is an F* subset in which a ve…
A Note on the Performance of Algorithms for Solving Linear Diophantine Equations in the Naturals
Valeriu Motroi, Stefan Ciobaca
We implement four algorithms for solving linear Diophantine equations in the naturals: a lexicographic enumeration algorithm, a completion procedure, a graph-based algorithm, and t…
Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
Cezar-Constantin Andrici, Ştefan Ciobâcă
We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and te…
A Typo in the Paterson-Wegman-de Champeaux algorithm
Valeriu Motroi, Stefan Ciobaca
We investigate the Paterson-Wegman-de Champeaux linear-time unification algorithm. We show that there is a small mistake in the de Champeaux presentation of the algorithm and we pr…
Operationally-based Program Equivalence Proofs using LCTRSs
Ştefan Ciobâcă, Dorel Lucanu, Andrei Sebastian Buruiană
We propose an operationally-based deductive proof method for program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LC…
Verifying the DPLL Algorithm in Dafny
Cezar-Constantin Andrici, Ştefan Ciobâcă
Modern high-performance SAT solvers quickly solve large satisfiability instances that occur in practice. If the instance is satisfiable, then the SAT solver can provide a witness w…
Trace-Relating Compiler Correctness and Secure Compilation
Carmine Abate, Roberto Blanco, Stefan Ciobaca +6
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equiva…
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics
Andrei-Sebastian Buruiană, Ştefan Ciobâcă
We give a language-parametric solution to the problem of total correctness, by automatically reducing it to the problem of partial correctness, under the assumption that an express…
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 Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems
Ştefan Ciobâcă, Dorel Lucanu
We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-s…