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