dataesr/scientific-paragraphs-categorization huggingface dataset:
Introduction Biologists are increasingly studying biological systems using holistic approaches such as genomics and proteomics. This means that a large amount of structural and interaction data becomes available. Interaction proteomics is especially focused on protein-protein interactions. Online databases like the MatrixDB centralises interactions data between proteins of the extracellular matrix (ECM)  [1]. While these provide invaluable pieces of information, there is no mean to simulate/visualise these interactions and to test their behaviour in a dynamical process. Although experimental observations methods have made great progress, there are still large portions of the cell or its environment, especially the ECM, that can only be observed indirectly. The ECM is an ensemble of molecules secreted outside the cells that were first considered as a medium providing structural support to the surrounding cells in tissues before being demonstrated as a reservoir of active molecules triggering biological signalling and functions  [2] ,  [3].
CGMD reduces the degree of liberty of a system by clustering many single atoms into single larger beads thus reducing the computational resources needed  [10]. It is multiscale in the sense that it is possible to go from an MD simulation to a CGMD simulation and vice versa. Molecular visualisation goes alongside simulation as the primary mean for the user to instinctively make sense of large complicated datasets. However, the average molecular visualisation package requires that you memorise hundreds of commands and shortcuts to be efficiently used. Biologists often have to get help from skilled computer users to learn the basics of navigating these software tools. And even then, the end-user often has to practice for a long time to achieve real proficiency. Immersive technologies such as virtual reality headsets free the users from the tedious apprenticeship required by molecular visualisation software.
Related Works Numerous initiatives in the field of mesoscale and/or multiscale modelling are worth being mentioned. CellPACK  [11]  builds 3D mesoscale models from a list of molecular ingredients provided by the user. These ingredients are treated as rigid bodies that CellPACK tries to pack as efficiently as possible inside a given geometrical shell that serves as a boundary. CellPACK itself does not generate motion or create trajectories. It relies on animation software or uses pre-calculated trajectories computed with other tools. The Open Dynamics Engine  [12]  rigid body physics has been used to study biological objects in the micrometre scale. The yeast nucleus has been studied using a simple physics model where each chromosome is modelled as chains of linked rigid bodies  [13]. UnityMol  [14]  is a visualisation tool developed with Unity3D.
Unity3D is a cross-platform game engine that is used in many applications outside of video games, mainly serious game but for simulation or data visualisation as well [15],  [16]. UnityMol is designed as a proof of concept to advocate the use of technologies developed in the video game industry to boost the performances of scientific visualisation tools. UnityMol uses Unity3D through scripting in C# or with custom shaders. Material shaders, like hyperball  [17] , are a set of instructions that are computed by the GPU for rendering. Compute shaders are softwares intended to be loaded and computed on the GPU for non-visual rendering tasks. UnityMol has also been used to make applications to explore the potential of augmented/mixed reality associated with tangible models  [18]. We think that the technology is now mature enough to try combining mesoscale models with rigid body chains.
Structural Data To gather as many information as possible on a macromolecular complex to make an accurate model of it, our main source of 3D structural data is derived from the Protein Data Bank (PDB) (www. rcsb. org) [22]  providing atomic coordinates for macromolecules, in a standard human-readable file, the PDB format. The perlecan molecule is a good example of a relatively simple reconstruction procedure we used because its domains have all been resolved individually and can be found directly in the PDB. In the literature, perlecan is described as being organised into five multi-domains (labelled from I to V), themselves consisting in a succession of domains of known structures. Biologists and biochemists already represent these multi-domain macromolecules as a series of colour schematic drawings as shown in the Figure  1A.
It is worth mentioning that a switch between models would be easy as soon as we get relevant structural or interaction data in the future. Another approach based on homologous structures permits the building of the laminin triple coil domain, a region missing in the starting model. The small helical part found in the integrin-binding region of laminin-111 (pdb id: 5MC9) bears a great structural similarity with Salmonella coiled coil (pdb id: 2WPQ), a triple coil structure solved and deposited in the PDB.
Coordinates Preparation Atoms coordinates found in the PDB are seldom centred around 0 and can make it harder to assemble the imported object together with joints if the pivot point is offset from the real centre of the molecule. Custom python scripts have been used in Blender  [24]  to manipulate 3D structural data by translating them so that the pivot point is located at the geometrical centre of the molecule. In cylindrical/elongated molecules, when a principal axis is self-evident, we realign them along one of the Cartesian axes. The Y axis is chosen because it is the default "up" vector in Unity's editor. The corrected coordinates are opened with VMD  [25]  to generate a surface mesh, then exported in a wavefront object file to be used in Unity.
6 mm). Major peaks were selected as follows: at each wavelength, a threshold corresponding to 20% of absorption observed in the highest peak was defined. Retention times of major peaks were identified for each of the five strains and mock extract, and an area under a curve (AUC) was calculated using Chem Station Open Lab software (Agilent Technologies, Santa Clara, CA, United States) for each extract at each retention time and each wavelength. When peaks at similar retention times were visible at different wavelengths, AUC correlation coefficients were measured. Peaks were considered to correspond to a single candidate compound when the minimum correlation coefficients (r) were above 0. 9, and thus a mean AUC was computed from each wavelength. When r was below 0. 9, AUCs from the two least correlated peaks were considered separately as candidate compounds.
Aldaulactone Purification and Characterization Aldaulactone purification and characterization was performed from cultures of A. dauci FRA001 and ITA002 strains. Liquid cultures and OE extractions were performed as previously, except that the scale of the liquid culture ranged from 10 × 100 mL in 250 mL erlenmeyer flasks, to 4 × 1 L in 5 L erlenmeyer flasks. Purification of aldaulactone from the obtained OE was achieved using the flash chromatography technique in an IntelliFlash 310 (Analogix) apparatus with pre-packed silica gel columns (Macherey-Nagel Chromabond R Flash RS column) and a cyclohexane/acetone mixture as mobile phase (9/1 to 6/4 gradient). 1 H and 13 C NMR along with 2D NMR data were obtained on a JEOL JNM-ECZS 400 MHz spectrometer (400 and 100 MHz, respectively) in deuterated chloroform with residual CHCl 3 signal as a reference.
Microscopic Evaluation of Cell Viability and Embryogenesis Ability Membrane integrity and cell viability were evaluated as previously described  (Lecomte et al. , 2014)  2 and 7 days after treatment. Briefly, 100 µL of the cell suspensions were stained with 10 µL fluorescein diacetate (0. 1 mg. mL -1 ) and 20 µL propidium iodide (1. 5 mg. mL -1 ), and incubated in the dark for 5 min. Stained cells were then observed under a fluorescence microscope (Leica DMR HC) equipped for illumination with a 100 W halogen bulb and a Leica L5 filter cube in order to detect green and red fluorescence simultaneously. The microscope was fitted with a digital camera (Qimaging, Retiga 2000R) and monitored using Image Pro Express 6. 0 software. Images were acquired at 3 s and 500 ms exposure, a gain of 1 with 1 × 1 binning (1600 pixels × 1200 pixels, 300 pixels per inch), and the images were saved in 24 bit-color TIFF format.
Microscopic Image Analysis Two methods were used: manual and automated fluorescent area evaluation. The toxic effect was estimated by calculating a percentage of living cells from green and red fluorescent areas. First, a manual method based on visual assessments was performed using the GNU Image Manipulation Program  (Kimball and Mattis, 2013). The 'curves' tool was used to enhance picture contrast and brightness. Thereafter, the 'posteriz' tool was used to reduce the number of colors. The suitable posterization level was determined by visual assessment. The 'select by color' tool was then used to select red and green areas and compute the number of green and red pixels in the image. Finally, these numbers were manually recorded in an Excel software file. The whole process was estimated to require several minutes of skilled work per image.
Secondly, a macro-based automated method was implemented. It was performed using ImageJ  (Schindelin et al. , 2015). We created an ImageJ macro for automatic determination of green and red areas. This macro can be applied in batch and requires about 1 s of machine time per image. 24-bit RGB (red green blue) pictures were converted into composite images. The 'split channels' command was used to separate the three different channels. Green and red channels were then analyzed separately. Green channel data were treated as follows: first, all pixel values above 50 were set at 50 using the 'max' function. Second, all pixel values were multiplied by 4. Then the 'subtract background' algorithm was used with the 'rolling' factor set at 50 pixels. When the picture's biggest object radius was higher, we used a rolling factor of 100.
The processed image was then binarized, with threshold values set at 25 and 255, and saved as a mask. The total green area of objects of more than 30 pixels 2 , was finally determined using the 'analyze particles' tool. Red channel data were treated as follows: first, the 'brightness/contrast' function was used, with minimum and maximum values set at 18 and 23, respectively. The image was subsequently binarized, with threshold values set at 50 and 255, and further processed using the 'erode' tool and then saved as a mask. The total red area of objects of more than 30 pixels 2 , was finally determined using the 'analyze particles' tool. Living cell percentages were calculated from green and red areas using Microsoft Excel (2016), and then stored for further analysis.
Statistical Analysis of Microscopic Images All statistical analyses were performed using the R v 3. 2. 4 software in R Studio v 1. 0. 136 (R Studio Team, 2016). Agreement between the two microscopic image analysis methods was assessed using a Passing-Bablok regression  (Bendix et al. , 2015). Normality and homoscedasticity of residues were checked by a Shapiro test and Bartlett test, respectively. Toxicity test data were analyzed using a two factor completely randomized design using two plant cell genotypes and 10 treatments as the two factors. Repetitions were treated as blocks. To determine cell viability in relation to the carrot genotype and treatment, data were submitted to multifactorial design ANOVA (type III) using the linear model  (Fox and Weisberg, 2017) , followed by a Tukey's HSD [honest significant difference post hoc test (de  Mendiburu, 2017) ].
In order to assess our new live and dead cell automated quantification method, we used a set of 97 microscopic images from one of our three toxicity assays. This image set was processed by visual assessment-and macro-based image analysis methods. Two datasets containing measured living cell percentages were thus generated. To assess the macro-based image analysis method, a Passing-Bablok regression analysis was performed on these two datasets. The confidence interval of 95% around the intercept and the slope, respectively, contained the values zero and one. We thus accepted the null hypothesis, i. e. , there was no constant or proportional difference between the two methods. The automated method selects pixels the same way as the conventional visual-assessment method. We thus decided to perform this macro-based method on all the microscopic images obtained from the three toxicity test experiments.
DISCUSSION The present study aimed to explore the link between A. dauci aggressiveness and toxin production. In our previous study  (Lecomte et al. , 2014) , a close correlation between the resistance FIGURE 4 | Correlations between aggressiveness and the composition of organic extract amongst A. dauci strains. Organic extracts from three different cultures of each A. dauci AUS001, FRA001, FRA017, and ITA002 strains and the A. brassicicola Abra 43 strain were analyzed using HPLC-DAD. Eleven candidate compounds were selected for area under a curve (AUC) statistical analysis from seven major peaks, as shown in Table  2. Organic extract weight (OEW), and AUC and OEW × AUC for each candidate compound were used as variables in 29 linear models of aggressiveness based on data obtained previously [mean NLA in  Boedo et al.
These results were generally in line with previous observations of differential resistance of H1 and I2 cells to A. dauci FRA017 OE toxicity  (Lecomte et al. , 2014). They also suggest that this differential resistance is not strain dependant. Both criteria also indicated that aldaulactone was toxic to carrot cells. Like FRA001 and ITA002 OEs, aldaulactone induced a delay in embryonic development and a decrease in cell viability. Moreover, H1 susceptibility and I2 resistance to OE could be paralleled with their resistance and susceptibility to aldaulactone. This dataset showed that aldaulactone toxicity is a key component of fungal exudate toxicity, and that aldaulactone is involved in both fungal pathogenicity and plant resistance mechanisms. Nevertheless, the higher toxicity of OEs as compared to that of corresponding aldaulactone concentrations indicated that cofactors or other toxins were perhaps also involved in these mechanisms.
Organic extract from three different cultures of A. dauci AUS001, FRA001, FRA017, and ITA002 strains and the A. brassicicola Abra 43 strain were analyzed using HPLC-DAD. Seven major peaks were selected for area under a curve (AUC) statistical analysis. Eleven candidate compounds were derived from those peaks, as described in the section "Materials and Methods. " OEW, and AUC and OEW × AUC for each candidate compound were used as variables in 23 linear models of aggressiveness based on data obtained previously [mean NLA in  Boedo et al. (2012) , Table  3 ]. For each linear model with a significant p-value (Bonferroni-corrected α = 0. 05/29= 1. 72. 10 -3 ), r 2 and p-values are shown, classified according to p-values.
Semi-structured interviews were conducted during the pre and post interviews. The observation took place while the CEO completed the tasks assigned during the evaluation. The researcher did not interfere with the activities performed by the interviewer, but the researcher answered questions and made clarifications when it was necessary. Furthermore, we instructed the CEO to speak out loud and explain his actions while he was doing the assigned tasks. The observation was registered in real time by taking notes and recording the CEO's voice. Data were collected only in the presence of the main researcher in a remote way using Skype. However, to reduce bias in the analysis, we used two different methods to collect information (interviews and observation) and more than one researcher participated in the analysis of the data.
Interview design Interviews with experts were divided into four stages: setup, framework training, questionnaire, and closing. Setup: The researcher explained to the expert the purpose and conditions of the interview and provided him the assessment tool. This tool already had data from a fictitious company to have information to show in the resulting charts. When possible, the interview was recorded. Finally, the researcher asked questions about its context and previous experience of the interviewee. Framework training: The researcher presented and explained the components of APPLIES (APPLIES-motivation and APPLIES-preparation) while asking the expert to interact with the assessment tool at the same time that the explanation was done. Questionnaire: Once the expert became familiar with the tool, he was asked questions to know his perception of the usefulness, completeness and potential limitations of APPLIES, as well as to know other works that could be of interest to consider.
One of these was an evaluation conducted with 14 practitioners of a postgraduate course in software engineering. In this experiment we evaluated human factors such as perceived usefulness and understandability over the version of the framework presented in this article. This evaluation was reported in  [61]. Other evaluations are also planned. For instance, regarding the quality of the content we plan to perform a second round of expert revisions. Regarding the perceived usefulness and understandability of the framework, we plan to conduct usability tests with potential users. Finally, regarding the intention of using APPLIES in real contexts, we are implementing the APPLIES framework as the online service of a product line engineering tool suite called VariaMos  [62]  and we are looking for companies that want to use APPLIES to evaluate APPLIES in real settings.
Such outcomes are consistent with the coincidence between both formu-lations when the CPM-EFG based solution is achieved under a reducedselective pressure nodal integration procedure, which has already been demonstrated in Section 5 ). Moreover, the computing time required under both numerical techniques are very similar, which suggests the convenience of preferably implementing the RIPM-EFG approach since allows the possibility of achieving accurate results with an entirely velocity based formulation. The EFG based formulations proposed in this study have been implemented in an in-house code developed in the Matlab ® software editor. Numerical solutions have been performed on a i3-2. 13 GHz (i3 is a trademark of Intel Corporation, Santa Clara, C. A. , USA) processor running the WINDOWS7 Home Basic (WINDOWS is a trademark of the Microsoft Corporation, Redmond, C.
Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts. In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers.
To leverage this issue, it is important, when no SMT solver is able to solve a given VC, to provide the user with means to investigate the proof failure: is it because the code needs to be fixed, is it because the program is not sufficiently annotated (e. g. a missing loop invariant), or is it because the VC is too complex to be discharged by automatic provers (e. g. an induction is needed). Among the possible means is the generation of counterexamples  [9]. Such a feature appears to be useful in particular to fix trivial mistakes, but for complex cases, its limitations quickly show up: because of the intrinsic incompleteness of back-end solvers, or more pragmatically because solvers proof search is typically interrupted after a given time limit is reached, the counterexamples may be spurious or absent  [9].
Moreover, there is no easy mean to distinguish a true bug from insufficiently detailed specifications (although there is on-going research in that direction  [15] ). This paper presents an approach that we designed in the context of the SPARK verifier for industrial development of safety-critical Ada code  [7, 12]. The goal is to provide simplified interactions between the user and the failing VC, so as to investigate a proof task without the need to rely on an external interactive prover. A specificity of SPARK is that the underlying toolchain from the given input Ada program to the VCs makes use of the external intermediate language Why3  [6]  that itself provides access to many different automated provers (mainly Alt-Ergo, CVC4 and Z3) but also general purpose interactive theorem provers (Coq, Isabelle/HOL, PVS).
Contributions and Overview of the Paper Our goals are shared with the above-mentioned related work. However, in the context of SPARK, there is an additional issue that does not show up in previous work. Indeed, in the previous work mentioned above, the language of formulas and proof tasks (e. g. proof sequents) is directly the language in which the user writes her input problem: for example in the context of the B method, the logic language is B set theory in which the code of the B machines is written; in KeY, the underlying Dynamic Logic incorporates pieces of Java code to verify. In the context of SPARK, we have the additional issue that a proof task generated by the Why3 VC generator is written in a language that is very different from the Ada input language. Our approach proceeds in the following steps.
Adding Interactive Proving in Why3 Figure  1  presents a general overview of Why3's core architecture. The input files contain code with formal specifications, written in the dedicated language WhyML  [8] , which essentially consists of a set of functions or procedures annotated with contracts (pre-and post-conditions, loop invariants, etc. ). The VC generator produces, from such a file, a set of proof tasks. A proof task, that we can denote as Γ G, consists in a set Γ of logical declarations of types, function symbols, predicates, and hypotheses, and finally the logical formula G representing the goal to prove. The soundness property of the VC generator expresses that if all generated proof tasks are valid logical statements, then the input program is safe: no runtime error can arise and formal contracts are satisfied.
For such a code, Why3 generates as the VC the formula forall a:array int, x:int. length a ≥ 1000 ∧ (0 ≤ x ∧ x ≤ 10) ∧ (forall i:int. 0 ≤ ((4 * i) + 1) ∧ ((4 * i) + 1) < length a → a[(4 * i) + 1] ≥ 0) → (let y = (2 * x) + 1 in let o = y * y in (0 ≤ o ∧ o < length a) ∧ a[o] ≥ 0) As one may guess such a formula can quickly become unreadable when code size grows, and is hardly suitable for human inspection.
Proof Tasks and Transformations The core of Why3 comes as a software library, written in the OCaml language and with a documented API, that proposes in particular data-types for terms, formulas and proof tasks, and a large collection of functions to operate on them. A central notion is the notion of transformation: an OCaml function that takes a proof task as input and returns a set of proof tasks. All implemented transformations are expected to be sound, in the sense that if all the resulting proof tasks are valid, then the original task is valid too. A simple example of such a transformation is splitting, which basically transforms a task of the form Γ G 1 ∧ G 2 ∧ • • • ∧ G k into the set of tasks Γ G i for 1 ≤ i ≤ k. The VC generator is designed so as to produce a single proof task for each procedure or function of the input code, as in the example above.