5 Search Results for "Conchon, Sylvain"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.34
New Fault Domains for Conformance Testing of Finite State Machines

Authors: Frits Vaandrager and Ivo Melse

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
A fault domain reflects a tester’s assumptions about faults that may occur in an implementation and that need to be detected during testing. A fault domain that has been widely studied in the literature on black-box conformance testing is the class of finite state machines (FSMs) with at most m states. Numerous strategies for generating test suites have been proposed that guarantee fault coverage for this class. These so-called m-complete test suites grow exponentially in m-n, where n is the number of states of the specification, so one can only run them for small values of m-n. But the assumption that m-n is small is not realistic in practice. In his seminal paper from 1964, Hennie raised the challenge to design checking experiments in which the number of states may increase appreciably. In order to solve this long-standing open problem, we propose (much larger) fault domains that capture the assumption that all states in an implementation can be reached by first performing a sequence from some set A (typically a state cover for the specification), followed by k arbitrary inputs, for some small k. The number of states of FSMs in these fault domains grows exponentially in k. We present a sufficient condition for k-A-completeness of test suites with respect to these fault domains. Our condition implies k-A-completeness of two prominent m-complete test suite generation strategies, the Wp and HSI methods. Thus these strategies are complete for much larger fault domains than those for which they were originally designed, and thereby solve Hennie’s challenge. We show that three other prominent m-complete methods (H, SPY and SPYH) do not always generate k-A-complete test suites.
Cite as

Frits Vaandrager and Ivo Melse. New Fault Domains for Conformance Testing of Finite State Machines. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vaandrager_et_al:LIPIcs.CONCUR.2025.34,
  author =	{Vaandrager, Frits and Melse, Ivo},
  title =	{{New Fault Domains for Conformance Testing of Finite State Machines}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{34:1--34:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.34},
  URN =		{urn:nbn:de:0030-drops-239843},
  doi =		{10.4230/LIPIcs.CONCUR.2025.34},
  annote =	{Keywords: conformance testing, finite state machines, Mealy machines, apartness, observation tree, fault domains, k-A-complete test suites}
}
Document
Experience Paper
DOI: 10.4230/LIPIcs.ECOOP.2025.37
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)

