5 citations · 17 across the 11 of their papers we have counts for
3 papers · 1 filter
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…