
@article{altisen_selfstabilizing_synchronous_unison_2024_hal-04580574,
	title = {Self-stabilizing synchronous unison in directed networks},
	volume = {1001},
	issn = {0304-3975},
	doi = {10.1016/J.TCS.2024.114577},
	abstract = {Self-stabilization is a general paradigm that characterizes the ability of a distributed system to recover from transient faults. Since its introduction by Dijkstra in 1974, self-stabilization has been successfully applied to efficiently solve many networking tasks. However, most of the literature focuses on bidirectional networks. Now, in today's networks such as WSNs, some communication channels may be one-way only. Considering such network topologies, a.k.a. directed graphs, makes self-stabilization more complicated, and sometimes even impossible. In this paper, we investigate the gap in terms of requirements and efficiency when considering a directed graph instead of an undirected one as network topology for a self-stabilizing algorithm. Our case study is a variant of a synchronous unison algorithm proposed by Arora et al.; the synchronous unison being a clock synchronization problem.},
	journal = {Theoretical Computer Science},
	author = {Altisen, K. and  Cournier, A. and  Defalque, G. and  Devismes, S.},
	pages = {114577},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04580574},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{aubouin--pairault_comparison_of_multiple_2024_hal-04565805,
	title = {Comparison of multiple Kalman filter and moving horizon estimator for the anesthesia process},
	volume = {136},
	issn = {0959-1524},
	url = {https://www.sciencedirect.com/science/article/abs/pii/S0959152424000192?via\%3Dihub},
	doi = {10.1016/j.jprocont.2024.103179},
	abstract = {In this paper, a new method to estimate the states and the parameters of the anesthesia process is proposed and compared to a Moving Horizon Estimator (MHE) approach. The proposed method makes use of multiple extended Kalman filters (MEKF) where each EKF uses a different set of system parameters whose selection is based on a predictive performance criterion. In view of usage in a closed loop, the comparison between the two methods is based on a metric quantifying the capability of the estimators to predict the future behavior of the system. The metric is also used as a performance measure for tuning the hyperparameters of the estimators. While the results on simulated data are similar, the MEKF method outperforms MHE on clinical data. Tests show that the MEKF method can better predict the future trajectory of the system during the whole induction, on average for all the patients but also for the worst scenario.},
	journal = {Journal of Process Control},
	author = {Aubouin--Pairault, B. and  Fiacchini, M. and  Dang, T.},
	pages = {103179},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04565805},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{aubouin--pairault_databased_modeling_of_2024_hal-04672903,
	title = {Data-based modeling of the Pharmacodynamics for the effect of Propofol and Remifentanil during General Anesthesia},
	volume = {98},
	issn = {1746-8094},
	url = {https://www.sciencedirect.com/science/article/abs/pii/S1746809424007869?via\%3Dihub},
	doi = {10.1016/j.bspc.2024.106728},
	abstract = {Predicting Bispectral Index (BIS) and Mean Arterial Pressure (MAP) during anesthesia is critical for patient safety and effective anesthesia management. Traditional pharmacodynamic response surface models have limitations in accuracy and adaptability. This paper presents a novel approach for predicting BIS and MAP using machine learning techniques. Rather than using standard pharmacodynamic response surface models, a machine learning-based approach is proposed to model the pharmacodynamic. The proposed method considers the state of the standard propofol and remifentanil pharmacokinetic model and the patient information as features to predict the BIS and MAP values. Training and testing are done on a selected subset of the VitalDB dataset (Lee and Jung, 2018) containing 191 different patients. Results demonstrate that the machine learning-based approach outperforms standard pharmacodynamic models in terms of accuracy. Specifically, the Support Vector Regression (SVR) model achieves a Mean Absolute Prediction Error (MDAPE) 32\% smaller than the Eleveld model for BIS prediction. For MAP prediction, the SVR model also demonstrates superior performance with a reduction of 66\% of MDAPE. The proposed method provides similar performance as the deep-learning method (Lee et al., 2018) while keeping a simple structure that may be used in other applications.},
	journal = {Biomedical Signal Processing and Control},
	author = {Aubouin--Pairault, B. and  Fiacchini, M. and  Dang, T.},
	pages = {106728},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04672903},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{aubouin--pairault_online_identification_of_2024_hal-04672940,
	title = {Online identification of pharmacodynamic parameters for closed-loop anesthesia with model predictive control},
	volume = {191},
	issn = {0098-1354},
	url = {https://www.sciencedirect.com/science/article/abs/pii/S0098135424002552?via\%3Dihub},
	doi = {10.1016/j.compchemeng.2024.108837},
	abstract = {In this paper, a controller is proposed to automate the injection of propofol and remifentanil during general anesthesia using bispectral index (BIS) measurement. To handle the parameter uncertainties due to inter- and intra-patient variability, an extended estimator is used coupled with a Model Predictive Controller (MPC). Two methods are considered for the estimator: the first one is a multiple extended Kalman filter (MEKF), and the second is a moving horizon estimator (MHE). The state and parameter estimations are then used in the MPC to compute the next drug rates. The methods are compared with a PID from the literature. The robustness of the controller is evaluated using Monte-Carlo simulations on a wide population, introducing uncertainties in all parts of the model. Results both on the induction and maintenance phases of anesthesia show the potential interest in using this adaptive method to handle parameter uncertainties.},
	journal = {Computers \& Chemical Engineering},
	author = {Aubouin--Pairault, B. and  Fiacchini, M. and  Dang, T.},
	pages = {108837},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04672940},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_rigorous_security_analysis_2024_hal-04549958,
	title = {Rigorous Security Analysis of RabbitMQ Broker with Concurrent Stochastic Games},
	volume = {26},
	issn = {2542-6605},
	url = {https://www.sciencedirect.com/science/article/abs/pii/S2542660524001021?via\%3Dihub},
	doi = {10.1016/j.iot.2024.101161},
	abstract = {Modern Internet of Things architectures encompass various computational logic and communication protocols. However, the security issues inherent in these systems pose significant risks, especially at the device edges. Addressing security threats on the deployed communication edges is imperative to ensure a robust and secure communication system. In this study, we propose an approach that utilizes the Concurrent Stochastic Game model (CSG) to specify the behavior of RabbitMQ Broker in the context of IoT systems precisely while considering potential data corruption attacks. For parametrizable evaluation, these attacks and their frequencies are learned. We implement the CSG model in PRISM games for automated analysis, leveraging reward Probabilistic Alternating Temporal Logic (rPATL) to model security requirements as game goals. Empirical validation of the work is presented via an industrial case study that shows how data corruption attacks can impact the sensed data in water dam infrastructure. This assessment gives valuable insights into the RabbitMQ deployment at the edge.},
	journal = {Internet of Things},
	author = {Baouya, A. and  Hamid, B. and  Gürgen, L. and  Bensalem, S.},
	pages = {101161},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04549958},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{denardi_huff_optimized_coadministration_of_2024_hal-04794828,
	title = {Optimized Coadministration of Propofol and Remifentanil During the Induction Phase of Total Intravenous Anesthesia With Statistical Validation},
	volume = {8},
	doi = {10.1109/LCSYS.2024.3359529},
	journal = {IEEE Control Systems Letters},
	author = {Denardi huff, D. and  Fiacchini, M. and  Dang, T. and  Alamo, T.},
	pages = {193-198},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04794828},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{flipo_le_numerique_face_2024_hal-04682690,
	title = {Le numérique face à ses responsabilités planétaires - Un état des lieux},
	issn = {1776-0860},
	doi = {10.51257/a-v1-ag126},
	abstract = {Cet article se propose de cadrer le problème du déploiement des technologies numériques et de leurs usages, dans leur rapport à leurs implications écologiques. Il montre que le secteur pose et posera toujours plus de choix difficiles, en raison d’une trajectoire peu compatible avec l’objectif de zéro émissions net fixé tant au niveau français qu’européen, et d’une production de déchets mal maîtrisée. Il indique les principales réglementations en vigueur et leurs limites. Il conclut à la nécessité d’une sobriété numérique.},
	journal = {Techniques de l'Ingénieur},
	author = {Flipo, F. and  Combaz, J.},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04682690},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{huang_a_survey_of_2024_hal-04749738,
	title = {A survey of safety and trustworthiness of large language models through the lens of verification and validation},
	volume = {57},
	issn = {0269-2821},
	doi = {10.1007/s10462-024-10824-0},
	abstract = {Abstract Large language models (LLMs) have exploded a new heatwave of AI for their ability to engage end-users in human-level conversations with detailed and articulate answers across many knowledge domains. In response to their fast adoption in many industrial applications, this survey concerns their safety and trustworthiness. First, we review known vulnerabilities and limitations of the LLMs, categorising them into inherent issues, attacks, and unintended bugs. Then, we consider if and how the Verification and Validation (V\&amp;V) techniques, which have been widely developed for traditional software and deep learning models such as convolutional neural networks as independent processes to check the alignment of their implementations against the specifications, can be integrated and further extended throughout the lifecycle of the LLMs to provide rigorous analysis to the safety and trustworthiness of LLMs and their applications. Specifically, we consider four complementary techniques: falsification and evaluation, verification, runtime monitoring, and regulations and ethical use. In total, 370+ references are considered to support the quick understanding of the safety and trustworthiness issues from the perspective of V\&amp;V. While intensive research has been conducted to identify the safety and trustworthiness issues, rigorous yet practical methods are called for to ensure the alignment of LLMs with safety and trustworthiness requirements.},
	journal = {Artificial Intelligence Review},
	author = {Huang, X. and  Ruan, W. and  Huang, W. and  Jin, G. and  Dong, Y. and  Wu, C. and  Bensalem, S. and  Mu, R. and  Qi, Y. and  Zhao, X. and  Cai, K. and  Zhang, Y. and  Wu, S. and  Xu, P. and  Wu, D. and  Freitas, A. and  Mustafa, M.},
	pages = {175},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04749738},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{mambakam_mining_of_extended_2024_hal-04796470,
	title = {Mining of extended signal temporal logic specifications with ParetoLib 2.0},
	volume = {62},
	issn = {0925-9856},
	doi = {10.1007/s10703-024-00453-2},
	abstract = {Abstract Cyber-physical systems are complex environments that combine physical devices (i.e., sensors and actuators) with a software controller. The ubiquity of these systems and dangers associated with their failure require the implementation of mechanisms to monitor, verify and guarantee their correct behaviour. This paper presents ParetoLib 2.0, a Python tool for offline monitoring and specification mining of cyber-physical systems. ParetoLib 2.0 uses signal temporal logic (STL) as the formalism for specifying properties on time series. ParetoLib 2.0 builds upon other tools for evaluating and mining STL expressions, and extends them with new functionalities. ParetoLib 2.0 implements a set of new quantitative operators for trace analysis in STL, a novel mining algorithm and an original graphical user interface. Additionally, the performance is optimised with respect to previous releases of the tool via data-type annotations and multi core support. ParetoLib 2.0 allows the offline verification of STL properties as well as the specification mining of parametric STL templates. Thanks to the implementation of the new quantitative operators for STL, the tool outperforms the expressiveness and capabilities of similar runtime monitors.},
	journal = {Formal Methods in System Design},
	author = {Mambakam, A. and  Requeno jarabo, J. I. and  Bakhirkin, A. and  Basset, N. and  Dang, T.},
	pages = {260-284},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04796470},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{monniaux_pragmatics_of_formally_2024_hal-04643135,
	title = {Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers},
	volume = {26},
	issn = {1433-2779},
	doi = {10.1007/s10009-024-00760-3},
	abstract = {Formally verified compilers and formally verified static analyzers are a solution to the problem that certain industries face when they have to demonstrate to authorities that the object code they run truly corresponds to its source code and that it satisfies certain properties. From a scientific and technological point of view, they are a challenge: not only a number of nontrivial invariants and algorithms must be proved to be correct, but also the implementation must be reasonably effective so that the tools operate within reasonable time. Many optimizations in compilers rely on static analysis, and thus a formally verified compiler entails formally verified static analyses. In this article, we explain some difficulties, possible solutions, design choices and trade-offs pertaining to verified static analysis, in particular when the solution of the analysis is expressed as some form of tree, map or set.},
	journal = {International Journal on Software Tools for Technology Transfer},
	author = {Monniaux, D.},
	pages = {463-477},
	year = {2024},
	eprinttype={HAL}, eprint = {hal-04643135},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{altisen_selfstabilizing_systems_in_2023_hal-04109662,
	title = {Self-stabilizing Systems in Spite of High Dynamics},
	issn = {0304-3975},
	doi = {10.1016/j.tcs.2023.113966},
	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 TCB(Δ) of TVGs with temporal diameter bounded by Δ, the class TCQ(Δ) of TVGs with temporal diameter quasi-bounded by Δ, and the class TCR of TVGs with recurrent connectivity only, where TCB(Δ)⊆TCQ(Δ)⊆TCR. 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 central. Our results reveal that, despite the existence of unique process identifiers, any deterministic self-stabilizing leader election algorithm working on the class TCQ(Δ) or TCR 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 Classes TCB(Δ), TCQ(Δ), and TCR, respectively. Our algorithm for TCB(Δ) stabilizes in at most 3Δ rounds. However, we show that stabilization time cannot be bounded for the leader election problem in TCQ(Δ) and TCR. Nevertheless, we circumvent this issue by showing that our solutions are speculative in the sense that their stabilization time in TCB(Δ) (⊆TCQ(Δ)⊆TCR) is O(Δ) rounds.},
	journal = {Theoretical Computer Science},
	author = {Altisen, K. and  Devismes, S. and  Durand, A. and  Johnen, C. and  Petit, F.},
	pages = {113966},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04109662},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{altisen_sasa__a_2023_hal-04186596,
	title = {sasa : a SimulAtor of Self-stabilizing Algorithms},
	volume = {66},
	issn = {0010-4620},
	doi = {10.1093/comjnl/bxab196},
	abstract = {In this paper, we present sasa, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. sasa is implemented as a faithful representation of the atomic-state model (also called the locally shared memory model with composite atomicity). This model is the most commonly used one in the self-stabilizing area to prove both the correct operation of self-stabilizing algorithms and complexity bounds on them. sasa encompasses all features necessary to debug, test and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Properties of algorithms can be checked using formal test oracles. The sasa distribution also provides several facilities to easily achieve (batch-mode) simulation campaigns. We show that the lightweight design of sasa allows to efficiently perform huge such campaigns. Following a modular approach, we have aimed at relying as much as possible the design of sasa on existing tools, including ocaml, dot and several tools developed in the Synchrone Group of the VERIMAG laboratory.},
	journal = {The Computer Journal},
	author = {Altisen, K. and  Devismes, S. and  Jahier, E.},
	pages = {796-814},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04186596},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{altmeyer_from_fmtv_to_2023_hal-04254710,
	title = {From FMTV to WATERS: Lessons Learned from the First Verification Challenge at ECRTS (Artifact)},
	volume = {9},
	issn = {2509-8195},
	url = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.1.4},
	doi = {10.4230/DARTS.9.1.4},
	abstract = {We propose here solutions to the FMTV 2015 challenge of a distributed video processing system using four different formalisms, as well as the description of the challenge itself. This artifact contains several solutions to various subchallenges, and instructions and scripts to reproduce these results smoothly.},
	journal = {Dagstuhl Artifacts Series},
	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.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04254710},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{aubouin--pairault_pas_a_python_2023_hal-04183029,
	title = {PAS: a Python Anesthesia Simulator for drug control},
	volume = {8},
	issn = {2475-9066},
	doi = {10.21105/joss.05480},
	abstract = {The Python Anesthesia Simulator (PAS) models the effect of drugs on physiological variables during total intravenous anesthesia. It is particularly dedicated to the control community, to be used as a benchmark for the design of multidrug controllers. The available drugs are propofol, remifentanil, and norepinephrine, the outputs are the bispectral index (BIS), mean arterial pressure (MAP), cardiac output (CO), and tolerance of laryngoscopy (TOL). PAS includes different well-known models along with their uncertainties to simulate inter-patient variability. Blood loss can also be simulated to assess the controller's performance in a shock scenario. Finally, PAS includes standard disturbance profiles and metric computation to facilitate the evaluation of the controller's performance. The statement of need of this package is first discussed; then some pieces of information about the programmed models are provided to the reader. The future developments of the package are discussed at the end.},
	journal = {Journal of Open Source Software},
	author = {Aubouin--Pairault, B. and  Dang, T. and  Fiacchini, M.},
	pages = {5480},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04183029},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_toward_a_contextdriven_2023_hal-04108274,
	title = {Toward a context-driven deployment optimization for embedded systems: a product line approach},
	volume = {79},
	issn = {0920-8542},
	doi = {10.1007/s11227-022-04741-8},
	abstract = {Producing a large family of resource-constrained multi-processing systems on chips (MPSoC) is challenging, and the existing techniques are generally geared toward a single product. When they are leveraged for a variety of products, they are expensive and complex. Further in the industry, a considerable lack of analysis support at the architectural level induces a strong dependency on the experiences and preferences of the designer. This paper proposes a formal foundation and analysis of MPSoC product lines based on a featured transition system (FTS) to express the variety of products. First, features diagrams are selected to model MPSoC product lines, which facilitate capturing its semantics as FTS. To this end, the probabilistic model checker verifies the resulting FTS that is decorated with tasks characteristics and processors’ failure probability. The experimental results indicate that the formal approach offers quantitative results on the relevant product that optimizes resource usage when exploring the product family.},
	journal = {Journal of Supercomputing},
	author = {Baouya, A. and  Ait mohamed, O. and  Ouchani, S.},
	pages = {2180-2211},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04108274},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{bozga_correct_by_design_2023_hal-04578203,
	title = {Correct by design coordination of autonomous driving systems},
	volume = {25},
	issn = {1433-2779},
	doi = {10.1007/S10009-023-00723-0},
	abstract = {The paper proposes a method for the correct by design coordination of autonomous driving systems (ADS). It builds on previous results on collision avoidance policies and the modeling of ADS by combining descriptions of their static environment in the form of maps, and the dynamic behavior of their vehicles. An ADS is modeled as a dynamic system involving a set of vehicles coordinated by a Runtime that based on vehicle positions on a map and their kinetic attributes, computes free spaces for each vehicle. Vehicles are bounded to move within the corresponding allocated free spaces. We provide a correct by design safe control policy for an ADS, if its vehicles and the Runtime respect corresponding assume-guarantee contracts. The result is established by showing that the composition of assume-guarantee contracts is an inductive invariant that entails ADS safety. We show that it is practically possible to define speed control policies for vehicles that comply with their contracts. Furthermore, we show that traffic rules can be specified in a linear-time temporal logic as a class of formulas that constrain vehicle speeds. The main result is that, given a set of traffic rules, it is possible to derive free-space policies of the Runtime such that the resulting system behavior is safe by design with respect to the rules.},
	journal = {International Journal on Software Tools for Technology Transfer},
	author = {Bozga, M. and  Sifakis, J.},
	pages = {625-639},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04578203},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{bozga_verification_of_componentbased_2023_hal-04263754,
	title = {Verification of component-based systems with recursive architectures},
	volume = {940},
	issn = {0304-3975},
	doi = {10.1016/j.tcs.2022.10.022},
	abstract = {We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. 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, thus reducing a verification problem to checking satisfiability of a WSκS formula.},
	journal = {Theoretical Computer Science},
	author = {Bozga, M. and  Iosif, R. and  Sifakis, J.},
	pages = {146-175},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04263754},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{bozga_verification_of_componentbased_2023_hal-04106065,
	title = {Verification of component-based systems with recursive architectures},
	volume = {940, Part B},
	issn = {0304-3975},
	doi = {10.1016/j.tcs.2022.10.022},
	abstract = {We study a sound verification method for parametric component-based systems. The method uses a resource logic, a new formal specification language for distributed systems consisting of a finite yet unbounded number of components. The logic allows the description of architecture configurations coordinating instances of a finite number of types of components, by means of inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. For parametric systems specified in this logic, we show that decision problems such as reaching deadlock or violating critical section are undecidable, in general. Despite this negative result, we provide for these decision problems practical semi-algorithms relying on the automatic synthesis of structural invariants allowing the proof of general safety properties. 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, thus reducing a verification problem to checking satisfiability of a WSκS formula.},
	journal = {Theoretical Computer Science},
	author = {Bozga, M. and  Iosif, R. and  Sifakis, J.},
	pages = {146-175},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04106065},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{gourdin_formally_verifying_optimizations_2023_hal-04102940,
	title = {Formally Verifying Optimizations with Block Simulations},
	volume = {7},
	issn = {2475-1421},
	doi = {10.1145/3622799},
	abstract = {CompCert (ACM Software System Award 2021) is the first industrial-strength compiler with a mechanically checked proof of correctness. Yet, CompCert remains a moderately optimizing C compiler. Indeed, some optimizations of "gcc-O1" such as Lazy Code Motion (LCM) or Strength Reduction (SR) were still missing: developing these efficient optimizations together with their formal proofs remained a challenge. Cyril Six et al. have developed efficient formally verified translation validators for certifying the results of superblock schedulers and peephole optimizations. We revisit and generalize their approach into a framework (integrated into CompCert) able to validate many more optimizations: an enhanced superblock scheduler, but also Dead Code Elimination (DCE), Constant Propagation (CP), and more noticeably, LCM and SR. In contrast to other approaches to translation validation, we co-design our untrusted optimizations and their validators. Our optimizations provide hints, in the forms of invariants or CFG morphisms, that help keep the formally verified validators both simple and efficient. Such designs seem applicable beyond CompCert.},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Gourdin, L. and  Bonneau, B. and  Boulmé, S. and  Monniaux, D. and  Bérard, A.},
	pages = {59-88},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04102940},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v3},
}