Authors: Tomáš Dacík and Tomáš Vojnar

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.
Cite as

Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dacik_et_al:LIPIcs.ECOOP.2025.37,
  author =	{Dac{\'\i}k, Tom\'{a}\v{s} and Vojnar, Tom\'{a}\v{s}},
  title =	{{RacerF: Lightweight Static Data Race Detection for C Code}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{37:1--37:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.37},
  URN =		{urn:nbn:de:0030-drops-233298},
  doi =		{10.4230/LIPIcs.ECOOP.2025.37},
  annote =	{Keywords: concurrency, data race detection, static analysis}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:34},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  URN =		{urn:nbn:de:0030-drops-192965},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
Invited Talk
DOI: 10.4230/OASIcs.FAB.2022.2
Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos (Invited Talk)

Authors: Sylvain Conchon

Published in: OASIcs, Volume 101, 5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022)

Abstract
Blockchain is an emerging field that started with the advent of Bitcoin, the first cryptocurrency launched in 2008. Since then, new distributed applications (DApps) based on blockchain have emerged, such as non-fungible tokens (NFT) or decentralized finance (DeFi). All this contributes to an ever-increasing use of blockchains and poses many technological and scientific challenges. The first challenge is related to scalability, usually measured by the number of transactions per second (TPS) that a blockchain can process. Recent solutions, such as Rollups, implement the concept of Layer 2, a secondary framework built on top of an existing blockchain that allows transactions to be managed off-chain for efficiency. The primary blockchain is used to secure the exchanges of the second layer by regularly recording its exchanges and its current state. A first experiment of Optimistic Rollups has been implemented in the Blockchain Tezos. The TORUs (Transaction Optimistic Rollups) allow efficient financial assets exchanges in the form of Michelson tickets. A generalization to Smart contracts Optimistic Rollups (SCORU) is currently under development. Another challenge is to improve the efficiency of the data structures used in blockchain implementations. The main explorative tracks are to reduce and improve disk usage (compact representations, serialization of big data, sharing, ...), increase the speed of access operations (efficient caching strategies, asynchronous I/O, ...). For example, recent improvements to the storage layer of Octez, Tezos' most popular node implementation, have shown that it is possible to significantly speed up transactions, stabilize average transaction latency, and significantly reduce memory usage. The security issues associated with blockchains also raise many challenges. Indeed, the economic protocols or consensus algorithms implemented in blockchains use incentive mechanisms to discourage nodes from engaging in bad behavior or in launching attacks. A fine tuning of these incentives is difficult in situations where decision makers interact. Game theory can be used to develop incentives, in particular its integration into verification tools (model-checkers, proof assistants, deductive program verification) or machine-learning tools could be very promising. Finally, given the financial amounts managed by blockchains, it is essential to have a very precise specification of the algorithms, protocols and data structures used in blockchain implementations in order to guarantee the reliability of these very complex software. Whether it is for the programming of smart contracts, consensus algorithms or the P2P layer, the introduction of formal methods in the development cycle of blockchains is a major challenge in this domain. A lot of work in formal methods has been done for the Tezos blockchain. Among others, the formalization in TLA+ of Tenderbake, a PBFT-style consensus algorithm which offers deterministic finality to Tezos. Author Bio. Sylvain Conchon is Professor in Computer Science at University Paris-Saclay since 2013. He is a member of LMF (Formal Methods Laboratory) and his research focuses on automatic deduction and model-checking, using techniques based on SMT (Satisfiabilty Modulo Theories) solvers. He is one of the designers of the SMT solver Alt-Ergo and the model-checker Cubicle. In collaboration with Nomadic-Labs, he is currently working on the use of formal methods to design and verify several aspects related to the blockchain Tezos, such as Michelson smart contracts or the Tenderbake consensus algorithm.
Cite as

Sylvain Conchon. Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos (Invited Talk). In 5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022). Open Access Series in Informatics (OASIcs), Volume 101, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{conchon:OASIcs.FAB.2022.2,
  author =	{Conchon, Sylvain},
  title =	{{Some Insights on Open Problems in Blockchains: Explorative Tracks for Tezos}},
  booktitle =	{5th International Symposium on Foundations and Applications of Blockchain 2022 (FAB 2022)},
  pages =	{2:1--2:1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-248-8},
  ISSN =	{2190-6807},
  year =	{2022},
  volume =	{101},
  editor =	{Tucci-Piergiovanni, Sara and Crooks, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FAB.2022.2},
  URN =		{urn:nbn:de:0030-drops-162696},
  doi =		{10.4230/OASIcs.FAB.2022.2},
  annote =	{Keywords: Blockchain, Tezos, Scalability, Efficiency, Security, Reliability}
}
Document
Short Paper
DOI: 10.4230/OASIcs.FMBC.2021.4
Formally Documenting Tenderbake (Short Paper)

Authors: Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

Abstract
In this paper, we propose a formal documentation of Tenderbake, the new Tezos consensus algorithm, slated to replace the current Emmy family algorithms. The algorithm is broken down to its essentials and represented as an automaton. The automaton models the various aspects of the algorithm: (i) the individual participant, referred to as a baker, (ii) how bakers communicate over the network (the mempool) and (iii) the overall network the bakers operate in. We also present a TLA+ implementation, which has proven to be useful for reasoning about this automaton and refining our documentation. The main goal of this work is to serve as a formal foundation for extracting intricate test scenarios and verifying invariants that Tenderbake’s implementation should satisfy.
Cite as

Sylvain Conchon, Alexandrina Korneva, Çagdas Bozman, Mohamed Iguernlala, and Alain Mebsout. Formally Documenting Tenderbake (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{conchon_et_al:OASIcs.FMBC.2021.4,
  author =	{Conchon, Sylvain and Korneva, Alexandrina and Bozman, \c{C}agdas and Iguernlala, Mohamed and Mebsout, Alain},
  title =	{{Formally Documenting Tenderbake}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{4:1--4:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.4},
  URN =		{urn:nbn:de:0030-drops-154281},
  doi =		{10.4230/OASIcs.FMBC.2021.4},
  annote =	{Keywords: Consensus algorithm, Tezos blockchain, TLA+}
}
  • Refine by Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 2 2022
  • 1 2021

  • Refine by Author
  • 2 Conchon, Sylvain
  • 1 Bozman, Çagdas
  • 1 Dacík, Tomáš
  • 1 Hähnle, Reiner
  • 1 Iguernlala, Mohamed
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 2 OASIcs
  • 1 LITES

  • Refine by Classification
  • 1 Computing methodologies → Distributed programming languages
  • 1 Computing methodologies → Model verification and validation
  • 1 Software and its engineering
  • 1 Software and its engineering → Automated static analysis
  • 1 Software and its engineering → Formal methods
  • Show More...

  • Refine by Keyword
  • 1 Active Objects
  • 1 Blockchain
  • 1 Consensus algorithm
  • 1 Differential Dynamic Logic
  • 1 Efficiency
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact