Ștefan Ciobâcă

• (NEW!) Verification Driven Program Development (Winter Semester 2024/2025)


• Logic in Computer Science (Winter Semester 2024/2025)


• Functional Programming (in Romanian, Summer Semester 2023/2024)

• I have presented at iFM 2024 the paper Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Study.

• April 10th, 2025: Presentation (slides) on A Game to Learn Natural Deduction for Propositional Logic at the Serious Games in Higher Education: Design, Facilitate and Reflect webinar, organized by the EC2U Alliance an REDICo.


• November 14th, 2024: Presentation (slides) of the paper Implementing, Specifying, and Verifying the QOI Format in Dafny: A Case Study at iFM 2024 in Manchester, UK (authors: Ștefan Ciobâcă, Diana-Elena Gratie)


• September 5th, 2019: Presentation on Verifying the DPLL Algorithm in Dafny at the Working Formal Methods Symposium, FROM 2019, Timișoara (authors: Cezar-Constantin Andrici, Ștefan Ciobâcă)


• July 1st, 2019: Slides and extra material on my ISR 2019 lecture on Logically Constrained Term Rewriting Systems.


• April 6th, 2019: Files for our presentation on Semantics-Based Proofs of Equivalence for Functions with Accumulators (Ștefan Ciobâcă, Dorel Lucanu and Sebastian Buruiană) at PERR 2019 (part of ETAPS 2019).


• July 28th, 2018: Presentation on Unification Modulo Builtins at WoLLIC 2018.


• July 14th, 2018: Presentation on A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems at IJCAR 2018 (part of FLOC 2018).


• July 8th, 2018: My coauthor Sebastian Buruiana gave a presentation on Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics at WPTE 2018.


• April, 2018: Presentation on Semantics-Parametric Program Equivalence (work-in-progress) at Dagstuhl Seminar on Program Equivalence.


• July 8th, 2017: Presentation on Proving reachability modulo theories at FROM 2017.


• May 31st, 2017: Presentation of the short paper Automatically Constructing a Type System from the Small-Step Semantics at TYPES 2017 (additional files) .


• May 15th, 2017: Presentation on RMT: a tool for rewriting modulo theories at INRIA Paris.


• April 11th - April 12th, 2016: Presentation at the Workshop on Program Equivalence.


• April 2nd - April 3rd, 2016: Presentation about proving program equivalence using matching logic at WRLA 2016 as part of the tutorial "Program Verification using Reachability Logic" given by Grigore Roșu, Andrei Ștefănescu and myself.

• See my DBLP profile for a more up-to-date list of publications.


• Cezar-Constantin Andrici, Ștefan Ciobâcă: Verifying the DPLL Algorithm in Dafny (FROM 2019). Abstract and BibTeX
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 assignment. However, if the instance is unsatisfiable, the certificates could be exponentially large or the SAT solver might not be able to output certificates. The implementation of the SAT solver should then be trusted not to contain bugs. However, the data structures and algorithms implemented by a typical high-performance SAT solver are complex enough to allow for subtle programming errors. To counter this issue, we build a verified SAT solver using the Dafny system. We discuss its implementation in the present article.

@Inproceedings{EPTCS303.1,
  author    = {Andrici, Cezar-Constantin and Ciob\^ac\u{a}, \c{S}tefan},
  year      = {2019},
  title     = {Verifying the {DPLL} Algorithm in {D}afny},
  editor    = {Marin, Mircea and Cr\u{a}ciun, Adrian},
  booktitle = {{\rm Proceedings Third Symposium on}
               Working Formal Methods,
               {\rm Timi\c{s}oara, Romania, 3-5 September 2019}},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {303},
  publisher = {Open Publishing Association},
  pages     = {3-15},
  doi       = {10.4204/EPTCS.303.1},
}		    



• 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 (arXiv:1907.05320). Abstract
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, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to a large class of secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.


• Andrei Ștefănescu, Ștefan Ciobâcă, Radu Mereuță, Brandom M. Moore, Grigore Roșu and Traian Florin Șerbănuță: All-path Reachability Logic (LMCS 2019). Abstract and BibTeX
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language. The soundness has also been mechanized in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org).