@article{iosif_expressiveness_results_for_2023_hal-04263750,
	title = {Expressiveness Results for an Inductive Logic of Separated Relations},
	series = {34th International Conference on Concurrency Theory (CONCUR 2023)},
	doi = {10.4230/LIPIcs.CONCUR.2023.20},
	abstract = {In this paper we study a Separation Logic of Relations (SLR) and compare its expressiveness to (Monadic) Second Order Logic [(M)SO]. SLR is based on the well-known Symbolic Heap fragment of Separation Logic, whose formulæare composed of points-to assertions, inductively defined predicates, with the separating conjunction as the only logical connective. SLR generalizes the Symbolic Heap fragment by supporting general relational atoms, instead of only points-to assertions. In this paper, we restrict ourselves to finite relational structures, and hence only consider Weak (M)SO, where quantification ranges over finite sets. Our main results are that SLR and MSO are incomparable on structures of unbounded treewidth, while SLR can be embedded in SO in general. Furthermore, MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter and all vertices attached to some hyperedge belong to the interpretation of a fixed unary relation symbol. We also discuss the problem of identifying a fragment of SLR that is equivalent to MSO over models of bounded treewidth.},
	journal = {Leibniz International Proceedings in Informatics},
	author = {Iosif, R. and  Zuleger, F.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04263750},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{lacombe_combining_static_analysis_2023_hal-04016189,
	title = {Combining static analysis and dynamic symbolic execution in a toolchain to detect fault injection vulnerabilities},
	issn = {2190-8508},
	doi = {10.1007/s13389-023-00310-8},
	abstract = {Certification through auditing allows to ensure that critical embedded systems are secure. This entails reviewing their critical components and checking for dangerous execution paths. This latter task requires the use of specialized tools which allow to explore and replay executions but are also difficult to use effectively within the context of the audit, where time and knowledge of the code are limited. Fault analysis is especially tricky as the attacker may actively influence execution, rendering some common methods unusable and increasing the number of possible execution paths exponentially. In this work, we present a new method which mitigates these issues by reducing the number of fault injection points considered to only the most relevant ones relatively to some security properties. We use fast and robust static analysis to detect injection points and assert their impactfulness. A more precise dynamic/symbolic method is then employed to validate attack paths. This way the insight required to find attacks is reduced and dynamic methods can better scale to realistically sized programs. Our method is implemented into a toolchain based on Frama-C and KLEE and validated on WooKey, a case-study proposed by the National Cybersecurity Agency of France.},
	journal = {Journal of Cryptographic Engineering},
	author = {Lacombe, G. and  Feliot, D. and  Boespflug, E. and  Potet, M.-L.},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04016189},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{mediouni_modelbased_design_of_2023_hal-04749757,
	title = {Model-based design of resilient systems using quantitative risk assessment},
	volume = {20},
	issn = {1614-5046},
	doi = {10.1007/s11334-023-00527-0},
	journal = {Innovations in Systems and Software Engineering},
	author = {Mediouni, B. L. and  Dragomir, I. and  Nouri, A. and  Bensalem, S.},
	pages = {3-16},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04749757},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{moussa_databased_extended_moving_2023_hal-04150872,
	title = {Data-based Extended Moving Horizon Estimation for MISO Anesthesia Dynamics},
	volume = {7},
	url = {https://ieeexplore.ieee.org/document/10171227},
	doi = {10.1109/lcsys.2023.3291665},
	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].},
	journal = {IEEE Control Systems Letters},
	author = {Moussa, K. and  Aubouin--Pairault, B. and  Alamir, M. and  Dang, T.},
	pages = {3054-3059},
	year = {2023},
	eprinttype={HAL}, eprint = {hal-04150872},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v3},
}

