
@inproceedings{altisen_pour_etre_cesar_2024_hal-04552810,
	title = {Pour être César, il faut que tous les chemins viennent de la Domus Augustana},
	booktitle = {AlgoTel 2024 – 26èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications},
	abstract = {Nous considérons des réseaux dirigés où chaque processus est identifié et connait une borne supérieure sur l’écart maximum des processus à leur descendants. Dans ce type de réseaux, nous étudions les conditions topologiques nécessaires et suffisantes pour résoudre de manière autostabilisante deux problèmes fondamentaux : l’élection de leader et l’unisson synchrone. Cette condition contraint le réseau à n’avoir qu’une seule composante source (c’est-à-dire, une composante fortement connexe où aucun nœud n’a de prédécesseur hors de la composante). Pour démontrer que notre condition est suffisante pour les deux problèmes cités, nous proposons deux algorithmes autostabilisants, dont nous étudions également la complexité.},
	author = {Altisen, K. and  Cournier, A. and  Defalque, G. and  Devismes, S.},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04552810},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{aubouin--pairault_pid_and_model_2024_hal-04565817,
	title = {PID and Model Predictive Control Approach for Drug Dosage in Anesthesia During Induction: a Comparative Study},
	volume = {58},
	booktitle = {PID24 - 4th IFAC Conference on Advances in Proportional-Integral-Derivative Control},
	doi = {10.1016/j.ifacol.2024.08.036},
	abstract = {In this paper, a PID controller is compared to an extended moving horizon estimator coupled with a model predictive control approach for the problem of dosing propofol and remifentanil during the induction of anesthesia. For the PID controller, taken from the literature, a fixed ratio is considered between propofol and remifentanil flow rates and an anti-windup strategy is used to prevent integration wind-up. The optimal control approach uses an MHE to estimate both the states and the pharmacodynamic parameters of the system, followed by a non-linear model predictive controller to compute the optimal drug rates according to the model. Both controllers are tuned using the same criterion, and are compared by simulating 500 uncertain patient models for the induction phase.},
	author = {Aubouin--Pairault, B. and  Fiacchini, M. and  Dang, T.},
	pages = {210-215},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04565817},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{chimes_treeverifiable_graph_grammars_2024_hal-04763023,
	title = {Tree-Verifiable Graph Grammars},
	booktitle = {Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning},
	doi = {10.29007/8l13},
	abstract = {Hyperedge-Replacement grammars (HR) have been introduced by Courcelle in order to extend the notion of context-free sets from words and trees to graphs of bounded tree-width. While for words and trees the syntactic restrictions that guarantee that the associated languages of words resp. trees are regular - and hence, MSO-definable - are known, the situation is far more complicated for graphs. Here, Courcelle proposed the notion of regular graph grammars, a syntactic restriction of HR grammars that guarantees the definability of the associated languages of graphs in Counting Monadic Second Order Logic (CMSO). However, these grammars are not complete in the sense that not every CMSO-definable set of graphs of bounded tree-width can be generated by a regular graph grammar. In this paper, we introduce a new syntactic restriction of HR grammars, called tree-verifiable graph grammars, and a new notion of bounded tree-width, called embeddable bounded tree-width, where the later restricts the trees of a tree-decomposition to be a subgraph of the analyzed graph. The main property of tree-verifiable graph grammars is that their associated languages are CMSO-definable and that they have bounded embeddable tree-width. We show further that they strictly generalize the regular graph grammars of Courcelle. Finally, we establish a completeness result, showing that every language of graphs that is CMSO-definable and of bounded embeddable tree-width can be generated by a tree-verifiable graph grammar.},
	author = {Chimes, M. and  Iosif, R. and  Zuleger, F.},
	pages = {165-148},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04763023},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{de_goër_informatique_et_durabilite_2024_hal-04482133,
	title = {Informatique et durabilité, une difficile transposition didactique},
	editor= {Mens, Kim and Goletti, Olivier},
	booktitle = {DidaSTIC 2024 - Colloque Didapro 10 sur la Didactique de l’informatique et des STIC},
	abstract = {Dans le contexte actuel de changement climatique, une demande forte d'enseigner à l'école les enjeux de durabilité liés au numérique émerge dans la société et en provenance des institutions. Or, la transposition didactique de ces sujets dans les cours d'informatique soulève un certain nombre de difficultés. Ce papier présente dans un premier temps un aperçu des savoirs scientifiques sur le sujet, des pratiques académiques associées et met en avant la difficile articulation entre l'informatique comme discipline scientifique et les questions de durabilité. Dans un second temps, inspirés de réflexions issues de l'éthique de la technologie, nous évoquons la possibilité de réancrer l'informatique dans le contexte matériel, économique, social et politique de son développement et de ses applications, ce qui constituerait une évolution importante de l'informatique aussi bien au niveau scolaire qu'académique.},
	author = {De goër, B. and  Micha, H. and  Quinton, S.},
	pages = {23-32},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04482133},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{monniaux_memory_simulations_security_2024_hal-04336347,
	title = {Memory Simulations, Security and Optimization in a Verified Compiler},
	editor= {Brigitte Pientka and Sandrine Blazy},
	booktitle = {Certified Programs and Proofs 2024},
	url = {https://popl24.sigplan.org/home/CPP-2024},
	doi = {10.1145/3636501.3636952},
	abstract = {Current compilers implement security features and optimizations that require nontrivial semantic reasoning about pointers and memory allocation: the program after the insertion of the security feature, or after applying the optimization, must simulate the original program despite a different memory layout. In this article, we illustrate such reasoning on pointer allocations through memory extensions and injections, as well as fine points on undefined values, by explaining how we implemented and proved correct two security features (stack canaries and pointer authentication) and one optimization (tail recursion elimination) in the CompCert formally verified compiler.},
	author = {Monniaux, D.},
	publisher = {Association for computing machinery (ACM)},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04336347},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{oulkaid_a_transistor_level_2024_hal-04527225,
	title = {A Transistor Level Relational Semantics for Electrical Rule Checking by SMT Solving},
	booktitle = {Design, Automation and Test in Europe Conference},
	doi = {10.23919/DATE58400.2024.10546537},
	abstract = {We present a novel technique for Electrical Rule Checking (ERC) based on formal methods. We define a relational semantics of Integrated Circuits (IC) as a means to model circuits’ behavior at transistor-level. We use Z3, a Satisfiability Modulo Theory (SMT) solver, to verify electrical properties on circuits — thanks to the defined semantics. We demonstrate the usability of the approach to detect current leakage due to missing level-shifter on large industrial circuits, and we conduct experiments to study the scalability of the approach.},
	author = {Oulkaid, O. and  Ferres, B. and  Moy, M. and  Raymond, P. and  Khosravian, M. and  Henrio, L. and  Radanne, G.},
	pages = {1-6},
	publisher = {IEEE},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04527225},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{vigouroux_function_synthesis_for maximizing_2024_hal-04578258,
	title = {Function Synthesis for Maximizing Model Counting},
	volume = {14499},
	editor= {Rayna Dimitrova and Ori Lahav and Sebastian Wolff},
	series = {Verification, Model Checking, and Abstract Interpretation 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part I},
	booktitle = {25th International  Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024)},
	doi = {10.1007/978-3-031-50524-9_12},
	abstract = {Given a boolean formula ϕ(X, Y,Z), the Max\#SAT problem asks for finding a partial model on the set of variables X, maximizing its number of projected models over the set of variables Y. We investigate a strict generalization of Max\#SAT allowing dependencies for variables in X, effectively turning it into a synthesis problem. We show that this new problem, called DQMax\#SAT, subsumes both the DQBF and DSSAT problems. We provide a general resolution method, based on a reduction to Max\#SAT, together with two improvements for dealing with its inherent complexity. We further discuss a concrete application of DQMax\#SAT for symbolic synthesis of adaptive attackers in the field of program security. Finally, we report preliminary results obtained on the resolution of benchmark problems using a prototype DQMax\#SAT solver implementation.},
	author = {Vigouroux, T. and  Bozga, M. and  Ene, C. and  Mounier, L.},
	pages = {258-279},
	publisher = {Springer Nature Switzerland},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04578258},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{adimoolam_safe_selftriggered_control_2023_hal-04295861,
	title = {Safe Self-Triggered Control Based on Precomputed Reachability Sequences},
	booktitle = {Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control},
	doi = {10.1145/3575870.3587124},
	abstract = {Self-triggered controllers have the potential to improve the stateof-the-art of Cyber-Physical Systems (CPSs) by enhancing the performance of the underlying closed-loop control systems. However, a major concern in deploying a self-triggered controller in a safetycritical CPS is that the stabilizing self-triggered controller may not always guarantee the satisfaction of the safety constraints. We propose a self-triggered control scheme that deals with the safe scheduling of control tasks for uncertain continuous-time linear systems. We derive a computationally efficient scheduling function that computes an upper bound on the next sampling period as a function of the current state in the presence of additive disturbance. To reduce the computational complexity of online reachability analysis and increase accuracy, we compute a large sequence of reachable sets offline and use these precomputed sets to derive a low-complexity online scheduling function that computes sufficiently large bounds in real time. We evaluate our algorithm on three high-dimensional benchmark control systems, where two of the examples have a twelve-dimensional joint state plus feedback input. Experimental results demonstrate that our self-triggered control algorithm guarantees the safety of the closed-loop control system through negligible online computation, establishing the feasibility of its practical implementation.},
	author = {Adimoolam, A. and  Dang, T. and  Saha, I.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04295861},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	HAL_version = {v1},
}

@inproceedings{al-qadasi_deepabstraction_enhancing_test_2023_hal-04380870,
	title = {DeepAbstraction++: Enhancing Test Prioritization Performance via Combined Parameterized Boxes},
	booktitle = {AISOLA 2023 - Bridging the Gap Between AI and Reality},
	abstract = {In artificial intelligence testing, there is an increased focus on enhancing the efficiency of test prioritization methods within deep learning systems. Subsequently, the DeepAbstraction algorithm has recently become one of the leading techniques in this area. It employs a box-abstraction concept, the efficiency of which depends on the tau parameter, the clustering parameter, that influences the size of these boxes. The conclusion of the previous experiments using tau values of 0.4 or 0.05 has failed to produce optimal results among all experiments. This highlights a significant challenge in the DeepAbstraction framework concerning the appropriate selection of the tau parameter. The selection of the tau value is extremely crucial, given its decisive effect on box size and, subsequently, the stability and efficacy of the framework. Addressing this challenge, we propose a methodology called combined parameterized boxes. This approach leverages the collective verdicts of monitors with various tau values to evaluate network predictions. We assign appropriate weights to these verdicts to ensure that no single verdict influences the decision-making process, thereby ensuring balance. Furthermore, we propose multiple strategies for integrating the weighted verdicts of monitors into a conclusive verdict, such as mean, max, product, and mode. The results of our investigation demonstrate that our approach can notably boost the DeepAbstraction framework's performance. Compared to the leading algorithms, DeepAbstraction++ consistently outperforms its competitors, delivering an increase in performance between 2.38\% and 7.71\%. Additionally, Deep-Abstraction++ brings remarkable stability to the process, addressing a significant shortcoming of the earlier version of DeepAbstraction.},
	author = {Al-Qadasi, H. and  Falcone, Y. and  Bensalem, S.},
	pages = {1-15},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04380870},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {1},
	HAL_version = {v1},
}

@inproceedings{al-qadasi_difficulty_and_severityoriented_2023_hal-04196591,
	title = {Difficulty and Severity-Oriented Metrics for Test Prioritization in Deep Learning Systems},
	booktitle = {5th IEEE International Conference on Artificial Intelligence (AITest 2023)},
	doi = {10.1109/AITest58265.2023.00015},
	abstract = {Recently, there has been a growing trend in AI testing toward developing new test prioritization algorithms for deep learning systems. These algorithms aim to reduce the cost and time needed to annotate test datasets by prioritizing instances with a higher chance of exposing faults. Various metrics have been used to evaluate the effectiveness of these algorithms, e.g., APFD, RAUC, and ATRC. However, there is a lack of research to confirm their validity. The results indicate that the existing metrics have severe limitations. For example, some metrics ignore the labeling budget and prioritize the fault detection rate instead of the fault detection ratio. Moreover, others overlook the prioritization difficulty in the evaluation. As a solution, we develop a new metric (WFDR), which solves the deficiencies of previous metrics. We also draw attention to a new research area, known as severity prioritization, which emphasizes the importance of prioritizing misclassified instances according to the severity level, particularly in critical situations. Our experiments reveal that instances with high severity make up more than 20\% of all misclassified instances. Thus, these instances should be prioritized when it comes to labeling. Consequently, we proposed a new metric known as (SFDR) that evaluates the effectiveness of algorithms in prioritizing high-severity instances. Our evaluations show that our proposed metrics are more effective than other existing metrics. Besides, our two metrics re-evaluate some recent algorithms and indicate that these algorithms perform poorly.},
	author = {Al-Qadasi, H. and  Falcone, Y. and  Bensalem, S.},
	pages = {40-48},
	publisher = {IEEE},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04196591},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{altisen_pour_battre_a_2023_hal-04076915,
	title = {Pour battre à l'unisson, il faut que tous les chemins viennent de Rome},
	booktitle = {AlgoTel 2023 - 25èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications},
	abstract = {La littérature portant sur l'autostabilisation dans les réseaux dirigés est nettement moins fournie que celle sur les réseaux non-dirigés. C'est encore plus vrai lorsque l'on se restreint aux problèmes dynamiques où, à notre connaissance, seules les topologies en anneau unidirectionnel ont été considérées. Notre but ici est d'étudier les conditions sous lesquelles un algorithme peut résoudre de manière autostabilisante un problème dynamique simple : l'unisson synchrone.},
	author = {Altisen, K. and  Cournier, A. and  Defalque, G. and  Devismes, S.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04076915},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{altmeyer_from_fmtv_to_2023_hal-04654624,
	title = {From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Invited Paper)},
	volume = {262},
	editor= {Alessandro V. Papadopoulos},
	series = {35th Euromicro Conference on Real-Time Systems (ECRTS 2023)},
	booktitle = {35th Euromicro Conference on Real-Time Systems (ECRTS 2023)},
	url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2023.19},
	doi = {10.4230/LIPIcs.ECRTS.2023.19},
	abstract = {We present here the main features and lessons learned from the first edition of what has now become the ECRTS industrial challenge, together with the final description of the challenge and a comparative overview of the proposed solutions. This verification challenge, proposed by Thales, was first discussed in 2014 as part of a dedicated workshop (FMTV, a satellite event of the FM 2014 conference), and solutions were discussed for the first time at the WATERS 2015 workshop. The use case for the verification challenge is an aerial video tracking system. A specificity of this system lies in the fact that periods are constant but known with a limited precision only. The first part of the challenge focuses on the video frame processing system. It consists in computing maximum values of the end-to-end latency of the frames sent by the camera to the display, for two different buffer sizes, and then the minimum duration between two consecutive frame losses. The second challenge is about computing end-to-end latencies on the tracking and camera control for two different values of jitter. Solutions based on five different tools - Fiacre/Tina, CPAL (simulation and analysis), IMITATOR, UPPAAL and MAST - were submitted for discussion at WATERS 2015. While none of these solutions provided a full answer to the challenge, a combination of several of them did allow to draw some conclusions.},
	author = {Altmeyer, S. and  André, É. and  Dal zilio, S. and  Fejoz, L. and  Harbour, M. G. and  Graf, S. and  Gutiérrez, J. J. and  Henia, R. and  Le botlan, D. and  Lipari, G. and  Medina, J. and  Navet, N. and  Quinton, S. and  Rivas, J. and  Sun, Y.},
	publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04654624},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {1},
	HAL_version = {v1},
}

@inproceedings{aubouin--pairault_databased_pharmacodynamic_modeling_2023_hal-04066401,
	title = {Data-based Pharmacodynamic Modeling for BIS and Mean Arterial Pressure Prediction during General Anesthesia},
	booktitle = {ECC 2023 - 21st European Control Conference},
	url = {https://ecc23.euca-ecc.org/},
	doi = {10.23919/ECC57647.2023.10178214},
	abstract = {In this paper, a data-based approach is used to predict the effect of Propofol and Remifentanil on Bispectral Index (BIS) and Mean Arterial Pressure (MAP) during total intravenous anesthesia. In particular, we aim to reproduce the measured data by identifying the pharmacodynamic function using machine-learning techniques. Features from the output of classic pharmacokinetic models and patient information are considered. Five learning methods are tested including linear models, support vector machine, Kernel, k-neighbors regressors, and neural-network. Learning and testing are performed on a particular subset of 150 surgery cases extracted from the VitalDB database. Results show that this approach improves the classic surface-response methods for BIS and MAP prediction and can be used for anesthesia control applications.},
	author = {Aubouin--Pairault, B. and  Fiacchini, M. and  Dang, T.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04066401},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{barbot_maxentropy_sampling_for deterministic_2023_hal-04239175,
	title = {Max-Entropy Sampling for Deterministic Timed Automata Under Linear Duration Constraints},
	volume = {14287},
	series = {Lecture Notes in Computer Science},
	booktitle = {Qest23},
	doi = {10.1007/978-3-031-43835-6_14},
	abstract = {Adding probabilities to timed automata enables one to carry random simulation of their behaviors and provide answers with statistical guarantees to problems otherwise untractable. Thus, when just a timed language is given, the following natural question arises: What probability should we consider if we have no a priori knowledge except the given language and the considered length (i.e. number of events) of timed words? The maximal entropy principle tells us to take the probability measure that maximises the entropy which is the uniform measure on the language restricted to timed word of the given length (with such a uniform measure every timed word has the same chance of being sampled). The uniform sampling method developed in the last decade provides no control on the duration of sampled timed words. In the present article we consider the problem of finding a probability measure on a timed language maximising the entropy under general linear constraints on duration and for timed words of a given length. The solution we provide generalizes to timed languages a well-known result on probability measure over the real line maximising the Shannon continuous entropy under linear constraints. After giving our general theorem for general linear constraints and for general timed languages, we concentrate to the case when only the mean duration is prescribed (and again when the length is fixed) for timed languages recognised by deterministic timed automata. For this latter case, we provide an efficient sampling algorithm we have implemented and illustrated on several examples.},
	author = {Barbot, B. and  Basset, N.},
	pages = {188-204},
	publisher = {Springer Nature Switzerland},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04239175},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{barbot_wordgen__a_2023_hal-04127298,
	title = {Wordgen : a Timed word Generation Tool},
	booktitle = {HSCC '23: 26th ACM International Conference on Hybrid Systems: Computation and Control},
	doi = {10.1145/3575870.3587116},
	abstract = {Sampling timed words out of a timed language described as a timed automaton may seem a simple task: start from the initial state, choose a transition and a delay and repeat until an accepting state is reached. Unfortunately, simple approach based on local, on-the-fly rules produces timed words from distributions that are biased in some unpredictable ways. For this reason, approaches have been developed to guarantee that the sampling follows a more desirable distribution defined over the timed language and not over the automaton. One such distribution is the maximal entropy distribution, whose implementation requires several non-trivial computational steps. In this paper, we present Wordgen which combines those different necessary steps into a lightweight standalone tool. The resulting timed words can be mapped to signals used for model-based testing and falsification of cyber-physical systems thanks to a simple interface with the Breach tool.},
	author = {Barbot, B. and  Basset, N. and  Donze, A.},
	pages = {1-7},
	publisher = {ACM},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04127298},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{bardin_adversarial_reachability_for_2023_cea-04199882,
	title = {Adversarial reachability for program-level security analysis},
	volume = {13990},
	editor= {ETAPS},
	series = {Programming Languages and Systems - proceedings of the 32nd European Symposium on Programming},
	booktitle = {ESOP 2023 - 32nd European Symposium on Programming,},
	url = {https://link.springer.com/chapter/10.1007/978-3-031-30044-8_3},
	doi = {10.1007/978-3-031-30044-8_3},
	abstract = {Many program analysis tools and techniques have been developed to assess program vulnerability. Yet, they are based on the standard concept of reachability and represent an attacker able to craft smart legitimate input, while in practice attackers can be much more powerful, using for instance micro-architectural exploits or fault injection methods. We introduce adversarial reachability, a framework allowing to reason about such advanced attackers and check whether a system is vulnerable or immune to a particular attacker. As equipping the attacker with new capacities significantly increases the state space of the program under analysis, we present a new symbolic exploration algorithm, namely adversarial symbolic execution, injecting faults in a forkless manner to prevent path explosion, together with optimizations dedicated to reduce the number of injections to consider while keeping the same attacker power. Experiments on representative benchmarks from fault injection show that our method significantly reduces the number of adversarial paths to explore, allowing to scale up to 10 faults where prior work timeout for 3 faults. In addition, we analyze the well-tested WooKey bootloader, and demonstrate the ability of our analysis to find attacks and evaluate countermeasures in real-life security scenarios. We were especially able to find an attack not mentioned in a previous patch.},
	author = {Bardin, S. and  Ducousso, S. and  Potet, M.-L.},
	pages = {58-89},
	publisher = {Springer},
	year = {2023},
	eprinttype={HAL}, eprint = {cea-04199882},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{dang_counterexample_guided_imitation_2023_hal-04295795,
	title = {Counter-Example Guided Imitation Learning of Feedback Controllers from Temporal Logic Specifications},
	booktitle = {62nd IEEE Conference on Decision and Control (CDC 2023)},
	abstract = {We present a novel method for imitation learning for control requirements expressed using Signal Temporal Logic (STL). More concretely we focus on the problem of training a neural network to imitate a complex controller. The learning process is guided by efficient data aggregation based on counterexamples and a coverage measure. Moreover, we introduce a method to evaluate the performance of the learned controller via parameterization and parameter estimation of the STL requirements. We demonstrate our approach with a flying robot case study.},
	author = {Dang, T. and  Donzé, A. and  Haque, I. and  Kekatos, N. and  Saha, I.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04295795},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{gourdin_lazy_code_transformations_2023_hal-04108775,
	title = {Lazy Code Transformations in a Formally Verified Compiler},
	booktitle = {ICOOOLPS '23: 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems},
	url = {https://conf.researchr.org/track/ecoop-issta-2023/ICOOOLPS-2023},
	doi = {10.1145/3605158.3605848},
	abstract = {Translation validation verifies the results of an untrusted translator---called an oracle---at the compiler's runtime using a validator. This approach enables validating intricate optimizations without having to prove them directly. Parametrizing such a validator with hints provided by oracles greatly simplifies its integration within a formally verified compiler---such as CompCert. However, generating those hints requires adapting state-of-the-art optimizations. The co-design of a validation framework supporting a class of optimizations led us to improve the Lazy Code Motion (LCM) and Lazy Strength Reduction (LSR) data-flow algorithms of Knoop, Rüthing, and Steffen. We propose an efficient implementation in OCaml combining both LCM and LSR, operating over basic-blocks, and whose result is checked by a Coq-verified validator. We show how to generate invariant annotations from the data-flow equations as hints for the defensive validation, and we introduce several algorithmic refinements w.r.t. the original papers. Our solution is fully integrated within CompCert, and to the best of our knowledge, it is the first formally verified strength-reduction of loop-induction variables.},
	author = {Gourdin, L.},
	pages = {3-14},
	publisher = {ACM},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04108775},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v4},
}

@inproceedings{larchey-wendling_proof_pearl_faithful_2023_hal-04200527,
	title = {Proof Pearl: Faithful Computation and Extraction of µ-Recursive Algorithms in Coq},
	volume = {278},
	editor= {LIPICS},
	booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
	url = {https://mizar.uwb.edu.pl/ITP2023/program.html},
	doi = {10.4230/LIPIcs.ITP.2023.21},
	abstract = {Basing on an original Coq implementation of unbounded linear search for partially decidable predicates, we study the computational contents of µ-recursive functions via their syntactic representation, and a correct by construction Coq interpreter for this abstract syntax. When this interpreter is extracted, we claim the resulting OCaml code to be the natural combination of the implementation of the µ-recursive schemes of composition, primitive recursion and unbounded minimization of partial (i.e., possibly non-terminating) functions. At the level of the fully specified Coq terms, this implies the representation of higher-order functions of which some of the arguments are themselves partial functions. We handle this issue using some techniques coming from the Braga method. Hence we get a faithful embedding of µ-recursive algorithms into Coq preserving not only their extensional meaning but also their intended computational behavior. We put a strong focus on the quality of the Coq artifact which is both self contained and with a line of code count of less than 1k in total.},
	author = {Larchey-Wendling, D. and  Monin, J.-F.},
	pages = {21:1--17},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04200527},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{mambakam_pattern_matching_and_2023_hal-04295896,
	title = {Pattern Matching and Parameter Identification for Parametric Timed Regular Expressions},
	booktitle = {26th ACM International Conference on Hybrid Systems: Computation and Control},
	doi = {10.1145/3575870.3587115},
	abstract = {Timed formalisms such as Timed Automata (TA), Signal Temporal Logic (STL) and Timed Regular expressions (TRE) have been previously applied as behaviour specifications for monitoring or runtime verification, in particular, under the form of pattern-matching, i.e. computing the set of all the segments of a given system run that satisfy the specification. In this work, timed regular expressions with parameters (for timing delays and for signal values) are considered. We define several classes of parametric expressions (based on Boolean or real-valued signals and discrete events), and tackle the problem of computing a parametric match-set, i.e. the parameter values and time segments of data that give a match for a given expression. We propose efficient data structures for representing match-sets (combining zones and polytopes), and devise pattern-matching algorithms. All these different types and algorithms are combined into a single implementation under a tool named parameTRE. We illustrate the approach on several examples, from electrocardiograms to driving patterns. CCS CONCEPTS • Theory of computation → Timed and hybrid models; • Computing methodologies → Algebraic algorithms.},
	author = {Mambakam, A. and  Asarin, E. and  Basset, N. and  Dang, T.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04295896},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	HAL_version = {v1},
}

@inproceedings{monniaux_data_abstraction_arrays_2023_hal-04750127,
	title = {Data Abstraction, Arrays, Maps, and Completeness, aka "Cell Morphing},
	volume = {402},
	editor= {David Monniaux and José F. Morales},
	booktitle = {10th Workshop on Horn Clauses for Verification and Synthesis (HCVS)},
	url = {https://www.sci.unich.it/hcvs23/},
	doi = {10.4204/EPTCS.402},
	author = {Monniaux, D.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04750127},
	peer_reviewing = {0},
	audience = {2},
	proceedings = {1},
	invited_communication = {1},
	HAL_version = {v1},
}

@inproceedings{monniaux_testing_a_formally_2023_hal-04096390,
	title = {Testing a Formally Verified Compiler},
	volume = {14066},
	editor= {Virgile Prevosto and Cristina Seceleanu},
	series = {Lecture Notes in Computer Science},
	booktitle = {Tests and Proofs (TAP 2023)},
	url = {https://conf.researchr.org/home/tap-2023},
	doi = {10.1007/978-3-031-38828-6_3},
	abstract = {We report on how we combine tests and formal proofs while developing extensions to the CompCert formally verified compiler.},
	author = {Monniaux, D. and  Gourdin, L. and  Boulmé, S. and  Lebeltel, O.},
	pages = {40-48},
	publisher = {Springer Nature Switzerland},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04096390},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{moussa_databased_extended_moving_2023_hal-04295820,
	title = {Data-based Extended Moving Horizon Estimation for MISO Anesthesia Dynamics},
	booktitle = {CDC 2023 - 62nd IEEE Conference on Decision and Control},
	url = {https://cdc2022.ieeecss.org/},
	abstract = {This paper presents an extended moving horizon observer to estimate both the states and the pharmacodynamic (PD) parameters of an anesthesia model, based on real data. The inputs of this model are the injection rates of Propofol and Remifentanil. The states represent the concentration of the anesthetic agents in different compartments of the human body (muscles, fat, blood) and in the effect site. The considered output is the Bispectral index (BIS) which is derived from the electroencephalogram (EEG). The observer is designed such that the parameters are estimated during the anesthesia induction phase, and then almost frozen for the rest of the surgery. The estimator is validated on real data that were extracted from the VitalDB database [12].},
	author = {Moussa, K. and  Aubouin--Pairault, B. and  Alamir, M. and  Dang, T.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04295820},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{rasoldier_assessing_the_potential_2023_hal-04401006,
	title = {Assessing the Potential of Carpooling for Reducing Vehicle Kilometers Traveled},
	booktitle = {ICT4S 2023 - 9th International Conference on Information and Communications Technology for Sustainability},
	doi = {10.1109/ICT4S58814.2023.00021},
	abstract = {The national and local strategies implemented to achieve the French Nationally Determined Contribution (a key element of the Paris Agreement) rely heavily on technological improvements to reach carbon neutrality by 2050, which raises the question of whether these technologies can rise to the challenge, and which social changes are needed to make these technologies reach their full potential. One example of this is the use of digital platforms for developing carpooling. We study the maximum potential of two carpooling schemes for local travel. Our results show that a massive adoption of carpooling would be needed to reach targets set by the national and local strategies, even under maximizing assumptions.},
	author = {Rasoldier, A. and  Girault, A. and  Quinton, S. and  Combaz, J. and  Marquet, K.},
	pages = {120-131},
	publisher = {IEEE},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04401006},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{vigouroux_baxmc_a_cegar_2022_hal-03773005,
	title = {BAXMC: a CEGAR approach to Max\#SAT},
	booktitle = {FMCAD 2022},
	doi = {10.34727/2022/isbn.978-3-85448-053-2},
	abstract = {Max\#SAT is an important problem with multiple applications in security and program synthesis that is proven hard to solve. It is defined as: given a parameterized quantifier-free propositional formula compute parameters such that the number of models of the formula is maximal. As an extension, the formula can include an existential prefix. We propose a CEGAR-based algorithm and refinements thereof, based on either exact or approximate model counting, and prove its correctness in both cases. Our experiments show that this algorithm has much better effective complexity than the state of the art.},
	author = {Vigouroux, T. and  Ene, C. and  Monniaux, D. and  Mounier, L. and  Potet, M.-L.},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03773005},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v2},
}

@inproceedings{al_qadasi_deepabstraction_2level_prioritization_2022_hal-03911812,
	title = {DeepAbstraction: 2-Level Prioritization for Unlabeled Test Inputs in Deep Neural Networks},
	booktitle = {AITest 2022 - IEEE 4th International Conference On Artificial Intelligence Testing},
	abstract = {Deep learning systems recently achieved unprecedented success in various industries. However, DNNs still exhibit some erroneous behaviors, which lead to catastrophic results. As a result, more data should be collected to cover more corner cases. On the other hand, a massive amount of data consumes more human annotators (oracle), which increases the labeling budget and time. We propose an effective test prioritization technique, called DeepAbstraction to prioritize the more likely error-exposing instances among the entire unlabeled test dataset. The ultimate goal of our framework is to reduce the labeling cost and select the potential corner cases earlier before production. Different from existing work, DeepAbstraction leverages runtime monitors. In the literature, runtime monitors are primarily used to supervise the prediction of the neural network. Then, monitors trigger a verdict for each prediction: acceptance, rejection, or uncertainty. Monitors quantify the acquired knowledge into box abstraction during the training. Each box abstraction contains instances that share similar high-level features. In the test part, the verdict of monitor depends in which box abstraction a test instance resides. Moreover, we study intensively where corner cases can reside in the feature space, either near-boundary regions or nearcentroid regions. The existing test prioritization techniques can only prioritize many near-boundary instances and a few nearcentroid instances. Nevertheless, DeepAbstraction can effectively prioritize numerous instances from both regions. Therefore, our evaluation shows that DeepAbstraction outperforms the state-ofthe-art test prioritization techniques.},
	author = {Al qadasi, H. and  Wu, C. and  Falcone, Y. and  Bensalem, S.},
	pages = {1-8},
	publisher = {IEEE},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03911812},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{baouya_formal_modelling_and security_2022_hal-04086240,
	title = {Formal Modelling and Security Analysis of Inter-Operable Systems},
	volume = {13343},
	editor= {Hamido Fujita and Philippe Fournier-Viger and Moonis Ali and Yinglin Wang},
	series = {Lecture Notes in Computer Science},
	booktitle = {35th International Conference on Industrial, Engineering and Other Applications of Applied Intelligent Systems (IEA AIE 2022)},
	url = {https://link.springer.com/book/10.1007/978-3-031-08530-7},
	doi = {10.1007/978-3-031-08530-7_47},
	abstract = {Emerging technologies utilised in building modern systems make them inter-operable but potentially exposed to security threats. Thus, engineers need to consider the system structure and behaviour at the design level. This paper addresses the security risk assessment of inter-operable IoT systems designed in BIP (Behaviour-Interaction-Priority). For this purpose, we model different attacks scenarios from Microsoft STRIDE threats catalogue and identify the threats entry points in the component-port-connector architecture. Using standards communication styles such as message passing, we compose architectural components to model data flow between communication entities. We use BIP statistical model checking to assess the architecture conformance regarding security properties expressed in temporal logic.},
	author = {Baouya, A. and  Ouchani, S. and  Bensalem, S.},
	pages = {555-567},
	publisher = {Springer International Publishing},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-04086240},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{bozga_decision_problems_in_2022_hal-03750586,
	title = {Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems},
	volume = {13385},
	series = {Lecture Notes in Computer Science},
	booktitle = {International Joint Conference on Automated Reasoning},
	doi = {10.1007/978-3-031-10769-6_40},
	abstract = {We consider a logic used to describe sets of configurations of distributed systems, whose network topologies can be changed at runtime, by reconfiguration programs. The logic uses inductive definitions to describe networks with an unbounded number of components and interactions, written using a multiplicative conjunction, reminiscent of Bunched Implications [38] and Separation Logic [40]. We study the complexity of the satisfiability and entailment problems for the configuration logic under consideration. Additionally, we consider robustness properties, such as tightness (are all interactions entirely connected to components?) and degree boundedness (is every component involved in a bounded number of interactions?), the latter being an ingredient for decidability of entailments.},
	author = {Bozga, M. and  Bueri, L. and  Iosif, R.},
	pages = {691-711},
	publisher = {Springer International Publishing},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03750586},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{ferres_electrical_rule_checking_2023_hal-04007446,
	title = {Electrical Rule Checking of Integrated Circuits using Satisfiability Modulo Theory},
	booktitle = {DATE 2023 - Design, Automation and Test in Europe Conference},
	doi = {10.23919/DATE56975.2023.10137147},
	abstract = {We consider the verification of electrical properties of circuits to identify potential violations of electrical design rules, also called Electrical Rule Checking (ERC). We present a general approach based on Satisfiability Modulo Theory (SMT) to verify that these errors cannot occur in a given circuit. We claim that our approach is scalable and more precise than existing analyses, like voltage propagation. We applied these techniques to a specific type of errors, the missing level shifters. On an industrial casestudy, our technique is able to flag 31\% of the warnings raised by the voltage propagation analysis as being false alarms.},
	author = {Ferres, B. and  Oulkaid, O. and  Henrio, L. and  G. and  M. K. and  Moy, M. and  Radanne, G. and  Raymond, P.},
	pages = {1-2},
	publisher = {IEEE},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04007446},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{monniaux_formally_verified_32_2022_hal-03722203,
	title = {Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic},
	booktitle = {2022 IEEE 29th Symposium on Computer Arithmetic (ARITH)},
	doi = {10.1109/ARITH54963.2022.00032},
	abstract = {Some recent processors are not equipped with an integer division unit. Compilers then implement division by a call to a special function supplied by the processor designers, which implements division by a loop producing one bit of quotient per iteration. This hinders compiler optimizations and results in non-constant time computation, which is a problem in some applications. We advocate instead using the processor's floating-point unit, and propose code that the compiler can easily interleave with other computations. We fully proved the correctness of our algorithm, which mixes floating-point and fixed-bitwidth integer computations, using the Coq proof assistant and successfully integrated it into the CompCert formally verified compiler.},
	author = {Monniaux, D. and  Pain, A.},
	pages = {128-132},
	publisher = {IEEE},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03722203},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{monniaux_the_trusted_computing_2022_hal-03541595,
	title = {The Trusted Computing Base of the CompCert Verified Compiler},
	volume = {13240},
	editor= {Ilya Sergey},
	series = {Lecture notes in computer science},
	booktitle = {Programming Languages and Systems (ESOP 2022)},
	url = {https://etaps.org/2022/esop},
	doi = {10.1007/978-3-030-99336-8_8},
	abstract = {CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.},
	author = {Monniaux, D. and  Boulmé, S.},
	pages = {204-233},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03541595},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v2},
}

@inproceedings{rasoldier_how_realistic_are_2022_hal-03949261,
	title = {How realistic are claims about the benefits of using digital technologies for GHG emissions mitigation?},
	booktitle = {LIMITS 2022 - Eighth Workshop on Computing within Limits},
	abstract = {While the direct environmental impacts of digital technologies are now well documented, it is often said that they could also help reduce greenhouse gas (GHG) emissions significantly in many domains such as transportation, building, manufacturing, agriculture, and energy. Assessing such claims is essential to avoid delaying alternative action or research. This also applies to related claims about how much GHG emissions existing digital technologies are already avoiding. In this paper, we point out critical issues related to these topics in the state of the art. First, most papers do not provide enough details on the scenarios underlying their evaluations: which hypotheses they are based on and why, and why specific scenarios are chosen as the baseline. This is a key point because it may lead to overestimating the current or potential benefits of digital solutions. Second, results are rarely discussed in the context of global strategies for GHG emissions reduction. These leaves open how the proposed technologies would fit into a realistic plan for meeting current GHG reduction goals. To overcome the underlined limitations, we propose a set of guidelines that all studies on digital solutions for mitigating GHG emissions should satisfy, point out overlooked research directions, and provide concrete examples and initial results for the specific case of carpooling.},
	author = {Rasoldier, A. and  Combaz, J. and  Girault, A. and  Marquet, K. and  Quinton, S.},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03949261},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{six_formally_verified_superblock_2022_hal-03200774,
	title = {Formally Verified Superblock Scheduling},
	editor= {Andrei Popescu and Steve Zdancewic},
	booktitle = {Certified Programs and Proofs (CPP ’22)},
	doi = {10.1145/3497775.3503679},
	abstract = {On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks (it may move instructions across branches), along with its performance evaluation. It is integrated within the CompCert C compiler, providing a complete machine-checked proof of semantic preservation from C to assembly. Our optimizer composes several passes designed by translation validation: program transformations are proposed by untrusted oracles, which are then validated by certified and scalable checkers. Our main checker is an architecture-independent simulation-test over superblocks modulo register liveness, which relies on hash-consed symbolic execution.},
	author = {Six, C. and  Gourdin, L. and  Boulmé, S. and  Monniaux, D. and  Fasse, J. and  Nardino, N.},
	pages = {40-54},
	publisher = {ACM Digital Library},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03200774},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v2},
}

@inproceedings{altisen_certification_of_an_2021_hal-03547154,
	title = {Certification of an Exact Worst-Case Self-Stabilization Time},
	booktitle = {ICDCN '21: International Conference on Distributed Computing and Networking 2021},
	doi = {10.1145/3427796.3427832},
	author = {Altisen, K. and  Corbineau, P. and  Devismes, S.},
	pages = {46-55},
	publisher = {ACM},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03547154},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{altisen_on_implementing_stabilizing_2021_hal-03346225,
	title = {On Implementing Stabilizing Leader Election with Weak Assumptions on Network Dynamics},
	booktitle = {PODC '21: ACM Symposium on Principles of Distributed Computing},
	doi = {10.1145/3465084.3467917},
	abstract = {We consider self-stabilization and its weakened form called pseudo-stabilization. We study conditions under which (pseudo- and self-) stabilizing leader election is solvable in networks subject to frequent topological changes. To model such an high dynamics, we use the dynamic graph (DG) paradigm and study a taxonomy of nine important DG classes. Our results show that self-stabilizing leader election can only be achieved in the classes where all processes are sources. Furthermore, even pseudo-stabilizing leader election cannot be solved in all remaining classes, except in the class where at least one process is a timely source. We illustrate that result by proposing a pseudo-stabilizing leader election algorithm for the latter class. We also show that in this last case, the convergence time of pseudo-stabilizing leader election algorithms cannot be bounded. Nevertheless, we show that our solution is speculative since its convergence time can be bounded when the dynamics is not too erratic, precisely when all processes are timely sources.},
	author = {Altisen, K. and  Devismes, S. and  Durand, A. and  Johnen, C. and  Petit, F.},
	pages = {21-31},
	publisher = {ACM},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03346225},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{altisen_selfstabilizing_systems_in_2021_hal-02376832,
	title = {Self-stabilizing Systems in Spite of High Dynamics},
	series = {ICDCN '21: International Conference on Distributed Computing and Networking 2021},
	booktitle = {22nd International Conference on Distributed Computing and Networking, ICDCN'21},
	url = {http://www.icdcn2021.net},
	doi = {10.1145/3427796.3427838},
	abstract = {We initiate research on self-stabilization in highly dynamic message-passing systems by addressing the self-stabilizing leader election problem in three wide classes of time-varying graphs (TVGs): the class of TVGs with temporal diameter bounded by Delta (boundDiam), the class of TVGs with temporal diameter quasi-bounded by Delta (quasiBoundDiam), and the class of TVGs with recurrent connectivity only (recur). We first study conditions under which our problem can be solved. We introduce the notion of size-ambiguity to show that the assumption on the knowledge of the number $n$ of processes is crucial. Our results show that any deterministic self-stabilizing leader election algorithm working in the class quasiBoundDiam or recur cannot be size-ambiguous, justifying then the necessity of assuming the exact knowledge of network size in those classes. We then present three self-stabilizing leader election algorithms for Classes boundDiam, quasiBoundDiam, and recur, respectively. Our algorithm for boundDiam stabilizes in at most 2.Delta rounds. In quasiBoundDiam and recur, stabilization time cannot be bounded. However, we show that our solutions are speculative in the sense that their stabilization time in boundDiam is O(Delta) rounds.},
	author = {Altisen, K. and  Devismes, S. and  Durand, A. and  Johnen, C. and  Petit, F.},
	pages = {156–165},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-02376832},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v3},
}

@inproceedings{balabonski_computer_aided_formal_2021_hal-03425768,
	title = {Computer Aided Formal Design of Swarm Robotics Algorithms},
	volume = {13046},
	series = {Lecture Notes in Computer Science},
	booktitle = {Stabilization, Safety, and Security of Distributed Systems. SSS 2021},
	doi = {10.1007/978-3-030-91081-5_31},
	author = {Balabonski, T. and  Courtieu, P. and  Pelle, R. and  Rieg, L. and  Tixeuil, S. and  Urbain, X.},
	pages = {469-473},
	publisher = {Springer International Publishing},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03425768},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{bozga_specification_and_safety_2021_hal-03418644,
	title = {Specification and Safety Verification of Parametric Hierarchical Distributed Systems},
	volume = {13077},
	series = {Lecture Notes in Computer Science},
	booktitle = {Formal Aspects of Component Software},
	doi = {10.1007/978-3-030-90636-8_6},
	abstract = {We introduce a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of components. The language allows to describe infinite sets of systems whose coordination between components share the same pattern, using inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. Further, we give a verification method for the parametric systems described in this language, relying on the automatic synthesis of structural invariants that enable proving general safety properties (absence of deadlocks and critical section violations). The invariants are defined using the WSκS fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection. This reduces the safety verification problem to checking satisfiability of a WSκS formula. We implemented the invariant synthesis method into a prototype tool and carried out verification experiments on a number of non-trivial models specified using the term algebra.},
	author = {Bozga, M. and  Iosif, R.},
	pages = {95-114},
	publisher = {Springer International Publishing},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03418644},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{braine_data_abstraction_a_2021_hal-03321868,
	title = {Data Abstraction: A General Framework to Handle Program Verification of Data Structures},
	volume = {12913},
	series = {Lecture notes in computer science},
	booktitle = {SAS 2021 - 28th Static Analysis Symposium},
	doi = {10.1007/978-3-030-88806-0_11},
	abstract = {Proving properties on programs accessing data structures such as arrays often requires universally quantified invariants, e.g., "all elements below index i are nonzero". In this article, we propose a general data abstraction scheme operating on Horn formulas, into which we recast previously published abstractions. We show that our instantiation scheme is relatively complete: the generated purely scalar Horn clauses have a solution (inductive invariants) if and only if the original problem has one expressible by the abstraction.},
	author = {Braine, J. and  Gonnord, L. and  Monniaux, D.},
	pages = {215-235},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03321868},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{brau_contractbased_verification_of_2021_hal-03059942,
	title = {Contract-Based Verification of Model Transformations: A Formally Founded Approach},
	booktitle = {36th ACM/SIGAPP Symposium On Applied Computing (SAC 2021)},
	abstract = {In safety-critical applications, using a Model Driven Engineering (MDE) approach requires a high level of trust in its underlying model transformations, the correctness of which should be verified formally. However, such verification remains challenging due to the absence of formal foundations of most model-based frameworks involved in MDE (e.g. AADL, SysML). In this paper, we propose a formally founded environment to verify certain aspects of correctness of model transformations in MDE. First, we define a transformation formally: this involves formalizing input and output models at some level of abstraction, as well as the transformation rules. Then, we extend the formalized transformation with contracts to build a Transition System (TS) representing a lightweight extensible verification environment. Finally, we formulate and verify correctness properties which we reduce, based on the previous steps, to reachability properties over the TS. We show how our approach is implemented in Ocarina, an open-source transformation tool for AADL, and how it applies, for example, to build correct transformations from AADL models to real-time task models in Cheddar ADL.},
	author = {Brau, G. and  Foughali, M.},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03059942},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{bégay_developing_and_certifying_2021_hal-03065304,
	title = {Developing and certifying Datalog optimizations in Coq/MathComp},
	booktitle = {Certified Programs and Proofs (CPP ’21)},
	doi = {10.1145/3437992.3439913},
	author = {Bégay, P.-L. and  Crégut, P. and  Monin, J.-F.},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03065304},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v2},
}

@inproceedings{echenim_unifying_decidable_entailments_2021_hal-03304653,
	title = {Unifying Decidable Entailments in Separation Logic with Inductive Definitions},
	booktitle= {Automated Deduction - {CADE} 28 - 28th International Conference on               Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings}},
	series = {Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event},
	booktitle = {CADE 28},
	doi = {10.1007/978-3-030-79876-5_11},
	abstract = {The entailment problem φ |= ψ in Separation Logic [12,15], between separated conjunctions of equational (x ≈y and x 6≈y), spatial (x 7→(y1,...,yκ)) and predicate (p(x1,...,xn)) atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, called establishment [10,13,14] and restrictedness [8], respectively. Both classes are shown to be in 2EXPTIME by the independent proofs from [14] and [8], respectively, and a many-one reduction of established to restricted entailment problems has been given [8]. In this paper, we strictly generalize the restricted class, by distinguishing the conditions that apply only to the left- (φ) and the right- (ψ) hand side of entailments, respectively. We provide a many-one reduction of this generalized class, called safe, to the established class. Together with the reduction of established to restricted entailment problems, this new reduction closes the loop and shows that the three classes of entailment problems (respectively established, restricted and safe) form a single, unified, 2EXPTIME-complete class},
	author = {Echenim, M. and  Iosif, R. and  Peltier, N.},
	pages = {183-199},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03304653},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{falcone_monitoring_distributed_componentbased_2021_hal-03525762,
	title = {Monitoring Distributed Component-Based Systems},
	booktitle = {FACS 2021 - 17th edition of the International Conference on Formal Aspects of Component Software},
	abstract = {We monitor asynchronous distributed component-based systems with multi-party interactions. We consider independent components whose interactions are managed by several distributed schedulers. In this context, neither a global state nor the total ordering of the executions of the system is available at runtime. We instrument the system to retrieve local events from the local traces of the schedulers. Local events are sent to a global observer which reconstructs on-the-fly the set of global traces that are compatible with the local traces, in a concurrency-preserving fashion. The set of compatible global traces is represented in the form of an original lattice over partial states, such that each path of the lattice corresponds to a possible execution of the system.},
	author = {Falcone, Y. and  Nazarpour, H. and  Bensalem, S. and  Bozga, M.},
	pages = {1-19},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03525762},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{mari_explaining_safety_violations_2021_hal-03348010,
	title = {Explaining Safety Violations in Real-Time Systems},
	booktitle= {Proc. 19th FORMATS 2021, Paris, France},
	booktitle = {FORMATS 2021 - Formal Modeling and Analysis of Timed Systems},
	doi = {10.1007/978-3-030-85037-1_7},
	abstract = {We tackle the problem of explaining faults in real-time systems. Intuitively, an explanation of the violation of a safety property by an execution is a concise excerpt of the faulty execution that retains only the elements that were relevant for entailing the violation, thus exhibiting how causes accumulate over time and propagate to entail the effect. Fault explanation therefore goes beyond the well-known concepts of fault diagnosis and localization. We provide a formal definition of causal explanations on dense-time models, based on the well-studied formalisms of timed automata and zone-based abstractions. Our approach is able to account for limited observability of the faulty execution. We propose a symbolic formalization to effectively construct such explanations, which we have implemented in a prototype tool. We illustrate our approach on several examples.},
	author = {Mari, T. and  Dang, T. and  Gössler, G.},
	pages = {100-116},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03348010},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{monniaux_simple_light_yet_2021_hal-03212087,
	title = {Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion},
	editor= {Jörg Henkel and Xu Liu},
	booktitle = {Languages, Compilers, Tools and Theory of Embedded Systems (LCTES)},
	url = {https://pldi21.sigplan.org/home/LCTES-2021},
	doi = {10.1145/3461648.3463850},
	abstract = {We present an approach for implementing a formally certified loop-invariant code motion optimization by composing an unrolling pass and a formally certified yet efficient global subexpression elimination. This approach is lightweight: each pass comes with a simple and independent proof of correctness. Experiments show the approach significantly narrows the performance gap between the CompCert certified compiler and state-of-the-art optimizing compilers. Our static analysis employs an efficient yet verified hashed set structure, resulting in fast compilation.},
	author = {Monniaux, D. and  Six, C.},
	pages = {85-96},
	publisher = {ACM},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03212087},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{rauch_optimal_exclusive_perpetual_2021_hal-03547159,
	title = {Optimal Exclusive Perpetual Grid Exploration by Luminous Myopic Robots Without Common Chirality},
	volume = {12754},
	editor= {Karima Echihabi, Roland Meyer},
	series = {Lecture Notes in Computer Science},
	booktitle = {9th International Conference, NETYS 2021},
	doi = {10.1007/978-3-030-91014-3_7},
	abstract = {We consider swarms of luminous myopic robots that run in synchronous Look-Compute-Move cycles. These robots evolve in a finite grid and are disoriented, i.e., they have neither global compass nor a common chirality. In this context, we propose optimal solutions for the perpetual exploration of a finite grid. Precisely, we investigate optimality in terms of the visibility range, number of robots, number of colors. In more detail, under the optimal visibility range one, we give an algorithm which is optimal w.r.t. the number of robots: it uses three robots and three colors. Under visibility two, we design an algorithm that uses five robots and only one color, i.e., robots are oblivious.},
	author = {Rauch, A. and  Bramas, Q. and  Devismes, S. and  Lafourcade, P. and  Lamani, A.},
	pages = {95-110},
	publisher = {Springer International Publishing},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03547159},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{recoules_interface_compliance_of_2021_cea-04228171,
	title = {Interface compliance of inline assembly: automatically check, patch and refine},
	series = {2021 Proceedings of IEEE/ACM 43rd International Conference on Software Engineering (ICSE'21)},
	booktitle = {2021 IEEE/ACM  - 43rd International Conference on Software Engineering},
	url = {https://dl.acm.org/doi/abs/10.1109/ICSE43902.2021.00113},
	doi = {10.1109/ICSE43902.2021.00113},
	abstract = {Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes in the GNU syntax (supported by major compilers such as GCC, Clang and ICC) have an interface specifying how the assembly codes interact with the C environment. For simplicity reasons, the compiler treats GNU inline assembly codes as blackboxes and relies only on their interface to correctly glue them into the compiled C code. Therefore, the adequacy between the assembly chunk and its interface (named compliance) is of primary importance, as such compliance issues can lead to subtle and hard-to-find bugs. We propose RUSTInA, the first automated technique for formally checking inline assembly compliance, with the extra ability to propose (proven) patches and (optimization) refinements in certain cases. RUSTInA is based on an original formalization of the inline assembly compliance problem together with novel dedicated algorithms. Our prototype has been evaluated on 202 Debian packages with inline assembly (2656 chunks), finding 2183 issues in 85 packages - 986 significant issues in 54 packages (including major projects such as ffmpeg or ALSA), and proposing patches for 92\% of them. Currently, 38 patches have already been accepted (solving 156 significant issues), with positive feedback from development teams.},
	author = {Recoules, F. and  Bardin, S. and  Bonichon, R. and  Lemerre, M. and  Mounier, L. and  Potet, M.-L.},
	pages = {1236-1247},
	year = {2021},
	eprinttype={HAL}, eprint = {cea-04228171},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{altisen_brief_announcement_selfstabilizing_2020_hal-02911071,
	title = {Brief Announcement: Self-stabilizing Systems in Spite of High Dynamics},
	booktitle = {PODC 2020 - ACM Symposium on Principles of Distributed Computing},
	doi = {10.1145/3382734.3404502},
	abstract = {We initiate research on self-stabilization in highly dynamic identified message-passing systems where dynamics is modeled using time-varying graphs (TVGs). More precisely, we address the self-stabilizing leader election problem in three wide classes of TVGs: the class $TC^B(∆)$ of TVGs with temporal diameter bounded by $∆$, the class $TC^Q(∆)$ of TVGs with temporal diameter quasi-bounded by $∆$, and the class $TC^R$ of TVGs with recurrent connectivity only, where TC^B(∆) ⊆ $TC^Q(∆) ⊆ TC^R$. We first study conditions under which our problem can be solved. Precisely, we introduce the notion of size-ambiguity to show that the assumption on the knowledge of the number n of processes is central. Our results reveal that, despite the existence of unique process identifiers, any deterministic self-stabilizing leader election algorithm working in the TVG class $TC^Q(∆)$ or $TC^R$ cannot be size-ambiguous, justifying why our solutions for those classes assume the exact knowledge of n. We then present three self-stabilizing leader election algorithms for the TVG classes $TC^B(∆)$, $TC^Q(∆)$, and $TC^R$, respectively.},
	author = {Altisen, K. and  Devismes, S. and  Durand, A. and  Johnen, C. and  Petit, F.},
	publisher = {ACM},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02911071},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{baouya_fog_computing_and_2020_hal-02902383,
	title = {Fog Computing and Blockchain Technology for Massive IoT Deployment},
	booktitle = {2020 9th Mediterranean Conference on Embedded Computing (MECO)},
	doi = {10.1109/MECO49872.2020.9134098},
	author = {Baouya, A. and  Chehida, S. and  Bensalem, S. and  Bozga, M.},
	pages = {1-4},
	publisher = {IEEE},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02902383},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{barbot_falsification_of_cyberphysical_2020_hal-03049273,
	title = {Falsification of Cyber-Physical Systems with Constrained Signal Spaces},
	booktitle= {NASA Formal Methods. NFM 2020},
	booktitle = {NASA Formal Methods},
	doi = {10.1007/978-3-030-55754-6_25},
	abstract = {Falsification has garnered much interest recently as a way to validate complex CPS designs with respect to a specification expressed via temporal logics. Using their quantitative semantics, the falsification problem can be formulated as robustness minimization problem. To make this infinite-dimensional problem tractable, a common approach is to restrict to classes of signals that can be defined using a finite number of parameters, such as piecewise-constant or piecewise-linear signals with fixed time intervals). A major drawback of this approach is that when the input signals must satisfy non-trivial temporal constraints, encoding these constraints into bounded domains for parameters can be difficult. In this work, to better capture temporal constraints on the input signal space, we use timed automata (TA) and make use of a transformation that allows sampling TA traces by sampling points in the unit box. We exploit this transformation to efficiently encode constrained CPS signals in the robustness minimization problem. This transformation also allows us to define an effective coverage measure of the constrained signal space so as to provide quantitative guarantees when no falsifying behaviour is found. In addition, this coverage is used to improve the black-box optimisation performance by detecting situations where the search is stuck near a local optimum. The approach is demonstrated on a ∆Σ modulator and a model of car automatic transmission subject to constraints describing usual driving patterns.},
	author = {Barbot, B. and  Basset, N. and  Dang, T. and  Donzé, A. and  Kapinski, J. and  Yamaguchi, T.},
	pages = {420-439},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03049273},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{basset_learning_specifications_for_2020_hal-03035697,
	title = {Learning Specifications for Labelled Patterns},
	booktitle = {Proceedinfs of the 18th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2020)},
	abstract = {In this work, we introduce a supervised learning framework for inferring temporal logic specifications from labelled patterns in signals, so that the formulae can then be used to correctly detect the same patterns in unlabelled samples. The input patterns that are fed to the training process are labelled by a Boolean signal that captures their occurrences. To express the patterns with quantitative features, we use parametric specifications that are increasing, which we call Increasing Parametric Pattern Predictor (IPPP). This means that augmenting the value of the parameters makes the predicted pattern true on a larger set. A particular class of parametric specification formalisms that we use is Parametric Signal Temporal Logic (PSTL). One of the main contributions of this paper is the definition of a new measure, called-count, to assess the quality of the learned formula. This measure enables us to compare two Boolean signals and, hence, quantifies how much the labelling signal induced by the formula differs from the true labelling signal (e.g. given by an expert). Therefore, the-count can measure the number of mismatches (either false positives or false negatives) up to some error tolerance. Our supervised learning framework can be expressed by a multicriteria optimization problem with two objective functions: the minimization of false positives and false negatives given by the parametric formula on a signal. We provide an algorithm to solve this multi-criteria optimization problem. Our approach is demonstrated on two case studies involving characterization and classification of labeled ECG (electrocardiogram) data.},
	author = {Basset, N. and  Dang, T. and  Mambakam, A. and  Jarabo, J. I. R.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03035697},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{boespflug_countermeasures_optimization_in_2020_hal-02951150,
	title = {Countermeasures Optimization in Multiple Fault-Injection Context},
	booktitle = {"Fault Diagnosis and Tolerance in Cryptography" FDTC  2020},
	doi = {10.1109/FDTC51366.2020.00011},
	abstract = {Fault attacks consist in changing the program behavior by injecting faults at run-time, either at hardware or at software level. Their goal is to change the correct progress of the algorithm and hence, either to allow gaining some privilege access or to allow retrieving some secret information based on an analysis of the deviation of the corrupted behavior with respect to the original one. Countermeasures have been proposed to protect embedded systems by adding spatial, temporal or information redundancy at hardware or software level. First we define Countermeasures Check Point (CCP) and CCPs-based countermeasures as an important subclass of countermeasures. Then we propose a methodology to generate an optimal protection scheme for CCPs-based countermeasure. Finally we evaluate our work on a benchmark of code examples with respect to several Control Flow Integrity (CFI) oriented existing protection schemes.},
	author = {Boespflug, E. and  Ene, C. and  Mounier, L. and  Potet, M.-L.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02951150},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{bozga_structural_invariants_for_2020_hal-02388027,
	title = {Structural Invariants for the Verification of Systems with Parameterized Architectures},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020},
	abstract = {We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g. rendezvous , broadcast) and the topology of the system (e.g. pipeline, ring). The logic can be easily embedded in monadic second logic of κ ≥ 1 successors (WSκS), and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions , without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify many textbook examples, such as dining philosophers, mutual exclusion protocols, and concurrent systems with preemption and priorities, for an arbitrary number of components.},
	author = {Bozga, D. M. and  Esparza, J. and  Iosif, R. and  Sifakis, J. and  Welzel, C. and  Bozga, M.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02388027},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v2},
}

@inproceedings{bramas_finding_water_on_2020_hal-02559617,
	title = {Finding Water on Poleless using Melomaniac Myopic Chameleon Robots},
	volume = {157},
	booktitle = {Tenth International Conference on Fun with Algorithms (FUN 2020)},
	doi = {10.4230/LIPIcs.FUN.2021.6},
	author = {Bramas, Q. and  Lafourcade, P. and  Devismes, S.},
	pages = {6:1-6:19},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02559617},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{bramas_vers_linfini_et_2020_hal-02791601,
	title = {Vers l'infini et au delà},
	booktitle = {ALGOTEL 2020 – 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications},
	abstract = {On considère le problème de l'exploration d'une grille infinie par un nombre fini de robots. Ces robots ont une visibilité finie et exécutent tous le même algorithme de manière synchrone. Les robots ne possèdent pas de système de coor-données commun, mais sont chiraux (ils savent distinguer leur droite de leur gauche). Les robots possèdent une lumière ayant un nombre fini de couleurs possibles. Misà part cette lumière, les robots n'ont aucune mémoire, aucun moyen de communiquer explicitement et sont anonymes.Évidemment, la couleur de leur lumière est un moyen de se distinguer, pour casser la symétrie et ainsi exécuter des actions différentes. On montre tout d'abord que cinq robots de ce type sont nécessaires et suffisants pour résoudre le problème de l'exploration de la grille infinie. Pour cela, nous prouvons qu'il n'existe pas d'algorithme n'utilisant que quatre robots, quelle que soit leur visibilité (tant qu'elle est finie). Puis nous donnons un algorithme qui fonctionne avec cinq robots, avec des lumières possédant cinq couleurs, et une visibilitéà un saut. Si on se restreintà des robots dont les couleurs ne sont pas modifiables (et toujours avec une visibilitéà un saut), on montre que six robots sont nécessaires et suffisants pour résoudre notre problème.},
	author = {Bramas, Q. and  Devismes, S. and  Lafourcade, P.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02791601},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{dupont_de_dinechin_scaling_up_the_2020_hal-02431273,
	title = {Scaling Up the Memory Interference Analysis for Hard Real-Time Many-Core Systems},
	booktitle = {DATE 2020 - Design, Automation and Test in Europe Conference},
	author = {Dupont de dinechin, M. and  Schuh, M. and  Moy, M. and  Maïza, C.},
	pages = {1-4},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02431273},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{echenim_the_lower_bound_2020_hal-02388028,
	title = {The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions},
	booktitle = {ADSL 2020 - Workshop on Automated Deduction in Separation Logic},
	abstract = {The entailment between separation logic formulae with inductive predicates (also known as symbolic heaps) has been shown to be decidable for a large class of inductive definitions [4]. Recently, a 2EXPTIME algorithm has been proposed [7], however no precise lower bound is known (although a EXPTIME-hard bound for this problem has been established in [5]). In this paper, we show that deciding entailment between predicate atoms is 2EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines [3].},
	author = {Echenim, M. and  Iosif, R. and  Peltier, N.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02388028},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{foughali_a_twostep_hybrid_2020_hal-02949916,
	title = {A Two-Step Hybrid Approach for Verifying Real-Time Robotic Systems},
	booktitle = {2020 IEEE 26th International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA)},
	doi = {10.1109/RTCSA50079.2020.9203687},
	abstract = {Due to the severe consequences of their possible failure, robotic systems must be rigorously verified against (i) behavioral properties, such as safety and (ii) real-time properties, such as schedulability, while taking into account the real hardware (e.g. number of cores) and operating system (e.g. scheduling policy) specificities. Formal verification and schedu-lability analysis are popular approaches that may help with such verification, but suffer from limitations such as scalability issues (for the former) and difficulty to generalize to complex robotic tasks (for the latter), when used independently. In this paper, we propose a two-step, efficient solution that combines both approaches. The first step provides a sufficient condition for the schedulability of hard-real-time tasks in a robotic application. Then, the second step automatically generates a formal model of the application, on which other important properties may be verified formally using statistical model checking. The solution is applied to an autonomous drone case study.},
	author = {Foughali, M.},
	pages = {1-10},
	publisher = {IEEE},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02949916},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{foughali_runtime_verification_of_2020_hal-03093298,
	title = {Runtime Verification of Timed Properties in Autonomous Robots},
	booktitle = {18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)},
	doi = {10.1109/MEMOCODE51338.2020.9315156},
	abstract = {Throughout the last few decades, researchers and practitioners are showing more and more interest in using formal methods in order to predict and prevent software failures in robotic and autonomous systems. However, the applicability of formal methods to such systems is limited due to several factors. For instance, robotic specifications are often non-formal which makes their formalization hard and error prone, and their translation into formal models ad-hoc and non automatic. Furthermore, the complexity and size of robotic applications lead most often to scalability issues with exhaustive techniques such as model checking. In this paper, we investigate the use of runtime verification as an alternative to model checking for the rigorous verification of large robotic systems. To do so, we first develop a sound and automatic translation from the robotic framework GenoM3 to the real-time version of the BIP formal language. Then, we apply the translation to a real-world case study the formal models of which do not scale with model checking, and use the BIP Engine to execute the generated BIP model, verify properties online, and adequately react to their possible violation. The experiments are carried out on a real Robotnik robot and show the efficiency of our approach in verifying timed properties, that is when the amount of time separating events is important.},
	author = {Foughali, M. and  Bensalem, S. and  Combaz, J. and  Ingrand, F.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03093298},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{meslem_on_the_reachable_2020_hal-03035743,
	title = {On the Reachable Set of Uncertain Closed Loop Discrete-Time Linear Systems},
	booktitle = {IFAC WC 2020 - 21st IFAC World Congress},
	url = {https://www.ifac2020.org/},
	abstract = {This work tackles the reachability problem of uncertain discrete-time linear systems controlled by estimated state feedback regulators. First an augmented system is considered in order to include the effect of the estimation error on the behavior of the closed loop system. Then, based on interval analysis, an interval predictor is proposed to compute tight trajectory tubes that contain in a guaranteed way the actual state trajectory of the augmented system. Moreover, under the standard controllability and observability assumptions of linear systems, the convergence of the width of these trajectory tubes is shown.},
	author = {Meslem, N. and  Dang, T.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03035743},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{morice_towards_a_power_2020_hal-02975061,
	title = {Towards A Power Advisor in a Devkit for Internet-of-Things Microcontrollers},
	booktitle = {RAPIDO'2020},
	url = {https://rapidoworkshop.github.io/2020/index.html},
	abstract = {Microcontrollers (MCUs) for the Internet-of-Things (IoT) are powerful and versatile computing platforms, which may be hard to program correctly and efficiently; power performance is particularly important. We inestigate automatic methods to detect software performance anti-patterns for this class of systems, so as to help the software developer with power-related aspects. We use a virtual prototype, i.e., we execute the real object code on a simulated model of the hardware platform, given as a transaction-level model (TLM) augmented with dedicated monitors. We study two cases taken from an industrial example, and show that our method can help detect patterns that would be difficult to detect statically, even when the source code is available, because they involve the state of the hardware and the timing of operations.},
	author = {Morice, V. and  Maraninchi, F. and  Cornet, J.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02975061},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{recoules_et_tina_rustina_2020_cea-04484523,
	title = {Et TINA RUSTINA le lien vers l’assembleur : Etude préliminaire},
	series = {Actes des JFLA 2020},
	booktitle = {Journées Francophones des Langages Applicatifs, 2020},
	abstract = {Le développement en C de logiciels non-critiques utilise régulièrement l’insertion d’assembleur « en ligne », que ce soit pour optimiser certaines opérations ou pour accéder à des primitives systèmes autrement inaccessibles. Celui-ci demande l’écriture de spécifications sous forme de contraintes pour faire le lien entre le langage hôte (C) et le langage assembleur embarqué. Ces spécifications sont ensuite utilisées par le compilateur afin d’insérer aveuglément l’assembleur dans le code émis – la pratique étant d’accorder toute confiance aux dires du programmeur. Pour éviter les erreurs issues de spécifications mal formées, nous proposons RUSTINA, un outil qui permet de vérifier que les spécifications assembleurs correspondent bien à l’implémentation des blocs qu’elles décrivent, ou, dans le cas contraire diagnostiquer ou corriger le problème.},
	author = {Recoules, F. and  Bardin, S. and  Bonichon, R. and  Mounier, L. and  Potet, M.-L.},
	pages = {168-175},
	year = {2020},
	eprinttype={HAL}, eprint = {cea-04484523},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{schuh_a_study_of_2020_hal-03185800,
	title = {A study of predictable execution models implementation for industrial data-flow applications on a multi-core platform with shared banked memory},
	booktitle = {2020 IEEE Real-Time Systems Symposium (RTSS)},
	doi = {10.1109/RTSS49844.2020.00034},
	abstract = {We study the implementation of dataflow applications on multi-core processor with on-chip shared multi-banked memory. Specifically, we consider the Kalray MPPA2 processor and three applications coded using the industrial toolchain SCADE Suite. We focus on the runtime environment assuming global static scheduling, time-triggered and non-preemptive execution of tasks. Our contributions include (i) a technique to implement SCADE applications compliant with execution models inspired by PREMs (PRedictable Execution Models), (ii) an exhaustive comparison of three execution models with and without isolation, and finally (iii) guidelines for predictable implementation of a data-flow application on multi-core processors with shared on-chip memory.},
	author = {Schuh, M. and  Maïza, C. and  Goossens, J. and  Raymond, P. and  Dupont de dinechin, B.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03185800},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{werner_an_endtoend_approach_2020_hal-03248430,
	title = {An End-to-End Approach for Multi-Fault Attack Vulnerability Assessment},
	series = {2020 Workshop on Fault Detection and Tolerance in Cryptography (FDTC)},
	booktitle = {2020 Workshop on Fault Detection and Tolerance in Cryptography (FDTC 2020)},
	url = {https://fdtc.deib.polimi.it/FDTC20/index.html},
	doi = {10.1109/FDTC51366.2020.00009},
	abstract = {Although multi-fault attacks are extremely powerful in defeating sophisticated hardware and software defences, detecting and exploiting such attacks remains a difficult problem, especially without any prior knowledge of the target. Our main contribution is an end-to-end approach for multi-fault attack vulnerability assessment We take advantage of target specific fault models rather than generic fault models to achieve complex multi-fault attacks that can lead to critical vulnerabilities. Target specific fault models are generated thanks to fault models inference process, based on a fault injections simulation and a characterization, in order to elaborate powerful multifault attacks based on different fault models. Combining fault models opens up new possible attack paths and adds flexibility to design fault attacks that adapt to countermeasures. Hence, the direct consequence of the increasing complexity of fault attacks question the effectiveness of software countermeasures based on generic fault models for sensitive applications.},
	author = {Werner, V. and  Maingault, L. and  Potet, M.-L.},
	publisher = {IEEE},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03248430},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{ziat_combination_of_boxes_2019_hal-02457083,
	title = {Combination of Boxes and Polyhedra Abstractions for Constraint Solving},
	volume = {12233},
	series = {Lecture Notes in Computer Science},
	booktitle = {The 8th International Workshop on Numerical and Symbolic Abstract Domains - NSAD 2019},
	doi = {10.1007/978-3-030-54997-8_8},
	abstract = {This paper investigates the use of abstract domains from Abstract Interpretation (AI) in the field of Constraint Programming (CP). CP solvers are generally very efficient on a specific constraint language, but can hardly be extended to tackle more general languages, both in terms of variable representation (discrete or continuous) and constraint type (global, arithmetic, etc.). For instance, linear constraints are usually solved with linear programming techniques, but non-linear ones have to be either linearized, reformulated or sent to an external solver. We approach this problem by adapting to CP a popular domain construction used to combine the power of several analyses in AI: the reduced product. We apply this product on two well-known abstract domains, Boxes and Polyhedra, that we lift to constraint solving. Finally we define general metrics for the quality of the solver results, and present a benchmark accordingly. Experiments show promising results and good performances.},
	author = {Ziat, G. and  Maréchal, A. and  Pelleau, M. and  Miné, A. and  Truchet, C.},
	pages = {119--135},
	publisher = {Springer International Publishing},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02457083},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{altisen_silence_dans_la_2019_hal-02118549,
	title = {Silence dans la forêt !},
	booktitle = {ALGOTEL 2019 - 21èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications},
	abstract = {Nous formalisons des schémas d'algorithmes distribués, classiquement utilisés en autostabilisation, afin d'obtenir des résultats généraux relatifs à leur correction et leur complexité. Précisément, nous étudions une classe d'algorithmes dédiés aux réseaux munis d'un sens de direction décrivant une forêt couvrante. La définition de cette classe est simple au sens où elle est quasi-syntaxique. Tous les algorithmes de cette classe sont (1) autostabilisants et silencieux, et (2) ont un temps de stabilisation à la fois polynomial en mouvements et asymptotiquement optimal en rondes. Pour illustrer la polyvalence de notre méthode, nous passons en revue plusieurs travaux où nos résultats s'appliquent.},
	author = {Altisen, K. and  Devismes, S. and  Durand, A.},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02118549},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v2},
}

@inproceedings{altisen_squeezing_streams_and_2019_hal-02313746,
	title = {Squeezing Streams and Composition of Self-stabilizing Algorithms},
	volume = {LNCS-11535},
	editor= {Jorge A. Pérez and Nobuko Yoshida},
	series = {Formal Techniques for Distributed Objects, Components, and Systems},
	booktitle = {39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)},
	doi = {10.1007/978-3-030-21759-4_2},
	abstract = {Composition is a fundamental tool when dealing with complex systems. We study the hierarchical collateral composition which is used to combine self-stabilizing distributed algorithms. The PADEC library is a framework developed with the Coq proof assistant and dedicated to the certification of self-stabilizing algorithms. We enrich PADEC with the composition operator and a sufficient condition to show its correctness. The formal proof of the condition leads us to develop new tools and methods on potentially infinite streams, these latter ones being used to model the algorithms’ executions. The cornerstone has been the definition of the function which removes duplicates from streams.},
	author = {Altisen, K. and  Corbineau, P. and  Devismes, S.},
	pages = {21-38},
	publisher = {Springer International Publishing},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02313746},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{balabonski_continuous_vs_discrete_2019_hal-02115599,
	title = {Continuous vs. Discrete Asynchronous Moves: A Certified Approach for Mobile Robots},
	volume = {11704},
	editor= {Mohamed Faouzi Atig and Alexander A. Schwarzmann},
	series = {Lecture Notes in Computer Science},
	booktitle = {7th International Conference on NETworked sYStems (NETYS 2019)},
	doi = {10.1007/978-3-030-31277-0_7},
	author = {Balabonski, T. and  Courtieu, P. and  Pelle, R. and  Rieg, L. and  Tixeuil, S. and  Urbain, X.},
	pages = {93-09},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02115599},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{balabonski_manuel_de_savoirprouver_2019_hal-02115611,
	title = {Manuel de savoir-prouver à l’usage des roboteux et des distributeux},
	booktitle = {ALGOTEL 2019 - 21èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications},
	url = {https://www.irit.fr/algotel2019/},
	abstract = {Les essaims de robots mobiles permettent de réaliser des tâches collaboratives complexes par assemblage de tâches plus simples accomplies individuellement par chaque robot. Néanmoins, leur nature massivement distribuée rend la preuve de correction d’un algorithme très difficile. De plus, il existe de nombreuses variantes du modèle en fonction des capacités de perception des robots, de l’espace et de sa topologie, des hypothèses de synchronisation, etc. Nous proposons Pactole, un cadre formel pour l’assistant à la preuve Coq, dans lequel tous ces modèles peuvent être simultanément exprimés. Nous illustrons ce formalisme sur plusieurs études de cas.},
	author = {Balabonski, T. and  Courtieu, P. and  Pelle, R. and  Rieg, L. and  Tixeuil, S. and  Urbain, X.},
	pages = {1-4},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02115611},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{barbot_generation_of_signals_2019_hal-02402402,
	title = {Generation of Signals Under Temporal Constraints for CPS Testing},
	volume = {Lecture Notes in Computer Science},
	series = {NASA Formal Methods NFM 2019, Springer},
	booktitle = {NASA Formal Methods NFM 2019},
	doi = {10.1007/978-3-030-20652-9},
	author = {Barbot, B. and  Basset, N. and  Dang, T.},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02402402},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{boulmé_the_verified_polyhedron_2018_hal-02100006,
	title = {The Verified Polyhedron Library: an overview},
	editor= {Erika Ábrahám and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Tudor Jebelean and Stephen Watt},
	series = {20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing},
	booktitle = {20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)},
	url = {https://synasc.ro/2018/},
	doi = {10.1109/SYNASC.2018.00014},
	abstract = {The Verified Polyhedra Library operates upon a constraint-only representation of convex polyhedra and provides all common operations (image, pre-image, projection, convex hull, widening, inclusion and equality tests.. .). Optionally, the soundness of the results is checked by a layer certified in Coq.},
	author = {Boulmé, S. and  Maréchal, A. and  Monniaux, D. and  Périn, M. and  Yu, H.},
	pages = {9-17},
	publisher = {IEEE Computer Society},
	year = {2018},
	eprinttype={HAL}, eprint = {hal-02100006},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {1},
	HAL_version = {v1},
}

@inproceedings{coti_parallel_parametric_linear_2019_hal-02097321,
	title = {Parallel parametric linear programming solving, and application to polyhedral computations},
	volume = {11540},
	editor= {João M. F. Rodrigues and Pedro J. S. Cardoso and Jânio Monteiro and Roberto Lam and Valeria V. Krzhizhanovskaya and Michael H. Lees and Jack J. Dongarra and Peter M.A. Sloot},
	series = {Computational Science – ICCS},
	booktitle = {International conference on computational science},
	url = {https://www.iccs-meeting.org/iccs2019/},
	doi = {10.1007/978-3-030-22750-0_52},
	abstract = {Parametric linear programming is central in polyhedral computations and in certain control applications. We propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems.},
	author = {Coti, C. and  Monniaux, D. and  Yu, H.},
	pages = {566-572},
	publisher = {Springer},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02097321},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{datta_brief_announcement_analysis_2019_hal-02489447,
	title = {Brief Announcement: Analysis of a Memory-Efficient Self-stabilizing BFS Spanning Tree Construction},
	volume = {11914},
	series = {Lecture Notes in Compter Science},
	booktitle = {21st International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2019)},
	doi = {10.1007/978-3-030-34992-9_8},
	abstract = {We present results on the last topic we collaborate with our late friend, Professor Ajoy Kumar Datta (1958-2019). In this work, we shed new light on a self-stabilizing wave algorithm proposed by Colette Johnen in 1997. This algorithm constructs a BFS spanning tree in any connected rooted network. Nowadays, it is still the best existing self-stabilizing BFS spanning tree construction in terms of memory requirement,(it only requires Θ(1) bits per edge). However, it has been proven assuming a weakly fair daemon. Moreover, its stabilization time was unknown. Here, we study the slightly modified version of this algorithm, still keeping the same memory requirement. We prove the self-stabilization of this variant under the distributed unfair daemon and show a stabilization time in O(D.n^2) rounds, where D is the network diameter and n the number of processes.},
	author = {Datta, A. and  Devismes, S. and  Johnen, C. and  Larmore, L.},
	pages = {99-104},
	publisher = {Sringer Verlag},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02489447},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{devismes_selfstabilizing_distributed_cooperative_2019_hal-02489666,
	title = {Self-Stabilizing Distributed Cooperative Reset},
	booktitle = {2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS)},
	doi = {10.1109/ICDCS.2019.00045},
	author = {Devismes, S. and  Johnen, C.},
	pages = {379-389},
	publisher = {IEEE},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02489666},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{devismes_silent_selfstabilizing_scheme_2019_hal-02127131,
	title = {Silent self-stabilizing scheme for spanning-tree-like constructions},
	series = {Proceedings of the 20th International Conference on Distributed Computing and Networking},
	booktitle = {ICDCN 2019},
	doi = {10.1145/3288599.3288607},
	abstract = {In this paper, we propose a general scheme, called Algorithm $\mathsf_STlC_$, to compute spanning-tree-like data structures on arbitrary networks. $\mathsf_STlC_$ is self-stabilizing and silent and, despite its generality, is also efficient. It is written in the locally shared memory model with composite atomicity assuming the distributed unfair daemon, the weakest scheduling assumption of the model. Its stabilization time is in $n__\texttt_maxCC__$ rounds, where $n__\texttt_maxCC__$ is the maximum number of processes in a connected component. We also exhibit polynomial upper bounds on its stabilization time in steps and process moves holding for large classes of instantiations of Algorithm $\mathsf_STlC_$. We illustrate the versatility of our approach by proposing several such instantiations that efficiently solve classical problems such as leader election, as well as, unconstrained and shortest-path spanning tree constructions.},
	author = {Devismes, S. and  Ilcinkas, D. and  Johnen, C.},
	pages = {158-167},
	publisher = {ACM Press},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02127131},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{dumas_secure_multiparty_matrix_2019_hal-01781554,
	title = {Secure Multi-Party Matrix Multiplication Based on Strassen-Winograd Algorithm},
	volume = {11689},
	editor= {Nuttapong Attrapadung and Takeshi Yagi},
	series = {Lecture Notes in Computer Science},
	booktitle = {The 14th International Workshop on Security (IWSEC 2019)},
	doi = {10.1007/978-3-030-26834-3_5},
	abstract = {This paper presents a secure multiparty computation protocol for the Strassen-Winograd matrix multiplication algorithm. We focus on the setting in which any given player knows only one row (or one block of rows) of both input matrices and learns the corresponding row (or block of rows) of the resulting product matrix. Neither the player initial data, nor the intermediate values, even during the recurrence part of the algorithm, are ever revealed to other players. We use a combination of partial homomorphic encryption schemes and additive masking techniques together with a novel schedule for the location and encryption layout of all intermediate computations to preserve privacy. Compared to state of the art protocols, the asymptotic communication volume of our construction is reduced from O(n^3) to O(n^_2.81_). This improvement in terms of communication volume arises with matrices of dimension as small as n=96 which is confirmed by experiments.},
	author = {Dumas, J.-G. and  Lafourcade, P. and  Fenner, J. and  Lucas, D. and  Orfila, J.-B. and  Pernet, C. and  Puys, M.},
	pages = {67-88},
	publisher = {Springer},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01781554},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v3},
}

@inproceedings{echenim_prenex_separation_logic_2019_hal-02323468,
	title = {Prenex Separation Logic with One Selector Field},
	booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference},
	doi = {10.1007/978-3-030-29026-9_23},
	abstract = {We show that infinite satisfiability can be reduced to finite satisfiabil-ity for all prenex formulas of Separation Logic with k ≥ 1 selector fields (SL k). This fact entails the decidability of the finite and infinite satisfiability problems for the class of prenex formulas of SL 1 , by reduction to the first-order theory of a single unary function symbol and an arbitrary number of unary predicate symbols. We also prove that the complexity of this fragment is not elementary recursive, by reduction from the first-order theory of one unary function symbol. Finally, we prove that the Bernays-Schönfinkel-Ramsey fragment of prenex SL 1 formulas with quantifier prefix in the language ∃ * ∀ * is PSPACE-complete.},
	author = {Echenim, M. and  Iosif, R. and  Peltier, N.},
	pages = {409-427},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02323468},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{echenim_the_bernaysschonfinkelramsey_class_2019_hal-02094154,
	title = {The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains},
	booktitle = {Foundations of Software Science and Computation Structures (FOSSACS) - 22nd International Conference},
	doi = {10.1007/978-3-030-17127-8_14},
	abstract = {This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications , for prenex formulae with quantifier prefix ∃ * ∀ *. In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SL k)]. In contrast to existing work in Separation Logic, in which the universe of possible locations is assumed to be infinite, both finite and infinite universes are considered. We show that, unlike in first-order logic, the (in)finite sat-isfiability problem is undecidable for BSR(SL k). Then we define two non-trivial subsets thereof, that are decidable for finite and infinite satisfiability respectively, by controlling the occurrences of universally quantified variables within the scope of separating implications, as well as the polarity of the occurrences of the latter. Beside the theoretical interest, our work has natural applications in program verification, for checking that constraints on the shape of a data-structure are preserved by a sequence of transformations.},
	author = {Echenim, M. and  Iosif, R. and  Peltier, N.},
	pages = {242-259},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02094154},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{ene_outputsensitive_information_flow_2019_hal-02303984,
	title = {Output-sensitive Information flow analysis},
	volume = {LNCS-11535},
	editor= {Jorge A. Pérez and Nobuko Yoshida},
	series = {Formal Techniques for Distributed Objects, Components, and Systems},
	booktitle = {39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)},
	doi = {10.1007/978-3-030-21759-4_6},
	abstract = {Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation. We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive non-interference. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong in practice. In order to take into account public outputs we proceed as follows: instead of using complex explicit declassification policies, we partition variables in three sets: input, output and leakage variables. Then, we propose a typing system to statically check that leakage variables do not leak more information about the secret inputs than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect not only to the initial values of input variables (as in classical approaches for noninterference), but taking also into account the final values of output variables. We adapted this approach to LLVM IR and we developed a prototype to verify LLVM implementations.},
	author = {Ene, C. and  Mounier, L. and  Potet, M.-L.},
	pages = {93-110},
	publisher = {Springer International Publishing},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02303984},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{farinier_en_finir_avec_2019_cea-04484565,
	title = {En finir avec les faux positifs grâce à l’exécution symbolique robuste},
	series = {Actes des JFLA 2019},
	booktitle = {JFLA 2019 - Journées Francophones des Langages Applicatifs},
	url = {https://dpt-info.u-strasbg.fr/~magaud/JFLA2019/programme.html},
	abstract = {L’exécution symbolique est une technique de vérification formelle par sous-approximation ayant fait ses preuves en recherche de bogues, notamment grâce à son absence de faux positifs : un bogue trouvé est un bogue réel. Cependant, si cette propriété est vraie dans le cas où l’utilisateur contrôle toutes les entrées du programme, les choses se compliquent quand certaines entrées sont hors de son contrôle, typiquement l’environnement. L’exécution symbolique devient alors fragile dans le sens où elle peut produire des faux positifs. Ce cas se rencontre particulièrement en recherche de vulnérabilités, où les failles cherchées doivent être reproductibles. Dans cet article nous montrons comment l’utilisation de quantificateurs permet de passer du problème de l’accessibilité à celui de l’accessibilité robuste et proposons une modélisation cohérente en tant que sous-approximation. Ces quantificateurs sont ensuite éliminés et les formules obtenues simplifiées afin de limiter au maximum l’impact sur le temps de résolution. Il en résulte ainsi une analyse par exécution symbolique efficace et robuste vis-à-vis de son environnement, réellement exempte de faux positifs},
	author = {Farinier, B. and  Bardin, S. and  Bonichon, R. and  Potet, M.-L.},
	pages = {245-252},
	year = {2019},
	eprinttype={HAL}, eprint = {cea-04484565},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{fradet_certican_a_tool_2019_hal-02119024,
	title = {CertiCAN: A Tool for the Coq Certification of CAN Analysis Results},
	booktitle = {RTAS 2019 - 25th IEEE Real-Time and Embedded Technology and Applications Symposium},
	doi = {10.1109/RTAS.2019.00023},
	abstract = {This paper introduces CertiCAN, a tool produced using the Coq proof assistant for the formal certification of CAN analysis results. Result certification is a process that is lightweight and flexible compared to tool certification, which makes it a practical choice for industrial purposes. The analysis underlying CertiCAN, which is based on a combined use of two well-known CAN analysis techniques, is computationally efficient. Experiments demonstrate that Certi-CAN is faster than the corresponding certified combined analysis. More importantly, it is able to certify the results of RTaW-Pegase, an industrial CAN analysis tool, even for large systems. This result paves the way for a broader acceptance of formal tools for the certification of real-time systems analysis results.},
	author = {Fradet, P. and  Guo, X. and  Monin, J.-F. and  Quinton, S.},
	pages = {1-10},
	publisher = {IEEE},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02119024},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{graillat_response_time_analysis_2019_hal-02320463,
	title = {Response Time Analysis of Dataflow Applications on a Many-Core Processor with Shared-Memory and Network-on-Chip},
	booktitle = {RTNS 2019 - 27th International Conference on Real-Time Networks and Systems},
	doi = {10.1145/3356401.3356416},
	author = {Graillat, A. and  Maiza, C. and  Moy, M. and  Raymond, P. and  Dupont de dinechin, B.},
	pages = {61-69},
	publisher = {ACM},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02320463},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{iosif_alternating_automata_modulo_2019_hal-02387992,
	title = {Alternating Automata Modulo First Order Theories},
	booktitle = {Computer Aided Verification - 31st International Conference},
	doi = {10.1007/978-3-030-25543-5_3},
	abstract = {We introduce first-order alternating automata, a generalization of boolean alternating automata, in which transition rules are described by multisorted first-order formulae, with states and internal variables given by uninterpreted predicate terms. The model is closed under union, intersection and complement, and its emptiness problem is undecidable, even for the simplest data theory of equality. To cope with the undecidability problem, we develop an abstraction refinement semi-algorithm based on lazy annotation of the symbolic execution paths with interpolants, obtained by applying (i) quantifier elimination with witness term generation and (ii) Lyndon interpolation in the quantifier-free theory of the data domain, with uninterpreted predicate symbols. This provides a method for checking inclusion of timed and finite-memory register automata, and emptiness of quantified predicate automata, previously used in the verification of parameter-ized concurrent programs, composed of replicated threads, with shared memory.},
	author = {Iosif, R. and  Xu, X.},
	pages = {43-63},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02387992},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{iosti_eventually_safe_languages_2019_hal-02348828,
	title = {Eventually Safe Languages},
	booktitle = {Developments in Language Theory},
	doi = {10.1007/978-3-030-24886-4_14},
	abstract = {Good-for-Games (GFG) automata constitute a sound alternative to determinism as a way to model specifications in the Church synthesis problem. Typically, inputs for the synthesis problem are in the form of LTL formulas. However, the only known examples where GFG automata present an exponential gap in succinctness compared to deter-ministic ones are not LTL-definable. We show that GFG automata still enjoy exponential succinctness for LTL-definable languages. We introduce a class of properties called "eventually safe" together with a specification language E νTL for this class. We finally give an algorithm to produce a Good-for-Games automaton from any E νTL formula, thereby allowing synthesis for eventually safe properties.},
	author = {Iosti, S. and  Kuperberg, D.},
	pages = {192-205},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02348828},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{recoules_de_l’assembleur_sur_2019_cea-04484567,
	title = {De l’assembleur sur la ligne ? Appelez TInA !},
	series = {Actes des JFLA 2019},
	booktitle = {JFLA 2019 - Journées Francophones des Langages Applicatifs},
	abstract = {Les méthodes formelles appliquées au logiciel ont fait des progrès importants lors des deux dernières décennies. Leur application à l’embarqué est ainsi un succès indéniable. Parmi les prochains défis réside la question de leur application à des domaines moins contraints. Par exemple, le développement en C de logiciels non-critiques utilise régulièrement l’insertion d’assembleur « en ligne », que ce soit pour optimiser certaines opérations ou pour accéder à des primitives systèmes autrement inaccessibles. Ceci empêche complètement l’utilisation des méthodes développés pour le C pur. Nous proposons ici TInA, une méthode générale, automatique, sûre et orientée vérification pour pouvoir porter le code assembleur en ligne vers un code C sémantiquement équivalent, et profiter en retour des analyses pré-existantes pour ce langage. Nos expérimentations sur du code C d’envergure montre la faisabilité et l’intérêt de l’approche.},
	author = {Recoules, F. and  Bardin, S. and  Bonichon, R. and  Mounier, L. and  Potet, M.-L.},
	pages = {209-224},
	year = {2019},
	eprinttype={HAL}, eprint = {cea-04484567},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}

@inproceedings{recoules_get_rid_of_2019_cea-04228170,
	title = {Get rid of inline assembly through verification-oriented lifting},
	series = {ASE '19: Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering},
	booktitle = {34th IEEE/ACM International Conference on Automated Software Engineering},
	url = {https://ieeexplore.ieee.org/document/8952223},
	doi = {10.1109/ASE.2019.00060},
	abstract = {Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in rendering state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, the first automated, generic, verification-friendly and trustworthy lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA.},
	author = {Recoules, F. and  Bardin, S. and  Bonichon, R. and  Mounier, L. and  Potet, M.-L.},
	pages = {577-589},
	year = {2019},
	eprinttype={HAL}, eprint = {cea-04228170},
	peer_reviewing = {1},
	audience = {2},
	proceedings = {1},
	invited_communication = {0},
	HAL_version = {v1},
}
