Stefan Ciobaca

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