@article{adimoolam_safety_verification_of_2022_hal-03477894,
	title = {Safety Verification of Networked Control Systems by Complex Zonotopes},
	volume = {8},
	issn = {2199-2002},
	doi = {10.4230/LITES.8.2.1},
	abstract = {Networked control systems (NCS) are widely used in real world applications because of their advantages, such as remote operability and reduced installation costs. However, they are prone to various inaccuracies in execution like delays, packet dropouts, inaccurate sensing and quantization errors. To ensure safety of NCS, their models have to be verified under the consideration of aforementioned uncertainties. In this paper, we tackle the problem of verifying safety of models of NCS under uncertain sampling time, inaccurate output measurement or estimation, and unknown disturbance input. Unbounded-time safety verification requires approximation of reachable sets by invariants, whose computation involves set operations. For uncertain linear dynamics, two important set operations for invariant computation are linear transformation and Minkowski sum operations. Zono-topes have the advantage that linear transformation and Minkowski sum operations can be efficiently approximated. However, they can not encode directions of convergence of trajectories along complex eigenvectors, which is closely related to encoding invariants. Therefore, we extend zonotopes to the complex valued domain by a representation called complex zonotope, which can capture contraction along complex eigenvectors for determining invariants. We prove a related mathematical result that in case of accurate feedback sampling, a complex zonotope will represent an invariant for a stable NCS. In addition, we propose an algorithm to verify the general case based on complex zonotopes, when there is uncertainty in sampling time and in input. We demonstrate the efficiency of our algorithm on benchmark examples and compare it with a stateof-the-art verification tool.},
	journal = {Leibniz Transactions on Embedded Systems},
	author = {Adimoolam, S. A. and  Dang, T. and  Adimoolam, A.},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03477894},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{ahrens_local_reasoning_about_2022_hal-03418999,
	title = {Local Reasoning about Parameterized Reconfigurable Distributed Systems},
	volume = {6},
	series = {Issue OOPSLA2},
	issn = {2475-1421},
	url = {ACM},
	doi = {10.1145/3563293},
	abstract = {This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs delete or create interactions or components while the system components change state according to their local behaviour. Our proof calculus uses a configuration logic that supports local reasoning and that relies on inductive predicates to describe distributed systems with an unbounded number of components. The validity of reconfiguration programs relies on havoc invariants, assertions about the ongoing interactions in the system. We present a proof system for such invariants in an assume/rely-guarantee style. We illustrate the feasibility of our approach by proving the correctness of self-adjustable tree architectures and provide tight complexity bounds for entailment checking in the configuration logic.},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Ahrens, E. and  Bozga, M. and  Iosif, R. and  Katoen, J.-P.},
	pages = {145–174},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03418999},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v2},
}

