Compartmented Threshold RSA Based on the Chinese Remainder Theorem. - Sorin Iftene; Stefan Ciobaca; Manuela Grindei (IACR Cryptol. ePrint Arch., 2008)

Protocol Composition for Arbitrary Primitives. - Stefan Ciobaca; Véronique Cortier (CSF, 2010)

Computing finite variants for subterm convergent rewrite systems. - Stefan Ciobaca (UNIF, 2011)

Verification and composition of security protocols with applications to electronic voting. (Vérification et composition des protocoles de securité avec des applications aux protocoles de vote electronique). - Stefan Ciobaca (2011)

Automated Verification of Equivalence Properties of Cryptographic Protocols. - Rohit Chadha; Stefan Ciobaca; Steve Kremer (ESOP, 2012)

Computing Knowledge in Security Protocols Under Convergent Equational Theories. - Stefan Ciobaca; Stéphanie Delaune; Steve Kremer (J. Autom. Reason., 2012)

From Small-Step Semantics to Big-Step Semantics, Automatically. - Stefan Ciobaca (IFM, 2013)

One-Path Reachability Logic. - Grigore Rosu; Andrei Stefanescu; Stefan Ciobaca; Brandon M. Moore (LICS, 2013)

A Language-Independent Proof System for Mutual Program Equivalence. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (ICFEM, 2014)

Reducing Partial Equivalence to Partial Correctness. - Stefan Ciobaca (SYNASC, 2014)

A Theoretical Foundation for Programming Languages Aggregation. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (WADT, 2014)

A language-independent proof system for full program equivalence. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (Formal Aspects Comput., 2016)

Automated Verification of Equivalence Properties of Cryptographic Protocols. - Rohit Chadha; Vincent Cheval; Stefan Ciobaca; Steve Kremer (ACM Trans. Comput. Log., 2016)

A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code. - Andrei Arusoaie; Stefan Ciobaca; Vlad Craciun; Dragos Gavrilut; Dorel Lucanu (SYNASC, 2017)

A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. - Stefan Ciobaca; Dorel Lucanu (IJCAR, 2018)

Unification Modulo Builtins. - Stefan Ciobaca; Andrei Arusoaie; Dorel Lucanu (WoLLIC, 2018)

Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics. - Andrei-Sebastian Buruiana; Stefan Ciobaca (WPTE@FSCD, 2018)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (CoRR, 2019)

Verifying the DPLL Algorithm in Dafny. - Cezar-Constantin Andrici; Stefan Ciobaca (FROM, 2019)

All-Path Reachability Logic. - Andrei Stefanescu; Stefan Ciobaca; Radu Mereuta; Brandon M. Moore; Traian-Florin Serbanuta; Grigore Rosu (Log. Methods Comput. Sci., 2019)

Trace-Relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ESOP, 2020)

A Typo in the Paterson-Wegman-de Champeaux algorithm. - Valeriu Motroi; Stefan Ciobaca (CoRR, 2020)

Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny. - Cezar-Constantin Andrici; Stefan Ciobaca (CoRR, 2020)

Verifying the Conversion into CNF in Dafny. - Viorel Iordache; Stefan Ciobaca (WoLLIC, 2021)

A Note on the Performance of Algorithms for Solving Linear Diophantine Equations in the Naturals. - Valeriu Motroi; Stefan Ciobaca (CoRR, 2021)

An Extended Account of Trace-relating Compiler Correctness and Secure Compilation. - Carmine Abate; Roberto Blanco; Stefan Ciobaca; Adrien Durier; Deepak Garg 001; Catalin Hritcu; Marco Patrignani; Éric Tanter; Jérémy Thibault (ACM Trans. Program. Lang. Syst., 2021)

Operationally-based program equivalence proofs using LCTRSs. - Stefan Ciobaca; Dorel Lucanu; Andrei-Sebastian Buruiana (J. Log. Algebraic Methods Program., 2023)

Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Study. - Stefan Ciobaca; Diana-Elena Gratie (IFM, 2024)

Securing Verified IO Programs Against Unverified Code in F. - Cezar-Constantin Andrici; Stefan Ciobaca; Catalin Hritcu; Guido Martínez; Exequiel Rivas; Éric Tanter; Théo Winterhalter (Proc. ACM Program. Lang., 2024)