Zobrazeno 1 - 10
of 30
pro vyhledávání: '"Ciobâcă, Ştefan"'
Autor:
Ciobâcǎ, Ştefan
Cette these concerne la verification formelle et la composition de protocoles de securite, motivees en particulier par l'analyse des protocoles de vote electronique. Les chapitres 3 a 5 ont comme sujet la verification de protocoles de securite et le
Externí odkaz:
http://www.theses.fr/2011DENS0059/document
Autor:
Andrici, Cezar-Constantin, Ciobaca, Stefan, Hritcu, Catalin, Martínez, Guido, Rivas, Exequiel, Tanter, Éric, Winterhalter, Théo
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 verified program interacts with its IO-performing context via a higher-o
Externí odkaz:
http://arxiv.org/abs/2303.01350
Autor:
Motroi, Valeriu, Ciobaca, Stefan
We implement four algorithms for solving linear Diophantine equations in the naturals: a lexicographic enumeration algorithm, a completion procedure, a graph-based algorithm, and the Slopes algorithm. As already known, the lexicographic enumeration a
Externí odkaz:
http://arxiv.org/abs/2104.05200
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 termination are computer checked). We benchmark our Dafny solver and we
Externí odkaz:
http://arxiv.org/abs/2007.10842
Autor:
Motroi, Valeriu, Ciobaca, Stefan
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 provide a fix.
Comment: Unification Algorithm
Comment: Unification Algorithm
Externí odkaz:
http://arxiv.org/abs/2007.00304
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 (LCTRSs) and the two programs as terms. The main feature of our method is
Externí odkaz:
http://arxiv.org/abs/2001.09649
Publikováno v:
In Journal of Logical and Algebraic Methods in Programming October 2023 135
Publikováno v:
EPTCS 303, 2019, pp. 3-15
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 which can be checked independently in the form of a satisfying truth as
Externí odkaz:
http://arxiv.org/abs/1909.01743
Autor:
Abate, Carmine, Blanco, Roberto, Ciobaca, Stefan, Durier, Adrien, Garg, Deepak, Hritcu, Catalin, Patrignani, Marco, Tanter, Éric, Thibault, Jérémy
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 equivalent to the preservation of all trace properties. Here traces collect,
Externí odkaz:
http://arxiv.org/abs/1907.05320
Publikováno v:
EPTCS 289, 2019, pp. 1-16
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 expression whose value decreases with each program step in a well-founded ord
Externí odkaz:
http://arxiv.org/abs/1902.08419