@article{altisen_certification_of_an_2022_hal-03862272,
	title = {Certification of an exact worst-case self-stabilization time},
	volume = {941},
	issn = {0304-3975},
	doi = {10.1016/j.tcs.2022.11.019},
	journal = {Theoretical Computer Science},
	author = {Altisen, K. and  Corbineau, P. and  Devismes, S.},
	pages = {262-277},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03862272},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_generation_and_verification_2022_hal-03762515,
	title = {Generation and verification of learned stochastic automata using k-NN and statistical model checking},
	volume = {52},
	issn = {0924-669X},
	doi = {10.1007/s10489-021-02884-4},
	abstract = {Deriving an accurate behavior model from historical data of a black box for verification and feature forecasting is seen by industry as a challenging issue especially for a large featured dataset. This paper focuses on an alternative approach where stochastic automata can be learned from time-series observations captured from a set of deployed sensors. The main advantage offered by such techniques is that they enable analysis and forecasting from a formal model instead of traditional learning methods. We perform statistical model checking to analyze the learned automata by expressing temporal properties. For this purpose, we consider a critical water infrastructure that provides a scenario based on a set of input and output values of heterogeneous sensors to regulate the dam spill gates. The method derives a consistent approximate model with traces collected over thirty years. The experiments show that the model provides not only an approximation of the desired output of a feature value but, also, forecasts the ebb and flow of the sensed data.},
	journal = {Applied Intelligence},
	author = {Baouya, A. and  Chehida, S. and  Ouchani, S. and  Bensalem, S. and  Bozga, M.},
	pages = {8874-8894},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03762515},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_generation_and_verification_2022_hal-04094178,
	title = {Generation and verification of learned stochastic automata using k-NN and statistical model checking},
	volume = {52},
	issn = {0924-669X},
	doi = {10.1007/s10489-021-02884-4},
	abstract = {Deriving an accurate behavior model from historical data of a black box for verification and feature forecasting is seen by industry as a challenging issue especially for a large featured dataset. This paper focuses on an alternative approach where stochastic automata can be learned from time-series observations captured from a set of deployed sensors. The main advantage offered by such techniques is that they enable analysis and forecasting from a formal model instead of traditional learning methods. We perform statistical model checking to analyze the learned automata by expressing temporal properties. For this purpose, we consider a critical water infrastructure that provides a scenario based on a set of input and output values of heterogeneous sensors to regulate the dam spill gates. The method derives a consistent approximate model with traces collected over thirty years. The experiments show that the model provides not only an approximation of the desired output of a feature value but, also, forecasts the ebb and flow of the sensed data.},
	journal = {Applied Intelligence},
	author = {Baouya, A. and  Chehida, S. and  Ouchani, S. and  Bensalem, S. and  Bozga, M.},
	pages = {8874-8894},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-04094178},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_toward_a_contextdriven_2022_hal-03762514,
	title = {Toward a context-driven deployment optimization for embedded systems: a product line approach},
	issn = {0920-8542},
	doi = {10.1007/s11227-022-04741-8},
	journal = {Journal of Supercomputing},
	author = {Baouya, A. and  Ait mohamed, O. and  Ouchani, S.},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03762514},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{casagrande_parameter_synthesis_of_2022_hal-03875928,
	title = {Parameter synthesis of polynomial dynamical systems},
	volume = {289},
	issn = {0890-5401},
	doi = {10.1016/j.ic.2022.104941},
	abstract = {Parametric dynamical systems emerge as a natural formalism for modeling natural and engineered systems ranging from biology, epidemiology, and medicine to cyber-physics. Parameter tuning is a complex task which, in many cases, is performed exploiting heavy simulations that have high computational complexity and do not ensure the correctness of the synthesized systems. In this manuscript, we consider the problem of parameter synthesis for discrete-time polynomial systems. We propose a formal method based on Bernstein coefficients that allows refining the set of parameters according to a temporal specification defined as a Signal Temporal Logic formula. We prove that the synthesized system is correct with respect to the specification and we demonstrate the scalability of the approach by implementing it in the C++ library Sapo, also available within a stand-alone application and as a web application. Finally, we illustrate the tool usage and the interface through a simple yet realistic epidemiological model and consider an intriguing application enhancing the accuracy of the verification of neural networks.},
	journal = {Information and Computation},
	author = {Casagrande, A. and  Dang, T. and  Dorigo, L. and  Dreossi, T. and  Piazza, C. and  Pippia, E.},
	pages = {104941},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03875928},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{courtieu_swarms_of_mobile_2022_hal-03901898,
	title = {Swarms of Mobile Robots: Towards Versatility with Safety},
	volume = {8},
	series = {Special Issue on Distributed Hybrid Systems},
	issn = {2199-2002},
	doi = {10.4230/LITES.8.2.2},
	abstract = {We present Pactole, a formal framework to design and prove the correctness of protocols (or the impossibility of their existence) that target mobile robotic swarms. Unlike previous approaches, our methodology unifies in a single formalism the execution model, the problem specification, the protocol, and its proof of correctness. The Pactole framework makes use of the Coq proof assistant, and is specially targeted at protocol designers and problem specifiers, so that a common unambiguous language is used from the very early stages of protocol development. We stress the underlying framework design principles to enable high expressivity and modularity, and provide concrete examples about how the Pactole framework can be used to tackle actual problems, some previously addressed by the Distributed Computing community, but also new problems, while being certified correct.},
	journal = {Leibniz Transactions on Embedded Systems},
	author = {Courtieu, P. and  Rieg, L. and  Tixeuil, S. and  Urbain, X.},
	pages = {02:1–02:36},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03901898},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{echenim_entailment_is_undecidable_2022_hal-03416093,
	title = {Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules},
	volume = {173},
	issn = {0020-0190},
	doi = {10.1016/j.ipl.2021.106169},
	abstract = {Entailment is undecidable in general for Separation (SL) Logic formulae with inductive definitions, but it has been shown to be decidable [1] if the inductive rules satisfy three conditions, namely progress, connectivity and establishment. We show that entailment is undecidable if the latter condition is dropped, thus drawing a much clearer frontier for (un)decidability.},
	journal = {Information Processing Letters},
	author = {Echenim, M. and  Iosif, R. and  Peltier, N.},
	pages = {106169},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03416093},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{ligozat_unraveling_the_hidden_2022_hal-03650884,
	title = {Unraveling the Hidden Environmental Impacts of AI Solutions for Environment Life Cycle Assessment of AI Solutions},
	volume = {14},
	issn = {2071-1050},
	doi = {10.3390/su14095172},
	abstract = {In the past ten years, artificial intelligence has encountered such dramatic progress that it is now seen as a tool of choice to solve environmental issues and, in the first place, greenhouse gas emissions (GHG). At the same time, the deep learning community began to realize that training models with more and more parameters require a lot of energy and, as a consequence, GHG emissions. To our knowledge, questioning the complete net environmental impacts of AI solutions for the environment (AI for Green) and not only GHG, has never been addressed directly. In this article, we propose to study the possible negative impacts of AI for Green. First, we review the different types of AI impacts; then, we present the different methodologies used to assess those impacts and show how to apply life cycle assessment to AI services. Finally, we discuss how to assess the environmental usefulness of a general AI service and point out the limitations of existing work in AI for Green.},
	journal = {Sustainability},
	author = {Ligozat, A.-L. and  Lefèvre, J. and  Bugeau, A. and  Combaz, J.},
	pages = {5172},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03650884},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{maraninchi_let_us_not_2022_hal-03766614,
	title = {Let us not put all our eggs in one basket},
	volume = {65},
	issn = {0001-0782},
	doi = {10.1145/3528088},
	abstract = {Toward new research directions in computer science.},
	journal = {Communications of the ACM},
	author = {Maraninchi, F.},
	pages = {35-37},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03766614},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{monniaux_formally_verified_loopinvariant_2022_hal-03628646,
	title = {Formally Verified Loop-Invariant Code Motion and Assorted Optimizations},
	volume = {22},
	issn = {1539-9087},
	doi = {10.1145/3529507},
	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.},
	journal = {ACM Transactions on Embedded Computing Systems (TECS)},
	author = {Monniaux, D. and  Six, C.},
	pages = {\#3 1-27},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03628646},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{monniaux_the_complexity_gap_2022_hal-03545774,
	title = {The complexity gap in the static analysis of cache accesses grows if procedure calls are added},
	volume = {59},
	issn = {0925-9856},
	doi = {10.1007/s10703-022-00392-w},
	abstract = {The static analysis of cache accesses consists in correctly predicting which accesses are hits or misses. While there exist good exact and approximate analyses for caches implementing the least recently used (LRU) replacement policy, such analyses were harder to find for other replacement policies. A theoretical explanation was found: for an appropriate setting of analysis over control-flow graphs, cache analysis is PSPACE-complete for all common replacement policies (FIFO, PLRU, NMRU) except for LRU, for which it is only NP-complete. In this paper, we show that if procedure calls are added to the control flow, then the gap widens: analysis remains NP-complete for LRU, but becomes EXPTIME-complete for the three other policies. For this, we improve on earlier results on the complexity of reachability problems on Boolean programs with procedure calls. In addition, for the LRU policy we derive a backtracking algorithm as well as an approach for using it as a last resort after other analyses have failed to conclude.},
	journal = {Formal Methods in System Design},
	author = {Monniaux, D.},
	pages = {1-20},
	year = {2022},
	eprinttype={HAL}, eprint = {hal-03545774},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{andré_parametric_analyses_of_2021_hal-03483440,
	title = {Parametric Analyses of Attack-fault Trees},
	volume = {182},
	issn = {0169-2968},
	doi = {10.3233/fi-2021-2066},
	abstract = {Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e., absence of unintentional failures) and security (i.e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to consider these problems is attack trees, a treebased formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parameterize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Moreover, we add the possibility to define countermeasures. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient countermeasure .},
	journal = {Fundamenta Informaticae},
	author = {André, É. and  Lime, D. and  Ramparison, M. and  Stoelinga, M.},
	pages = {69 - 94},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03483440},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{andré_parametric_updates_in_2021_hal-03340905,
	title = {Parametric updates in parametric timed automata},
	volume = {17},
	url = {https://lmcs.episciences.org/7470},
	doi = {10.23638/LMCS-17(2:13)2021},
	abstract = {We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.},
	journal = {Logical Methods in Computer Science},
	author = {André, É. and  Lime, D. and  Ramparison, M.},
	pages = {13:1-13:67},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03340905},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_reliabilitydriven_automotive_software_2021_hal-04094152,
	title = {Reliability-driven Automotive Software Deployment based on a Parametrizable Probabilistic Model Checking},
	volume = {174},
	issn = {0957-4174},
	doi = {10.1016/j.eswa.2021.114572},
	journal = {Expert Systems with Applications},
	author = {Baouya, A. and  Mohamed, O. A. and  Ouchani, S. and  Bennouar, D.},
	pages = {114572},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-04094152},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{baouya_reliabilitydriven_automotive_software_2021_hal-03112932,
	title = {Reliability-driven Automotive Software Deployment based on a Parametrizable Probabilistic Model Checking},
	issn = {0957-4174},
	doi = {10.1016/j.eswa.2021.114572},
	journal = {Expert Systems with Applications},
	author = {Baouya, A. and  Mohamed, O. A. and  Ouchani, S. and  Bennouar, D.},
	pages = {114572},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03112932},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{bliudze_on_methods_and_2021_hal-03720402,
	title = {On methods and tools for rigorous system design},
	volume = {23},
	issn = {1433-2779},
	doi = {10.1007/s10009-021-00632-0},
	abstract = {Full a posteriori verification of the correctness of modern software systems is practically infeasible due to the sheer complexity resulting from their intrinsic concurrent nature. An alternative approach consists of ensuring correctness by construction. We discuss the Rigorous System Design (RSD) approach, which relies on a sequence of semantics-preserving transformations to obtain an implementation of the system from a high-level model while preserving all the properties established along the way. In particular, we highlight some of the key requirements for the feasibility of such an approach, namely availability of (1) methods and tools for the design of correct-by-construction high-level models and (2) definition and proof of the validity of suitable domain-specific abstractions. We summarise the results of the extended versions of seven papers selected among those presented at the 1st and the 2nd International Workshops on Methods and Tools for Rigorous System Design (MeTRiD 2018–2019), indicating how they contribute to the advancement of the RSD approach.},
	journal = {International Journal on Software Tools for Technology Transfer},
	author = {Bliudze, S. and  Katsaros, P. and  Bensalem, S. and  Wirsing, M.},
	pages = {679-684},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03720402},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{chehida_learning_and_analysis_2021_hal-03265797,
	title = {Learning and analysis of sensors behavior in IoT systems using statistical model checking},
	issn = {0963-9314},
	doi = {10.1007/s11219-021-09559-w},
	journal = {Software Quality Journal},
	author = {Chehida, S. and  Baouya, A. and  Bensalem, S. and  Bozga, M.},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-03265797},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{coti_a_taskbased_approach_2021_hal-02951016,
	title = {A task-based approach to parallel parametric linear programming solving, and application to polyhedral computations},
	volume = {33},
	issn = {1532-0634},
	doi = {10.1002/cpe.6050},
	abstract = {Parametric linear programming is a central operation for polyhedral computations, as well as in certain control applications. Here we propose a task-based scheme for parallelizing it, with quasi-linear speedup over large problems. This type of parallel applications is challenging, because several tasks might be computing the same region. In this paper, we are presenting the algorithm itself with a parallel redundancy elimination algorithm, and conducting a thorough performance analysis.},
	journal = {Concurrency and Computation: Practice and Experience},
	author = {Coti, C. and  Monniaux, D. and  Yu, H.},
	pages = {e6050},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-02951016},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{devismes_terminating_exploration_of_2021_hal-02363013,
	title = {Terminating Exploration Of A Grid By An Optimal Number Of Asynchronous Oblivious Robots},
	volume = {64},
	series = {The Computer Journal},
	issn = {0010-4620},
	doi = {10.1093/comjnl/bxz166},
	abstract = {We consider swarms of asynchronous oblivious robots evolving into an anonymous grid-shaped network. In this context, we investigate optimal (w.r.t. the number of robots) deterministic solutions for the terminating exploration problem. We first show lower bounds in the semi-synchronous model. Precisely, we show that at least three robots are required to explore any grid of at least three nodes, even in the probabilistic case. Then, we show that at least four (resp. five) robots are necessary to deterministically explore a (2,2)-Grid (resp. a (3,3)-Grid). We then propose deterministic algorithms in the asynchronous model. This latter being strictly weakest than the semi-synchronous model, all the aforementioned bounds still hold in that context. Our algorithms actually exhibit the optimal number of robots that is necessary to explore a given grid. Overall, our results show that except in two particular cases, three robots are necessary and sufficient to deterministically explore a grid of at least three nodes and then terminate. The optimal number of robots for the two remaining cases is four for the (2,2)-Grid and five for the (3,3)-Grid, respectively.},
	journal = {The Computer Journal},
	author = {Devismes, S. and  Lamani, A. and  Petit, F. and  Raymond, P. and  Tixeuil, S.},
	pages = {132-154},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-02363013},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{el_ballouli_programming_dynamic_reconfigurable_2021_hal-04106085,
	title = {Programming dynamic reconfigurable systems},
	volume = {23},
	issn = {1433-2779},
	doi = {10.1007/s10009-020-00596-7},
	abstract = {DR-BIP is an extension of the BIP component framework intended for programming reconfigurable systems encompassing various aspects of dynamism. It relies on architectural motifs to structure the architecture of a system and to coordinate its reconfiguration at runtime. An architectural motif defines a set of interacting components that evolve according to reconfiguration rules. With DR-BIP, the dynamism can be captured as the interplay of dynamic changes in three independent directions 1) the organization of interactions between instances of components in a given configuration; 2) the reconfiguration mechanisms allowing creation/deletion of components and management of their interaction according to a given architectural motif; 3) the migration of components between predefined architectural motifs which characterizes dynamic execution environments. The paper lays down the formal foundation of DR-BIP, illustrates its expressiveness on few examples and discusses avenues for dynamic reconfigurable system design.},
	journal = {International Journal on Software Tools for Technology Transfer},
	author = {El ballouli, R. and  Bensalem, S. and  Bozga, M. and  Sifakis, J.},
	pages = {701-719},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-04106085},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{el-hokayem_a_framework_for_2021_hal-04106260,
	title = {A framework for the specification and validation of dynamic reconfigurable systems},
	volume = {21},
	issn = {1559-6915},
	doi = {10.1145/3477127.3477129},
	abstract = {We study a framework for the specification and validation of dynamic reconfigurable systems. The framework is based on configuration logic for the description of architecture styles which are families of architectures sharing common connectivity features. We express specifications in the Temporal Configuration Logic (TCL), a linear time temporal logic built from atomic formulas characterizing system configurations and temporal modalities. Two non-trivial benchmarks are introduced to show the adequacy of TCL for the specification of dynamic reconfigurable systems. We study an effective model-checking procedure based on SMT techniques for a non-trivial fragment of TCL which has been implemented in a prototype runtime verification tool. We provide preliminary experimental results illustrating the capabilities of the tool on the considered benchmark systems.},
	journal = {ACM SIGAPP applied computing review : a publication of the Special Interest Group on Applied Computing},
	author = {El-Hokayem, A. and  Bozga, M. and  Sifakis, J.},
	pages = {18-32},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-04106260},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{ene_outputsensitive_information_flow_2021_hal-04750655,
	title = {Output-sensitive information flow analysis *},
	volume = {17},
	doi = {10.23638/LMCS-17(1:15)2021},
	abstract = {<div><p>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.</p><p>We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive noninterference. 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.</p></div>},
	journal = {Logical Methods in Computer Science},
	author = {Ene, C. and  Mounier, L. and  Potet, M.-L.},
	pages = {15:1-15:29},
	year = {2021},
	eprinttype={HAL}, eprint = {hal-04750655},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{altisen_election_in_unidirectional_2020_hal-03452675,
	title = {Election in unidirectional rings with homonyms},
	volume = {146},
	issn = {0743-7315},
	doi = {10.1016/j.jpdc.2020.08.004},
	abstract = {We study leader election in unidirectional rings of homonyms that have no a priori knowledge of the number of processes. In this context, we show that there exists no algorithm that solves the process-terminating leader election problem for the class of asymmetrically labeled unidirectional rings. More precisely, we prove that there is no process-terminating leader election algorithm even for the subclass of unidirectional rings where at least one label is unique. Message-terminating leader election is also impossible for the class of unidirectional rings where only a bound on multiplicity is known. However, we show that the processterminating leader election is possible for two particular subclasses of asymmetrically labeled unidirectional rings where the multiplicity is bounded. We propose three efficient algorithms and analyze their complexities. We also give some non-trivial lower bounds.},
	journal = {Journal of Parallel and Distributed Computing},
	author = {Altisen, K. and  Datta, A. and  Devismes, S. and  Durand, A. and  Larmore, L.},
	pages = {79-95},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03452675},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{bozga_checking_deadlockfreedom_of_2020_hal-03040227,
	title = {Checking deadlock-freedom of parametric component-based systems},
	volume = {119},
	issn = {2352-2208},
	doi = {10.1016/j.jlamp.2020.100621},
	abstract = {We propose an automated method for computing inductive invariants used to proving deadlock freedom of parametric component-based systems. The method generalizes the approach for computing structural trap invariants from bounded to parametric systems with general architectures. It symbolically extracts trap invariants from interaction formulae defining the system architecture. The paper presents the theoretical foundations of the method and proves its soundness. It also reports on a preliminary experimental evaluation on several textbook examples.},
	journal = {Journal of Logical and Algebraic Methods in Programming},
	author = {Bozga, M. and  Iosif, R. and  Sifakis, J.},
	pages = {100621},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-03040227},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{echenim_the_bernaysschonfinkelramsey_class_2020_hal-02388326,
	title = {The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates},
	issn = {1529-3785},
	abstract = {This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications. It focuses on prenex formulae with a quantifier prefix in the language ∃ * ∀ * , that contain uninterpreted (heap-independent) predicate symbols. In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SL k)]. In contrast with existing work on Separation Logic, in which the universe of possible locations is assumed to be infinite, we consider both finite and infinite universes in the present paper. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SL k). Then we define two non-trivial subsets thereof, for which the finite and infinite satisfiability problems are PSPACE-complete, respectively, assuming that the maximum arity of the uninterpreted predicate symbols does not depend on the input. These fragments are defined by controlling the polarity of the occurrences of separating implications, as well as the occurrences of universally quantified variables within their scope. These decidability results have natural applications in program verification, as they allow to automatically prove lemmas that occur in e.g. entailment checking between inductively defined predicates and validity checking of Hoare triples expressing partial correctness conditions.},
	journal = {ACM Transactions on Computational Logic},
	author = {Echenim, M. and  Iosif, R. and  Peltier, N.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02388326},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{foughali_bridging_the_gap_2020_hal-02864928,
	title = {Bridging the Gap between Formal Verification and Schedulability Analysis: The Case of Robotics},
	volume = {111},
	issn = {1383-7621},
	doi = {10.1016/j.sysarc.2020.101817},
	abstract = {The challenges of deploying robots and autonomous vehicles call for further efforts to bridge the gap between the robotics, the real-time systems and the formal methods communities. Indeed, with robots being more and more involved in costly missions and contact with humans, a rigorous formal verification of their behavior in the presence of various real-time constraints is crucial. In order to increase our trust in its results, such verification should be carried out on models that are the closest possible to reality, and thus take into account hardware and OS specificities such as the number of cores provided by the robotic platform and the scheduling policy. In this paper, we propose a novel binary-search-inspired technique that allows to extend timed automata models of robotic specifications with dynamic-priority schedulers. Given a number of cores, the extended models can then be checked against various real-time and behav-ioral properties, including schedulability, within the same model checking framework. Our technique is implemented in an automatic translation from a robotic framework to UPPAAL, and evaluated on a real robotic case study, where it shows a significant gain in scalability as opposed to the counting technique used in the literature.},
	journal = {Journal of Systems Architecture},
	author = {Foughali, M. and  Hladik, P.-E.},
	pages = {101817},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02864928},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v3},
}