@article{lmcs:5408
  TITLE = {{All-Path Reachability Logic}},
  AUTHOR = {Stefanescu, Andrei and Ciobaca, Stefan and Mereuta, Radu and Moore, Brandon and Serbanuta, Traian Florin and Rosu, Grigore},
  URL = {https://lmcs.episciences.org/5408},
  DOI = {},
  JOURNAL = {{Logical Methods in Computer Science}},
  VOLUME = {{Volume 15, Issue 2}},
  YEAR = {2019},
  MONTH = Apr,
  KEYWORDS = {Computer Science - Programming Languages ; Computer Science - Formal Languages and Automata Theory ; Computer Science - Logic in Computer Science},
}		    



• Andrei-Sebastian Buruiană, Ştefan Ciobâcă : Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics (WPTE 2018). Abstract and BibTeX
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 order is provided. Our approach assumes that the programming language semantics is given as a rewrite theory. We implement a prototype on top of the RMT tool and we show that it works in practice on a number of examples.

@Inproceedings{EPTCS289.1,
  author    = {Buruian\u{a}, Andrei-Sebastian and Ciob\^ac\u{a}, \c{S}tefan},
  year      = {2019},
  title     = {Reducing Total Correctness to Partial Correctness by a Transformation of the Language Semantics},
  editor    = {Niehren, Joachim and Sabel, David},
  booktitle = {{\rm Proceedings Fifth International Workshop on}
               Rewriting Techniques for Program Transformations and Evaluation,
               {\rm Oxford, England, 8th July 2018}},
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {289},
  publisher = {Open Publishing Association},
  pages     = {1-16},
  doi       = {10.4204/EPTCS.289.1},
}
		    



• Ștefan Ciobâcă, Andrei Arusoaie, Dorel Lucanu: Unification Modulo Builtins (WoLLIC 2018).
Combining rewriting modulo an equational theory and SMT solving introduces new challenges in the area of term rewriting. One such challenge is unification of terms in the presence of equations and of uninterpreted and interpreted function symbols. The interpreted function symbols are part of a builtin model which can be reasoned about using an SMT solver. In this article, we formalize this problem, that we call unification modulo builtins. We show that under reasonable assumptions, complete sets of unifiers for unification modulo builtins problems can be effectively computed by reduction to usual E-unification problems and by relying on an oracle for SMT solving.

@inproceedings{DBLP:conf/wollic/CiobacaAL18,
  author    = {\c{S}tefan Ciob\^ac\u{a} and
               Andrei Arusoaie and
               Dorel Lucanu},
  title     = {Unification Modulo Builtins},
  booktitle = {Logic, Language, Information, and Computation - 25th International
               Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018, Proceedings},
  pages     = {179--195},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-662-57669-4\_10},
  doi       = {10.1007/978-3-662-57669-4\_10},
  timestamp = {Wed, 14 Nov 2018 10:55:35 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/wollic/CiobacaAL18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
		    



• Ștefan Ciobâcă, Dorel Lucanu: A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems (IJCAR 2018; extended technical report). Abstract and BibTeX
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-sorted signature modulo builtins. A key feature of the calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proofs.

@inproceedings{DBLP:conf/cade/CiobacaL18,
  author    = {\c{S}tefan Ciob\^ac\u{a} and
               Dorel Lucanu},
  title     = {A Coinductive Approach to Proving Reachability Properties in Logically
               Constrained Term Rewriting Systems},
  booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
               2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
               UK, July 14-17, 2018, Proceedings},
  pages     = {295--311},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-94205-6\_20},
  doi       = {10.1007/978-3-319-94205-6\_20},
  timestamp = {Mon, 09 Jul 2018 13:01:56 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/CiobacaL18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}		    



• Andrei Arusoaie, Ștefan Ciobâcă, Vlad Crăciun, Dragoș Gavriluț, Dorel Lucanu: A Comparison of Open-Source Static Analysis Tools for Vulnerability Detection in C/C++ Code . Postproceedings SYNASC 2017. PDF Abstract and BibTeX
We describe work that is part of a research project on static code analysis between the Alexandru Ioan Cuza University and Bitdefender. The goal of the project is to develop customized static analysis tools for detecting potential vulnerabilities in C/C++ code. We present the results of benchmarking several existing open source static analysis tools for C/C++ against the Toyota ITC test suite [1] in order to determine which tools are best suited to our purpose. The Toyota ITC test suite is a synthetic benchmark for C/C++ consisting of around 650 test cases organized by defect type and defect subtype and is well-suited to our purpose, since it contains various bugs such as buffer overflows that are common in C/C++ code. We analyze the open-source static analysis tools according to the existing quality indicators such as detection rate and false positive rate proposed in [1], but we also introduce a new quality metric that we call robust detection which also allows us to measure unique detections by tool and by (sub)defect type. We also find several mistakes in the Toyota ITC testsuite that we fix. We publish the harness used to benchmark the static analyzers in order for anyone to be able to reproduce our results.

@inproceedings{DBLP:conf/synasc/ArusoaieCCGL17,
  author    = {Andrei Arusoaie and
               \c{S}tefan Ciob\^ac\u{a} and
               Vlad Craciun and
               Dragos Gavrilut and
               Dorel Lucanu},
  title     = {A Comparison of Open-Source Static Analysis Tools for Vulnerability
               Detection in {C/C++} Code},
  booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for
               Scientific Computing, {SYNASC} 2017, Timisoara, Romania, September
               21-24, 2017},
  pages     = {161--168},
  year      = {2017},
  url       = {https://doi.org/10.1109/SYNASC.2017.00035},
  doi       = {10.1109/SYNASC.2017.00035},
  timestamp = {Thu, 14 Feb 2019 16:15:01 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/synasc/ArusoaieCCGL17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}		    

• 

  Rohit Chadha, Vincent Cheval, Ștefan Ciobâcă, Steve Kremer:Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Transactions on Computational Logic, 2016. (PDF - technical report | ACM Digital Library) Abstract and BibTeX

Abstract: Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties. We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryp- tographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples. The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effec- tively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.

@article{Chadha:2016:AVE:2996393.2926715,
author = {Chadha, Rohit and Cheval, Vincent and Ciob\^{a}c\u{a}, \c{S}tefan and Kremer, Steve},
title = {Automated Verification of Equivalence Properties of Cryptographic Protocols},
journal = {ACM Trans. Comput. Logic},
issue_date = {November 2016},
volume = {17},
number = {4},
month = sep,
year = {2016},
issn = {1529-3785},
pages = {23:1--23:32},
articleno = {23},
numpages = {32},
url = {http://doi.acm.org/10.1145/2926715},
doi = {10.1145/2926715},
acmid = {2926715},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {Applied pi calculus, automated verification, process equivalence, security protocols},
}
		    



• Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A Language-Independent Proof System for Full Program Equivalence. Formal Aspects of Computing, 2016. (SpringerLink) Abstract and BibTeX
Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in determin- istic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known weather the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).

	      @Article{CLRRFAOC2016,
	      author="Ciob{\^a}c{\u{a}}, {\c{S}}tefan
	      and Lucanu, Dorel
	      and Rusu, Vlad
	      and Ro{\c{s}}u, Grigore",
	      title="A language-independent proof system for full program equivalence",
	      journal="Formal Aspects of Computing",
	      year="2016",
	      month="May",
	      day="01",
	      volume="28",
	      number="3",
	      pages="469--497",
	      issn="1433-299X",
	      doi="10.1007/s00165-016-0361-7",
	      url="https://doi.org/10.1007/s00165-016-0361-7"
	      }
		    



• Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A Theoretical Foundation for Programming Languages Aggregation. WADT 2014 post-proceedings, LNCS 9463, 2015. (SpringerLink) Abstract and BibTeX
Abstract: Programming languages should be formally specified in order to reason about programs written in them. We show that, given two formally specified programming languages, it is possible to construct the formal semantics of an aggregated language, in which programs consist of pairs of programs from the initial languages. The construction is based on algebraic techniques and it can be used to reduce relational properties (such as equivalence of programs) to reachability properties (in the aggregated language).

	      @Inbook{CLRRWADT2014,
	      author="Ciob{\^a}c{\u{a}}, {\c{S}}tefan
	      and Lucanu, Dorel
	      and Rusu, Vlad
	      and Ro{\c{s}}u, Grigore",
	      editor="Codescu, Mihai
	      and Diaconescu, R{\u{a}}zvan
	      and Țuțu, Ionuț",
	      title="A Theoretical Foundation for Programming Languages Aggregation",
	      bookTitle="Recent Trends in Algebraic Development Techniques: 22nd International Workshop, WADT 2014, Sinaia, Romania, September 4-7, 2014, Revised Selected Papers",
	      year="2015",
	      publisher="Springer International Publishing",
	      address="Cham",
	      pages="30--47",
	      isbn="978-3-319-28114-8",
	      doi="10.1007/978-3-319-28114-8_3",
	      url="https://doi.org/10.1007/978-3-319-28114-8_3"
	      }
		    



• Ștefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roșu, A Language-Independent Proof System for Mutual Program Equivalence. ICFEM 2014. Abstract and BibTeX
Abstract: Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in determin- istic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known weather the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).

	      @inproceedings{CLRRICFEM2014,
	      author = "Ciobaca, Stefan and Lucanu, Dorel and Rusu, Vlad and Rosu, Grigore",
	      publisher = "Springer",
	      doi = "http://dx.doi.org/10.1007/978-3-319-11737-9_6",
	      title = "A Language-Independent Proof System for Mutual Program Equivalence",
	      series = "LNCS",
	      booktitle = "Proceedings of the 16th International Conference on Formal Engineering Methods (ICFEM'14)",
	      month = "November",
	      volume = "8829",
	      year = "2014",
	      pages = "75-90"
	      }
		    



• Andrei Ștefănescu, Ștefan Ciobâcă, Radu Mereuță, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Roșu, All-Path Reachability Logic, RTA-TLCA 2014.


• Ștefan Ciobâcă, Reducing Partial Equivalence to Partial Correctness. SYNASC 2014.


• Ștefan Ciobâcă, From Small-Step Semantics to Big-Step Semantics, Automatically, IFM 2013.


• Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobâcă and Brandon M. Moore, One-Path Reachability Logic, LICS 2013.


• Grigore Roșu, Andrei Ștefănescu, Ștefan Ciobâcă and Brandon M. Moore, Reachability Logic, Technical Report, July 2012. PDF


• Ștefan Ciobâcă, From Small-step Semantics to Big-step Semantics, Automatically, Summer School on Language Frameworks 2012, SSLF 2012, Sinaia, Romania.


• Rohit Chadha, Ștefan Ciobâcă, Steve Kremer, Automated Verification of Equivalence Properties of Cryptographic Protocols. ESOP 2012: 108-127 PDF

More publications are available on my DBLP profile.

Here are some recent BSc/MSc theses that I have supervized:

• (February, 2025) Alina-Adriana Haidău: Verifying an algorithm for the discrete version of the knapsack problem in Dafny (in Romanian)


• (July, 2024) Roxana Mihaela Timon: Verifying an algorithm for the weighted activity selection problem in Dafny (in Romanian)


• (July, 2024) Daniel-Antoniu Dumitru: Implementing and Verifying the Boyer-Moore-Horspool Algorithm in F* (in English)


• (June-July, 2023) Alexandru Donica: Verifying the DPLL algorithm F* (in Romanian)


• (June-July, 2023) Bianca-Maria Buzilă: Computing CNFs in F*. Implementation and verification (in Romanian)


• (February, 2023) Alexandra Elena Contur: Implementing and formally verifying in Dafny the greedy algorithm for a version of the coin change problem (in Romanian)


• (June-July, 2022) Viorel Iordache: Comparison between formal verification tools (in English)


• (June-July, 2022) Mihnea-Ștefan Sidorencu: The rod cutting problem in Dafny (in Romanian)


• (June-July, 2022) Radu Plăcintă: Verifying an algorithm for solving the Sudoku problem using the Dafny language (in Romanian)


• (June-July, 2022) Veronica Elisa Chicoș: Implementing a greedy algorithm for the coin change problem in Dafny (in Romanian)


• (June, 2021) Cristi-Constantin Rusu: Applying a greedy algorithm to solve the activity selection problem - a study on its correctness and completeness using Dafny (in Romanian)


• (July, 2021) Cezar-Constantin Andrici: Secure F*-ML interoperability for IO programs (in English)


• (July, 2020) Viorel Iordache: Verifying some transformation in propositional logic using Dafny (in Romanian)


• (July, 2020) Valeriu Motroi: Unification Library (in English)


• (July, 2019) Cezar-Constantin Andrici: Proving SAT Solving Algorithms and Data Structures in Dafny (in English)


• (July, 2019) Andrei-Sebastian Buruiană: Program Equivalence Proofs using LCTRSs (in English)

I defended my PhD thesis on the security of cryptographic protocols at ENS Cachan on December 9th, 2011.

For my PhD thesis, I worked on a few tools for the verification of security protocols, the most important being AKiSs, a tool for verifying equivalence properties of cryptographic protocols.

I have also contributed to the K Tool, a framework for giving executable semantics to programming languages.