dataesr/scientific-paragraphs-categorization huggingface dataset:
The goal of this work is to perform deductive verification of the linked list module, one of the most critical modules of Contiki. It is performed using the ACSL specification language  [4]  and the deductive verification plugin WP of FRAMA-C  [16]. Our approach is based on a parallel view of a linked list via a companion ghost array. Such a "flattened" view of the list avoids complex inductive predicates and allows for automatic struct list { struct list * next; int k; // a data field }; typedef struct list ** list_t; //Initialize a list void list_init(list_t pLst); //Get the length of a list int list_length(list_t pLst); //Get the first element of a list void * list_head(list_t pLst); //Get the last element of a list void * list_tail(list_t pLst); //Remove the first element of a list void * list_pop (list_t pLst); 16 //Add an item to the start of a list.
17 void list_push(list_t pLst, void * item); 18 //Remove the last element of a list. proof of most properties, but requires to maintain a strong link between the companion array and the list it models. All proofs have been checked for several list structures. A few auxiliary lemmas have been proved in the Coq proof assistant  [24] , where a significant effort has been done to make their proofs robust and independent of the specific list structure. Finally, we have validated the proposed specification by proving a few functions manipulating lists. The contributions of this work include formal specification of the list module  4  of Contiki in the ACSL specification language and its deductive verification using the WP plugin of FRAMA-C; a presentation of the underlying approach based on a companion ghost array; formal statement and proof of several lemmas useful for reasoning about this representation; pointing out an (unintended?) inconsistency in precondition of one function; a preliminary validation of the proposed specification of the module via a successful verification of a few annotated test functions dealing with lists.
The List Module of Contiki Required by 32 modules and invoked more than 250 times in the core of the OS, the linked list module (list) is a crucial library in Contiki. It is used, for instance, to implement the scheduler, where lists are used to manage timers and processes. Its verification is thus a key step for proving many other modules of the OS. The API of the module is given in Figure  1. Technically, it differs from many common linked list implementations in several regards. First, in Contiki an existing list (illustrated by the lower part of Figure  3 ) is identified or modified through a dedicated list handler -a variable supposed to refer to the first list element -called root in Figure  3. Copying one linked list into another is just copying such a list handler (cf. lines 22-23 in Figure  1 ) without duplicating list elements.
However, if prev_item is present in the list, the function directly adds new_item after prev_item without removing a previous instance of new_item from the list (if any). It shows that the uniqueness property is in general not preserved by the function, but in some cases it is. Thus this function does not respect a contract consistent with the other functions. We decided to ask the authors of Contiki to clarify this potentially dangerous behavior, that could for example allow to break the integrity of the list  6. Moreover, in the entire code of Contiki, we have found only one call to list_insert, and not a single one in the core part of the system. Unit tests could have permitted to identify such a bug. However, one difficulty with tests (that is also the cause of many security bugs) is the fact that we tend to test valid scenarios rather than invalid ones.
Validation of Specification To get confidence in the proposed specification, we have implemented 15 simple valid test functions  7  manipulating lists, and tried to prove simple properties on lists in them using the proposed contracts of the list module functions. The results show that in all tests, the correct properties were successfully proved by WP. We have also implemented 15 invalid tests. Each invalid function is a variant of a valid one where we have altered the contract (including such dangerous cases as violations of separation, or validity, or uniqueness), the ghost values or the code itself. For those functions, the verification leads, as expected, to proof failure. This gives us further confidence that the proposed contracts can be successfully used for a larger deductive verification of Contiki.
They also rely on ghost code for the proof, the main difference in our work is that the array we use for representation is only part of the specification and thus the cells can be allocated independently of this array using another policy, while they use arrays as the actual implementation of the trees. On the proof side, the main difference is that we rely on Coq to prove simple lemmas that can be used automatically by SMT solvers, while they use the so-called auto-active proof  [18]  to avoid the use of an interactive proof assistant. In this context, separation logic  [23]  is more suitable than the Hoare logic on which the WP plugin of FRAMA-C is based. Tools based on such a kind of logic may therefore be more suitable for the verification of a linked list API, for example VeriFast  [15]  or the Verified Software Toolchain  [1, 3].
The former has been used in several industrial case studies  [22]  while the latter has been mainly used to verify crytography related software  [2, 26]  but also a message passing system  [20]. We are not aware of efforts dedicated to the verification of linked list functions, but the example gallery of VeriFast 8  and the VST case studies do include linked list function specifications and verification. They are based on a logic list data structure and an inductive predicate relating the memory and such a logical data structure, as initially done by Reynolds  [23]. Reynolds reasoned on sequences of instructions rather than functions. He thus mostly expressed loop invariants. This has an impact on the style of the specifications. In this case, an existential quantification of logical data structures is convenient.
VeriFast and VST are based on concurrent separation logic  [7, 14]. It is difficult to compare the specifications because most VeriFast case studies take into account concurrency. For some of the examples related to linked lists, being based on separation logic does not seem to have a significant impact on the size of specifications with respect to the specifications we have. For the verification, FRAMA-C is the most automated. Moreover, in addition to the automated and interactive provers it natively supports, it can output verification conditions to many different provers using Why3ML  [11]  as an intermediate verification language. This eases the verification, and makes it more trustworthy. VeriFast is based on its embedded SMT solver Redux and can also use Z3. VST is a framework for Coq.
The specifications can be written in the Gallina language of Coq, making them very expressive. However, even with the dedicated tactics, proofs are less automated in VST than in FRAMA-C or VeriFast. One strong point of VST is that its logic is fully formalized in Coq and its soundness has been proved in Coq. It makes it the safer framework. Both for the WP Plugin and VeriFast, there exist some results about the correctness of subsets of the tools  [13, 25].
Conclusion and Future Work The expansion of devices connected to the Internet raises many security risks. One promising way to tackle this challenge is to use formal methods, which is one of the goals of the EU H2020 VESSEDIA project. This paper reports on verification of the list module of Contiki, which is one of the most critical modules of the operating system. It requires, in the context of C language, to deal with linked data structures and memory separation that are still hard to handle automatically. Our verification approach relies on a companion ghost array and some ghost code. Although the idea of using ghost code is not new, it appears to be highly beneficial in this context, allowing for an elegant reasoning over the companion array and for an automatic proof of the great majority of goals: more than 96% of goals in this case study have been proved automatically.
Imposing a limit on the size of the companion array (and therefore, the lists it models) is not a limitation since list sizes in Contiki are always bounded. The verification of the list module, intensively used by other modules of Contiki, opens the way to formal verification of higher-level modules depending on it. All proofs of this case study have been checked for several list structures. Moreover, we have implemented several test functions working with lists, and validated the proposed specification by obtaining a successful proof for correct properties, and a proof failure in the erroneous cases. In future work, we plan to start the verification of higher-level modules of Contiki. This verification is planned to be done using both the deductive verification tool FRAMA-C/WP and the value analysis tool FRAMA-C/EVA.
Acknowledgment. This work was partially supported by a grant from  CPER DATA  and the project  VESSEDIA , which has received funding from the  European Union 's  Horizon 2020 research and innovation programme  under grant agreement No  731453. The authors thank the  FRAMA-C team  for providing the tools and support, as well as  Patrick Baudin ,  Francois Bobot  and  Loïc Correnson  for many fruitful discussions and advice. Many thanks to the anonymous referees for their helpful comments.
In contrast to the analysis of cellular phenotypes  17  and protein localization  18  , smFISH data can be treated as point clouds. The smFISH signal inside a cell can thus be represented by features describing this spatial distribution of points, such as the mean nearest neighbor distance between spots or their average distance to the nuclear envelope. These features can then be used to group cells based on similarity in their RNA localization patterns, using supervised or unsupervised machine learning methods  7. However, one of the main difficulty in this approach is the absence of a ground truth for RNA localization in smFISH data, making it impossible to assess usefulness of features and performance of the classification workflow. Hence, as of today, there is no rigorously validated method to analyze smFISH data at the cellular level.
We show that the simulation of a large set of images enables designing and validating workflows for unsupervised and supervised analysis of smFISH data, which are capable of detecting a large variety of localization classes. We applied this approach to experimental data and successfully detected the different manually annotated localization classes. We also implemented a metric to quantitatively analyze heterogeneity of localization patterns. Application of this metric to our experimental data set revealed a surprisingly high degree of localization heterogeneity.
Results Simulating realistic ground-truth data. We designed a simulation framework capable of generating ground-truth data closely mimicking experimental smFISH images. First, we acquired fluorescence microscopy data to determine the 3D volume of cells and nuclei, as well as the typical smFISH background signal. We then placed individual RNAs with realistic signals according to pre-defined localization rules inside these cellular volumes. This set of simulated images allowed us to validate the entire analysis workflow from RNA detection to the identification of localization classes. Our approach to generate such synthetic smFISH images consists of four main steps (Supplementary Note 1): First, we inferred accurate 3D cellular shapes from experimental data  22. To do so, we performed an smFISH experiment in HeLa cells using Cy5-labeled probes against the highly expressed GAPDH mRNA.
Gene-level annotation therefore describes only a tendency and cannot be considered as a single-cell annotation. We applied the workflow that we had benchmarked on the simulated data to the experimental data and extracted localization features for each cell. We represented the extracted localization features as a t-SNE plot (Fig. 3a , Supplementary Note 5). We also created a more detailed version of this plot where each point was replaced by a thumbnail representation of the cell, showing outlines of cells and nuclei and the detected RNAs. The plot can be viewed at https://muellerflorian. github. io/locFISH_deepzoom/ #results/tsne_exp (for examples of the thumbnails see Fig. 3a ). The tools to generate such plots are part of the provided Matlab source code. This zoomable t-SNE plot gives a clear picture of what the localization patterns in different regions of the feature space look like.
Discussion In this study, we present a framework for the simulation of smFISH images with non-random mRNA localization patterns and methods for their computational analysis. The realistic simulations allow to: (i) benchmark computational workflows aiming at studying RNA localization; (ii) assess the descriptive power of features; and (iii) evaluate the overall performance of clustering and classification methods. We developed a set of 23 localization features that could group cells based on seven simulated localization patterns with unprecedented accuracy. We further analyzed experimental data and correctly identified manually annotated localization classes. Importantly, we also demonstrate that simulated smFISH data can be used to train classifiers in a supervised setting, which when applied on real smFISH data allow to observe and quantify heterogeneity in RNA localization.
Methods Cell culture. HeLa and C2C12 cell lines were obtained from ATCC and grown in DMEM medium (Gibco) supplemented with 10% FCS (Sigma). HeLa cell lines stably transfected with GFP-tagged BAC  29  were a kind gift from Anthony Hyman laboratory (MPI-CBG, Dresden, Germany) and were grown in DMEM medium supplemented with 10% FCS and 0. 4 mg/ml G418 (Gibco). smFISH probes. smiFISH probes were purchased from Integrated DNA Technologies. smFISH probes were synthesized by J. M. Escudier (SPCMIB, Toulouse, France) and labeled with Cy3 mono-reactive dye pack (GE Healthcare). Probe sequences are available in Supplementary Data 1. smFISH experiments for cell shape. Single molecule FISH (smFISH) and our recently published inexpensive variant (smiFISH  13  ) were performed as follows. Briefly, cells were fixed with 4% paraformaldehyde (Electron Microscopy Sciences) for 20 min at RT, and permeabilised in 70% ethanol overnight at 4 °C.
Three-dimensional image stacks were captured on a wide-field microscope (Zeiss Axioimager Z1) equipped with a 63 × 1. 4 NA objective and a scMOS camera (Zyla 4. 2 MP, Andor Technology) and controlled with Metamorph (Version 7. 8. 8. 0; Molecular Devices). Image analysis to infer cell shape. 2D segmentation of nuclei and cells was performed with the DAPI and CellMask TM channels with the open-source software CellCognition  19  using a standard segmentation workflow: Otsu and watershed separation for nuclei in the DAPI channel. Each nucleus then serves as a seed for a watershed segmentation to obtain the cells in the CellMask TM channel. Individual GAPDH mRNA molecules were localized with FISH-quant 14 in 3D. The Matlab function boundary was used to determine the conforming 3D boundary around the mRNAs, corresponding to the 3D cellular outline.
GAPDH is predominately excluded from the nuclei. To infer the positioning and height of the nuclei, the zpositions of mRNAs localized in small region in the center of the nuclei were analyzed. mRNAs were automatically separated into two groups above and below the nucleus by k-means clustering. This allowed inference of the average 3D height and position of the nuclei. For more information, see Supplementary Note 1. mRNA detection and localization in simulations. mRNA detection in 2D was performed with the MATLAB script provided in Battich et al. 7. mRNA detection in 3D was performed with a standard spot detection approach in FISH-quant  14. In short, an approximation of the second derivative of the images was first calculated with a LoG filter. mRNAs were pre-detected with a local maximum detection with a manually determined intensity threshold.
After detection, spots are fitted with a 3D Gaussian function and the GMM approach applied as detailed in Supplementary Note 2. In short, the algorithm reconstructs the mRNA foci in multiple single mRNA by using the average signal of a single mRNA as a reference. For each cell, the different localization features are calculated in Matlab, and saved as a text file that can be further analyzed. Ripley-K function calculation was implemented from scratch. The Matlab functions pdist and p_poly_dist (from Matlab file exchange) were used to compute the distance between mRNAs and a reference point (cell centroid, nucleus centroid) and mRNA and a polygon (cell membrane, nuclear envelope). The Matlab function imopen was used to perform a morphological opening on the cellular outlines. The normalization coefficients were calculated using the bwdist function that compute the distance map of a binary mask.
Statistical methods to analyze localization features. t-SNE projections were performed using the tsne function implemented in MATLAB available at https:// lvdmaaten. github. io/tsne/. k-means classification was performed using the Matlab function kmeans using 50 replicates; spectral clustering with the function Spec-tralClustering from Matlab file exchange; hierarchical clustering with the Matlab function clustergram with linkage method ward. Random forest (RF) classification was performed with the Matlab function treebagger. 100 trees were trained on simulated cells with moderate and high pattern strength and mRNA densities corresponding to an average of 100 and 200 mRNAs/cell. Gini impurity was calculated from the posterior probabilities for the RF classification: either from the mean probability per mRNA (population impurity) or the mean impurity for all cells of a mRNA (intracellular impurity).
Cell segmentation for mRNA localization. Automated nuclear and cell segmentation was performed with a custom algorithm based on the U-net 30 deep convolutional network. Nuclear segmentation was performed with the DAPI channel, cell segmentation was performed either with CellMask TM (if present) or with the actual smFISH image. For segmentation, 3D images were projected into 2D images with a recently described approach  13. mRNA detection and feature calculation. Analysis of experimental smFISH data was performed as described for simulated data. Except that the detection intensity threshold was determined for each experiment (mRNA) separately. We implemented a simple Matlab user interface FQ_detect, which is now part of FISH-quant, to facilitate the determination of this threshold. It proposes an automatically calculated threshold based on Otsu thresholding, based on empirically determined criteria.
Acknowledgements We thank  Anthony Hyman  for providing the HeLa cell lines transfected with BAC. We thank  Maria Vera  for critical reading of the manuscript. This research was supported by the  Agence Nationale de la Recherche  ( ANR-11-BSV8-018-02  and  ANR-14-CE10-0018-01 ),  Institut Pasteur ,  Fondation pour la Recherche Médicale  ( FRM DBI20131228556 ), and  La Ligue Nationale Contre le Cancer.
37, 38 To investigate the protection of rods by transplantation, we measured at P60 the thickness of the ONL that is composed of 95%-97% rods in most rodents. 39 Measurements were made on the whole retina (9. 5 mm 2 ). The measures were taken every 100 mm on each section by optical coherence tomography (OCT) (on average, 1,005 measurements per retina). On optical sections, the ONL is clearly identified by comparing the wild-type retina to that of the uninjected RCS rat in which this layer is absent (Figure  6A ). OCT images only the central 25%-30% of the retina, so the data do not score the peripheral retina. We noticed the irregular appearance of the outer segment of the RPE interface in the eyes of transplanted RCS rats compared to the regular linear reflective band seen in wild-type eyes.
Briefly, each rat at P50 was placed on a pedestal located in the center of four inward-facing liquid crystal display (LCD) computer monitor screens and was observed by an overhead infrared video camera with an infrared light source. Once the rat became accustomed to the pedestal, a 7 s trial was initiated by presenting the rat with a sinusoidal striped pattern that rotates either clockwise or counter-clockwise, as determined randomly by the OptoMotry software. Involuntary reflex head-tracking responses are driven by the left eye (clockwise rotations) and right eye (counter-clockwise rotations), respectively. Contrast sensitivity was measured at a spatial frequency of 0. 042 cycles per degree and at a speed of rotation of 0. 5 Hz. To assess visual acuity, gratings had a constant contrast of 100% and initial stimulus was 0.
6 mg in 0. 4 mL. Upper and lower lids were retracted to keep the eye open and proptosed. Viscotears liquid gel was placed on each cornea to keep it moistened after corneal contact by golden electrodes. A stainless-steel reference electrode was inserted subcutaneously on the head of the rat, and a second needle electrode inserted subcutaneously in the back of the rat grounded the signal. Animals were left for a further 5 min in complete darkness before recording. Ganzfeld ERGs were obtained simultaneously from both eyes to provide an internal control. For scotopic recordings, single flash recordings were obtained at light intensities of 3 mcds/m 2 , 30 mcds/m 2 , 0. 3 cds/m 2 , and 3 cds/m 2 using a sampling frequency of 5 kHz, a flash duration of 4 ms, and a frequency stimulus of 0. 5 Hz. Data were recorded from 50 ms before stimulus onset to 450 ms post-stimulus.
We used a live and dead assay (Molecular Probes) to monitor cell viability. A blind protocol was employed such that the person performing the live and dead analysis did not know which supernatant came from RPE-GFP-or RPE-OTX2transduced cells. For acquisition and cell counting, we developed an algorithm based on the Metamorph software (Universal Imaging). We read plates under an inverted fluorescence microscope (TE 200, Nikon) equipped with a mercury epifluorescent lamp with two excitation filters (485 and 520 nm), two emission filters (520 and 635 nm), a 10Â objective, a computer-driven motorized scanning stage (Märzhäuser), and a CCD camera. For the assay, we compared numbers of live cells with the mean number of live cells in the negative controls. Each assay was repeated three independent times with four replicates for each condition.
Statistics All data are expressed as means ± SE, unless otherwise stated. n = number of animals, eyes, or cells examined, as appropriate. Statistical significance was assessed using GraphPad Prism 6 software and applying unpaired non-parametric t test, ANOVA with Bonferroni or Dunnett's correction for multiple comparisons, Welch correction, Kolmogorov-Smirnov, and Wilcoxon matched pairs (two-tailed), where appropriate.
ACKNOWLEDGMENTS We thank  A. Bemelmans  for providing biological material. We thank  D. Zack ,  J. Bennicelli , and  J. Bennett  for technical and scientific help. This work was supported by  INSERM ,  Université Pierre  and  Marie Curie , and  Fondation Voir & Entendre. Molecular Therapy Vol. 26 No 1 January 2018 Please cite this article in press as: Kole et al. ,  Otx2-Genetically Modified Retinal Pigment Epithelial Cells Rescue Photoreceptors after Transplantation ,  Molecular Therapy  ( 2017 ), https://doi. org/10. 1016/j. ymthe. 2017. 09. 007.