@article{holík¨radu_abstraction_refinement_and_2020_hal-02388322,
	title = {Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems},
	issn = {0925-9856},
	doi = {10.1007/s10703-020-00345-1},
	abstract = {A generic register automaton is a finite automaton equipped with variables (which may be viewed as counters or, more generally, registers) ranging over infinite data domains. A trace of a generic register automaton is an alternating sequence of alphabet symbols and values taken by the variables during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable in general, we give a semi-algorithm based on a combination of abstraction refinement and antichains, which is proved to be sound and complete, but whose termination is not guaranteed. Moreover, we further enhance the proposed algorithm by exploiting a concept of data simulations, i.e., simulation relations aware of the data associated with the words. We have implemented our technique in a prototype tool and show promising results on multiple non-trivial examples.},
	journal = {Formal Methods in System Design},
	author = {Holík¨radu, L. and  Iosif, R. and  Rogalewicz, A. and  Vojnar, T.},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02388322},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{liu_virtual_timeline_a_2020_hal-02875542,
	title = {Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation},
	volume = {4},
	issn = {2475-1421},
	doi = {10.1145/3371088},
	abstract = {The reliability and security of safety-critical real-time systems are of utmost importance because the failure of these systems could incur severe consequences (loss of lives or failure of the mission). Such properties require strong isolation between components (given the ongoing trend of accommodating multiple components in a single platform), and they rely on enforcement mechanisms provided by the underlying operating system (OS) kernel. In addition to spatial isolation which is commonly provided by OS kernels to various extents, it also requires temporal isolation, that is, properties on the schedule of one component (e.g., schedulability) are independent of behaviors of other components. The strict isolation between components relies critically on algorithmic properties of the concrete implementation of the scheduler, such as timely provision of time slots, obliviousness to preemption, etc. However, existing work either only reasons about an abstract model of the scheduler, or proves properties of the scheduler implementation that are not rich enough to establish the isolation between different components. In this paper, we present a novel compositional framework for reasoning about algorithmic properties of the concrete implementation of preemptive schedulers. In particular, we use virtual timeline, a variant of the supply bound function used in the real-time scheduling analysis, to specify and reason about the scheduling of each component in isolation. We show that the properties proved on this abstraction carry down to the generated assembly code of the OS kernel. Using this framework, we successfully verify a real-time OS kernel, which extends mCertiKOS, a single-processor non-preemptive kernel, with user-level preemption, a verified timer interrupt handler and a verified real-time scheduler. We prove that in the absence of microarchitectural level timing channels, this new kernel enjoys temporal and spatial isolation on top of the functional correctness guarantee. All the proofs are implemented in the Coq proof assistant.},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Liu, M. and  Rieg, L. and  Shao, Z. and  Gu, R. and  Costanzo, D. and  Kim, E. J. and  Yoon, M.-K.},
	pages = {1-31},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02875542},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{six_certified_and_efficient_2020_hal-02185883,
	title = {Certified and efficient instruction scheduling. Application to interlocked VLIW processors.},
	series = {OOPSLA 2020},
	issn = {2475-1421},
	doi = {10.1145/3428197},
	abstract = {CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics, and did not attempt reordering instructions for optimization. We present here a CompCert backend for a VLIW core (i.e. with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Six, C. and  Boulmé, S. and  Monniaux, D.},
	pages = {129},
	year = {2020},
	eprinttype={HAL}, eprint = {hal-02185883},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v3},
}

