Stefan Ciobaca

ORCID

Publication Activity (10 Years)

Years Active: 2008-2024
Publications (10 Years): 20

Top Venues

CoRR

SYNASC

WoLLIC

J. Log. Algebraic Methods Program.

École normale supérieure de Cachan, France (PHD)

Education History

École normale supérieure de Cachan, France

PHD

Publications

Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter
Securing Verified IO Programs Against Unverified Code in F. Proc. ACM Program. Lang. 8 (POPL) (2024)
Stefan Ciobaca, Dorel Lucanu, Andrei-Sebastian Buruiana
Operationally-based program equivalence proofs using LCTRSs. J. Log. Algebraic Methods Program. 135 (2023)
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
An Extended Account of Trace-relating Compiler Correctness and Secure Compilation. ACM Trans. Program. Lang. Syst. 43 (4) (2021)
Valeriu Motroi, Stefan Ciobaca
A Note on the Performance of Algorithms for Solving Linear Diophantine Equations in the Naturals. CoRR (2021)
Viorel Iordache, Stefan Ciobaca
Verifying the Conversion into CNF in Dafny. WoLLIC (2021)
Cezar-Constantin Andrici, Stefan Ciobaca
Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny. CoRR (2020)
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
Trace-Relating Compiler Correctness and Secure Compilation. ESOP (2020)
Stefan Ciobaca, Dorel Lucanu, Andrei-Sebastian Buruiana
Operationally-based Program Equivalence Proofs using LCTRSs. CoRR (2020)
Valeriu Motroi, Stefan Ciobaca
A Typo in the Paterson-Wegman-de Champeaux algorithm. CoRR (2020)
Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault
Trace-Relating Compiler Correctness and Secure Compilation. CoRR (2019)
Cezar-Constantin Andrici, Stefan Ciobaca
Verifying the DPLL Algorithm in Dafny. FROM (2019)
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
All-Path Reachability Logic. Log. Methods Comput. Sci. 15 (2) (2019)
Stefan Ciobaca, Andrei Arusoaie, Dorel Lucanu
Unification Modulo Builtins. WoLLIC (2018)
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
All-Path Reachability Logic. CoRR (2018)
Stefan Ciobaca, Dorel Lucanu
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. IJCAR (2018)
Andrei-Sebastian Buruiana, Stefan Ciobaca
Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics. WPTE@FSCD (2018)
Stefan Ciobaca, Dorel Lucanu
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. CoRR (2018)
Andrei Arusoaie, Stefan Ciobaca, Vlad Craciun, Dragos Gavrilut, Dorel Lucanu
A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code. SYNASC (2017)
Rohit Chadha, Vincent Cheval, Stefan Ciobaca, Steve Kremer
Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Trans. Comput. Log. 17 (4) (2016)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A language-independent proof system for full program equivalence. Formal Aspects Comput. 28 (3) (2016)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A Language-Independent Proof System for Mutual Program Equivalence. ICFEM (2014)
Stefan Ciobaca
Reducing Partial Equivalence to Partial Correctness. SYNASC (2014)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A Theoretical Foundation for Programming Languages Aggregation. WADT (2014)
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
All-Path Reachability Logic. RTA-TLCA (2014)
Stefan Ciobaca
From Small-Step Semantics to Big-Step Semantics, Automatically. IFM (2013)
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore
One-Path Reachability Logic. LICS (2013)
Rohit Chadha, Stefan Ciobaca, Steve Kremer
Automated Verification of Equivalence Properties of Cryptographic Protocols. ESOP (2012)
Stefan Ciobaca, Stéphanie Delaune, Steve Kremer
Computing Knowledge in Security Protocols Under Convergent Equational Theories. J. Autom. Reason. 48 (2) (2012)
Stefan Ciobaca
Computing finite variants for subterm convergent rewrite systems. UNIF (2011)
Stefan Ciobaca, Véronique Cortier
Protocol Composition for Arbitrary Primitives. CSF (2010)
Stefan Ciobaca, Stéphanie Delaune, Steve Kremer
Computing Knowledge in Security Protocols under Convergent Equational Theories. CADE (2009)
Sorin Iftene, Stefan Ciobaca, Manuela Grindei
Compartmented Threshold RSA Based on the Chinese Remainder Theorem. IACR Cryptol. ePrint Arch. 2008 (2008)

Stefan Ciobaca.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Stefan Ciobaca