4 citations · 6 across the 4 of their papers we have counts for
8 papers
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…