@article{altisen_gradual_stabilization_2019_hal-02420362,
	title = {Gradual stabilization},
	volume = {123},
	issn = {0743-7315},
	doi = {10.1016/j.jpdc.2018.09.002},
	journal = {Journal of Parallel and Distributed Computing},
	author = {Altisen, K. and  Devismes, S. and  Durand, A. and  Petit, F.},
	pages = {26-45},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02420362},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{balabonski_synchronous_gathering_without_2019_hal-01894618,
	title = {Synchronous Gathering without Multiplicity Detection: a Certified Algorithm},
	volume = {63},
	issn = {1432-4350},
	doi = {10.1007/s00224-017-9828-z},
	abstract = {In mobile robotic swarms, the gathering problem consists in coordinating all the robots so that in finite time they occupy the same location, not known beforehand. Multiplicity detection refers to the ability to detect that more than one robot can occupy a given position. When the robotic swarm operates synchronously, a well-known result by Cohen and Peleg permits to achieve gathering, provided robots are capable of multiplicity detection. We present a new algorithm for synchronous gathering, that does not assume that robots are capable of multiplicity detection, nor make any other extra assumption. Unlike previous approaches, the correctness of our proof is certified in the model where the protocol is defined, using the Coq proof assistant.},
	journal = {Theory of Computing Systems},
	author = {Balabonski, T. and  Delga, A. and  Rieg, L. and  Tixeuil, S. and  Urbain, X.},
	pages = {200-218},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01894618},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{bliudze_rigorous_design_of_2019_hal-01636392,
	title = {Rigorous Design of Cyber-Physical Systems : Linking Physicality and Computation},
	volume = {18},
	series = {Software and System Modeling},
	issn = {1619-1366},
	url = {https://doi.org/10.1007/s10270-017-0642-5},
	doi = {10.1007/s10270-017-0642-5},
	abstract = {Cyber-physical systems have developed into a very active research field, with a broad range of challenges and research directions going from requirements, to implementation and simulation, as well as validation and verification to guarantee essential properties. In this survey paper, we focus exclusively on the following fundamental issue: how to link physicality and computation, continuous time-space dynamics with discrete untimed ones? We consider that cyber-physical system design flow involves the following three main steps: 1) cyber-physical systems modeling; 2) discretization for executability; and 3) simulation and implementation. We review—and strive to provide insight into possible approaches for addressing—the key issues, for each of these three steps.},
	journal = {Software and Systems Modeling},
	author = {Bliudze, S. and  Furic, S. and  Sifakis, J. and  Viel, A.},
	pages = {1613--1636},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01636392},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{boulmé_refinement_to_certify_2019_hal-01133865,
	title = {Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra},
	volume = {62},
	issn = {0168-7433},
	doi = {10.1007/s10817-018-9492-2},
	abstract = {Our concern is the modular development of a certified static analyzer in Coq: we extend a certified abstract domain of convex polyhedra with a linearization procedure approximating polynomial expressions. In order to help such a development, we propose a proof framework, embedded in Coq, that implements a refinement calculus. It allows to hide for proofs several low-level aspects of the computations on abstract domains. Moreover, refinement proofs are naturally simplified thanks to computations of weakest preconditions.},
	journal = {Journal of Automated Reasoning},
	author = {Boulmé, S. and  Maréchal, A.},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01133865},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v4},
}

@article{dellabani_local_planning_semantics_2019_hal-04580644,
	title = {Local Planning Semantics: A Semantics for Distributed Real-Time Systems},
	volume = {6},
	issn = {2199-2002},
	doi = {10.4230/LITES-V006-I001-A001},
	abstract = {Design, implementation and verification of distributed real-time systems are acknowledged to be very hard tasks. Such systems are prone to different kinds of delay, such as execution time of actions or communication delays implied by distributed platforms. The latter increase considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies ensuring global consistency while satisfying the imposed timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and propose a semantics aiming to overcome the communication delays problem through anticipating the execution of interactions. To be effective in a distributed context, scheduling an interaction should rely on (as much as possible) local information only, namely the state of its participating components. However, as shown in this paper these information is not always sufficient and does not guarantee a safe execution of the system as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the former model. Thus, we also explore methods for analyzing such deadlock situations and for computing deadlock-free scheduling strategies when possible.},
	journal = {Leibniz Transactions on Embedded Systems},
	author = {Dellabani, M. and  Combaz, J. and  Bensalem, S. and  Bozga, M.},
	pages = {01:1--01:27},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-04580644},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{devismes_optimal_torus_exploration_2019_hal-02420598,
	title = {Optimal torus exploration by oblivious robots},
	volume = {101},
	issn = {0010-485X},
	doi = {10.1007/s00607-018-0595-8},
	abstract = {We deal with a team of autonomous robots that are endowed with motion actuators and visibility sensors. Those robots are weak and evolve in a discrete environment. By weak, we mean that they are anonymous, uniform, unable to explicitly communicate, and oblivious. We first show that it is impossible to solve the terminating exploration of a simple torus of arbitrary size with less than 4 or 5 such robots, respectively depending on whether the algorithm is probabilistic or deterministic. Next, we propose in the SSYNC model a probabilistic solution for the terminating exploration of torus-shaped networks of size ℓ×L, where 7≤ℓ≤L, by a team of 4 such weak robots. So, this algorithm is optimal w.r.t. the number of robots.},
	journal = {Computing},
	author = {Devismes, S. and  Lamani, A. and  Petit, F. and  Tixeuil, S.},
	pages = {1241-1264},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02420598},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{el-hokayem_on_the_monitoring_2019_hal-02283429,
	title = {On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation},
	issn = {1049-331X},
	abstract = {We introduce two complementary approaches to monitor decentralized systems. The first approach relies on systems with a centralized specification, i.e., when the specification is written for the behavior of the entire system. To do so, our approach introduces a data structure that (i) keeps track of the execution of an automaton (ii) has predictable parameters and size and (iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study two properties of decentralized specifications pertaining to monitorability and compatibility between specification and architecture. We also present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Furthermore, we present THEMIS, a framework for designing such decentralized algorithms and simulating their behavior. We demonstrate the usage of THEMIS to compare multiple algorithms and validate the trends predicted by the analysis in two scenarios: a synthetic benchmark and the Chiron user interface.},
	journal = {ACM Transactions on Software Engineering and Methodology},
	author = {El-Hokayem, A. and  Falcone, Y.},
	pages = {1-57},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-02283429},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v2},
}

@article{magron_algorithms_for_weighted_2019_hal-01538729,
	title = {Algorithms for Weighted Sums of Squares Decomposition of Non-negative Univariate Polynomials},
	volume = {93},
	issn = {0747-7171},
	doi = {10.1016/j.jsc.2018.06.005},
	abstract = {It is well-known that every non-negative univariate real polynomial can be written as the sum of two polynomial squares with real coefficients. When one allows a weighted sum of finitely many squares instead of a sum of two squares, then one can choose all coefficients in the representation to lie in the field generated by the coefficients of the polynomial. In particular, this allows an effective treatment of polynomials with rational coefficients. In this article, we describe, analyze and compare both from the theoretical and practical points of view, two algorithms computing such a weighted sums of squares decomposition for univariate polynomials with rational coefficients. The first algorithm, due to the third author relies on real root isolation, quadratic approximations of positive polynomials and square-free decomposition but its complexity was not analyzed. We provide bit complexity estimates, both on the runtime and the output size of this algorithm. They are exponential in the degree of the input univariate polynomial and linear in the maximum bitsize of its complexity. This analysis is obtained using quantifier elimination and root isolation bounds. The second algorithm, due to Chevillard, Harrison, Joldes and Lauter, relies on complex root isolation and square-free decomposition and has been introduced for certifying positiveness of poly-nomials in the context of computer arithmetics. Again, its complexity was not analyzed. We provide bit complexity estimates, both on the runtime and the output size of this algorithm, which are polynomial in the degree of the input polynomial and linear in the maximum bitsize of its complexity. This analysis is obtained using Vieta's formula and root isolation bounds. Finally, we report on our implementations of both algorithms and compare them in practice on several application benchmarks. While the second algorithm is, as expected from the complexity result, more efficient on most of examples, we exhibit families of non-negative polynomials for which the first algorithm is better.},
	journal = {Journal of Symbolic Computation},
	author = {Magron, V. and  Safey el din, M. and  Schweighofer, M.},
	pages = {200-220},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01538729},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{magron_certified_roundoff_error_2019_hal-01956817,
	title = {Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations},
	volume = {68},
	issn = {0018-9340},
	doi = {10.1109/TC.2018.2851235},
	abstract = {Floating point error is a drawback of embedded systems implementation that is difficult to avoid. Computing rigorous upper bounds of roundoff errors is absolutely necessary for the validation of critical software. This problem of computing rigorous upper bounds is even more challenging when addressing non-linear programs. In this paper, we propose and compare two new algorithms based on Bernstein expansions and sparse Krivine-Stengle representations, adapted from the field of the global optimization, to compute upper bounds of roundoff errors for programs implementing polynomial and rational functions. We also provide the convergence rate of these two algorithms. We release two related software package FPBern and FPKriSten, and compare them with the state-of-the-art tools. We show that these two methods achieve competitive performance, while providing accurate upper bounds by comparison with the other tools.},
	journal = {IEEE Transactions on Computers},
	author = {Magron, V. and  Rocca, A. and  Dang, T.},
	pages = {953-966},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01956817},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{magron_semidefinite_approximations_of_2019_hal-01828443,
	title = {Semidefinite Approximations of Invariant Measures for Polynomial Systems},
	volume = {24},
	issn = {1531-3492},
	doi = {10.3934/dcdsb.2019165},
	abstract = {We consider the problem of approximating numerically the moments and the supports of measures which are invariant with respect to the dynamics of continuous- and discrete-time polynomial systems, under semialgebraic set constraints. First, we address the problem of approximating the density and hence the support of an invariant measure which is absolutely continuous with respect to the Lebesgue measure. Then, we focus on the approximation of the support of an invariant measure which is singular with respect to the Lebesgue measure. Each problem is handled through an appropriate reformulation into a linear optimization problem over measures, solved in practice with two hierarchies of finite-dimensional semidefinite moment-sum-of-square relaxations, also called Lasserre hierarchies. Under specific assumptions, the first Lasserre hierarchy allows to approximate the moments of an absolutely continuous invariant measure as close as desired and to extract a sequence of polynomials converging weakly to the density of this measure. The second Lasserre hierarchy allows to approximate as close as desired in the Hausdorff metric the support of a singular invariant measure with the level sets of the Christoffel polynomials associated to the moment matrices of this measure. We also present some application examples together with numerical results for several dynamical systems admitting either absolutely continuous or singular invariant measures.},
	journal = {Discrete and Continuous Dynamical Systems - Series B},
	author = {Magron, V. and  Forets, M. and  Henrion, D.},
	pages = {6745-6770},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01828443},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{maiza_a_survey_of_2019_hal-04741676,
	title = {A Survey of Timing Verification Techniques for Multi-Core Real-Time Systems},
	volume = {52},
	issn = {0360-0300},
	doi = {10.1145/3323212},
	abstract = {This survey provides an overview of the scientific literature on timing verification techniques for multi-core real-time systems. It reviews the key results in the field from its origins around 2006 to the latest research published up to the end of 2018. The survey highlights the key issues involved in providing guarantees of timing correctness for multi-core systems. A detailed review is provided covering four main categories: full integration, temporal isolation, integrating interference effects into schedulability analysis, and mapping and allocation. The survey concludes with a discussion of the advantages and disadvantages of these different approaches, identifying open issues, key challenges, and possible directions for future research.},
	journal = {ACM Computing Surveys},
	author = {Maiza, C. and  Rihani, H. and  Rivas, J. and  Goossens, J. and  Altmeyer, S. and  Davis, R.},
	pages = {1-38},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-04741676},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{maïza_fast_and_exact_2019_hal-01908648,
	title = {Fast and exact analysis for LRU caches},
	volume = {3},
	issn = {2475-1421},
	url = {https://dl.acm.org/citation.cfm?id=3290367},
	doi = {10.1145/3290367},
	abstract = {For applications in worst-case execution time analysis and in security, it is desirable to statically classify memory accesses into those that result in cache hits, and those that result in cache misses. Among cache replacement policies, the least recently used (LRU) policy has been studied the most and is considered to be the most predictable. The state-of-the-art in LRU cache analysis presents a tradeoff between precision and analysis efficiency: The classical approach to analyzing programs running on LRU caches, an abstract interpretation based on a range abstraction, is very fast but can be imprecise. An exact analysis was recently presented, but, as a last resort, it calls a model checker, which is expensive. In this paper, we develop an analysis based on abstract interpretation that comes close to the efficiency of the classical approach, while achieving exact classification of all memory accesses as the model-checking approach. Compared with the model-checking approach we observe speedups of several orders of magnitude. As a secondary contribution we show that LRU cache analysis problems are in general NP-complete.},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {Maïza, C. and  Touzeau, V. and  Monniaux, D. and  Reineke, J.},
	pages = {\#54},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01908648},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v2},
}

@article{monniaux_on_the_complexity_2019_hal-01910216,
	title = {On the complexity of cache analysis for different replacement policies},
	volume = {66},
	issn = {0004-5411},
	doi = {10.1145/3366018},
	abstract = {Modern processors use cache memory: a memory access that “hits” the cache returns early, while a “miss” takes more time. Given a memory access in a program, cache analysis consists in deciding whether this access is always a hit, always a miss, or is a hit or a miss depending on execution. Such an analysis is of high importance for bounding the worst-case execution time of safety-critical real-time programs. There exist multiple possible policies for evicting old data from the cache when new data are brought in, and different policies, though apparently similar in goals and performance, may be very different from the analysis point of view. In this paper, we explore these differences from a complexity-theoretical point of view. Specifically, we show that, among the common replacement policies, LRU (Least Recently Used) is the only one whose analysis is NP-complete, whereas the analysis problems for the other policies are PSPACE-complete.},
	journal = {Journal of the ACM (JACM)},
	author = {Monniaux, D. and  Touzeau, V.},
	pages = {41},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01910216},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v3},
}

@article{monniaux_on_the_decidability_2019_hal-01587125,
	title = {On the decidability of the existence of polyhedral invariants in transition systems},
	volume = {56},
	issn = {0001-5903},
	doi = {10.1007/s00236-018-0324-y},
	abstract = {Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties. For numerical properties, a classical class of invariants is convex polyhedra: solution sets of system of linear (in)equalities. Forty years of research on convex polyhedral invariants have focused, on the one hand, on identifying “easier” subclasses, on the other hand on heuristics for finding general convex polyhedra. These heuristics are however not guaranteed to find polyhedral inductive invariants when they exist. To our best knowledge, the existence of polyhedral inductive invariants has never been proved to be undecidable. In this article, we show that the existence of convex polyhedral invariants is undecidable, even if there is only one control state in addition to the “bad” one. The question is still open if one is not allowed any nonlinear constraint.},
	journal = {Acta Informatica},
	author = {Monniaux, D.},
	pages = {385-389},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-01587125},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v2},
}

@article{raymond_improving_wcet_evaluation_2019_hal-03013987,
	title = {Improving WCET Evaluation using Linear Relation Analysis},
	volume = {6},
	issn = {2199-2002},
	url = {https://ojs.dagstuhl.de/index.php/lites/article/view/LITES-v006-i001-a002},
	doi = {10.4230/LITES-v006-i001-a002},
	abstract = {The precision of a worst case execution time (WCET) evaluation tool on a given program is highly dependent on how the tool is able to detect and discard semantically infeasible executions of the program. In this paper, we propose to use the classical abstract interpretation-based method of linear relation analysis to discover and exploit relations between execution paths. For this purpose, we add auxiliary variables (counters) to the program to trace its execution paths. The results are easily incorporated in the classical workflow of a WCET evaluator, when the evaluator is based on the popular implicit path enumeration technique. We use existing tools - a WCET evaluator and a linear relation analyzer - to build and experiment a prototype implementation of this idea.},
	journal = {Leibniz Transactions on Embedded Systems},
	author = {Raymond, P. and  Maiza, C. and  Parent-Vigouroux, C. and  Jahier, E. and  Halbwachs, N. and  Carrier, F. and  Asavoae, M. and  Boutonnet, R.},
	pages = {02:28},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-03013987},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}

@article{socci_prioritybased_scheduling_of_2019_hal-04580646,
	title = {Priority-based scheduling of mixed-critical jobs},
	volume = {55},
	issn = {0922-6443},
	doi = {10.1007/S11241-019-09329-9},
	abstract = {Modern real-time systems tend to be mixed-critical, in the sense that they integrate on the same computational platform applications at different levels of criticality (e.g., safety critical and mission critical). Scheduling of such systems is a popular topic in literature due to the complexity and importance of the problem. In this paper we propose two algorithms for job scheduling in mixed critical systems: mixed criticality earliest deadline first (MCEDF) and mixed critical priority improvement (MCPI). MCEDF is a single processor algorithm that theoretically dominates state-of-the-art fixed-priority algorithm own criticality based priority (OCBP), while having a better computational complexity. The dominance is achieved by profiting from a common extension of fixed-priority online policy to mixed criticality. MCPI is a multiprocessor algorithm that supports dependency constraints. Experiments show good schedulability results. Also we formally prove that both MCEDF and MCPI are optimal in a particular class of algorithms.},
	journal = {Real-Time Systems},
	author = {Socci, D. and  Poplavko, P. and  Bensalem, S. and  Bozga, M.},
	pages = {709-773},
	year = {2019},
	eprinttype={HAL}, eprint = {hal-04580646},
	peer_reviewing = {1},
	audience = {2},
	HAL_version = {v1},
}
