GACAL: Conjecture-Based Verification : (Competition Contribution)
Ontology highlight
ABSTRACT:
SUBMITTER: Biere A
PROVIDER: S-EPMC7480696 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:In information security, one way to keep a secret content is through encryption. The objective is to alter the content so that it is not intelligible, and therefore only the intended user can reveal the secret content. With the aim to provide examples of encrypted audio data, we applied a novel method of encryption based on the Collatz conjecture in five hundred speech recordings (50 speakers, 10 different messages), and then five hundred encrypted audio files were obtained. The main characteristics of our encrypted recordings are as follows: the spectrogram is quasi-uniform, histograms have a repetitive pattern, average of samples is around -0.4, standard deviation is around 0.55; Shannon entropy is around 7.5 (for 8-bits per sample). The novelty of the results consists in obtaining a completely different behavior than natural speech recordings, i.e.: spectrogram with higher energy in low frequencies, histogram with Gaussian behavior, average of samples around 0, standard deviation around 0.11, entropy around 5.5. A more comprehensive analysis of our encrypted signals may be obtained from the article "High-uncertainty audio signal encryption based on the Collatz conjecture" in the Journal of Information Security and Applications.
| S-EPMC6811906 | biostudies-literature
Project description:We consider three graphs,
| S-EPMC7324133 | biostudies-literature
Project description:JDart performs dynamic symbolic execution of Java programs: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A constraint solver is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. JDart is built on top of the Java PathFinder software model checker and uses the JConstraints library for the integration of constraint solvers.
| S-EPMC7480698 | biostudies-literature
Project description:Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.
| S-EPMC7480687 | biostudies-literature
Project description:Members of social groups face a trade-off between investing selfish effort for themselves and investing cooperative effort to produce a shared group resource. Many group resources are shared equitably: they may be intrinsically non-excludable public goods, such as vigilance against predators, or so large that there is little cost to sharing, such as cooperatively hunted big game. However, group members' personal resources, such as food hunted individually, may be monopolizable. In such cases, an individual may benefit by investing effort in taking others' personal resources, and in defending one's own resources against others. We use a game theoretic "tug-of-war" model to predict that when such competition over personal resources is possible, players will contribute more towards a group resource, and also obtain higher payoffs from doing so. We test and find support for these predictions in two laboratory economic games with humans, comparing people's investment decisions in games with and without the options to compete over personal resources or invest in a group resource. Our results help explain why people cooperatively contribute to group resources, suggest how a tragedy of the commons may be avoided, and highlight unifying features in the evolution of cooperation and competition in human and non-human societies.
| S-EPMC3592809 | biostudies-literature
Project description:A common assumption in comparative genomics is that orthologous genes share greater functional similarity than do paralogous genes (the "ortholog conjecture"). Many methods used to computationally predict protein function are based on this assumption, even though it is largely untested. Here we present the first large-scale test of the ortholog conjecture using comparative functional genomic data from human and mouse. We use the experimentally derived functions of more than 8,900 genes, as well as an independent microarray dataset, to directly assess our ability to predict function using both orthologs and paralogs. Both datasets show that paralogs are often a much better predictor of function than are orthologs, even at lower sequence identities. Among paralogs, those found within the same species are consistently more functionally similar than those found in a different species. We also find that paralogous pairs residing on the same chromosome are more functionally similar than those on different chromosomes, perhaps due to higher levels of interlocus gene conversion between these pairs. In addition to offering implications for the computational prediction of protein function, our results shed light on the relationship between sequence divergence and functional divergence. We conclude that the most important factor in the evolution of function is not amino acid sequence, but rather the cellular context in which proteins act.
| S-EPMC3111532 | biostudies-literature
Project description:The linear composite direction represents, theoretically, where the unidimensional scale would lie within a multidimensional latent space. Using compensatory multidimensional IRT, the linear composite can be derived from the structure of the items and the latent distribution. The purpose of this study was to evaluate the validity of the linear composite conjecture and examine how well a fitted unidimensional IRT model approximates the linear composite direction in a multidimensional latent space. Simulation experiment results overall show that the fitted unidimensional IRT model sufficiently approximates linear composite direction when correlation between bivariate latent variables is positive. When the correlation between bivariate latent variables is negative, instability occurs when the fitted unidimensional IRT model is used to approximate linear composite direction. A real data experiment was also conducted using 20 items from a multiple-choice mathematics test from American College Testing.
| S-EPMC9265490 | biostudies-literature
Project description:Cellular memory, which allows cells to retain information from their environment, is important for a variety of cellular functions, such as adaptation to external stimuli, cell differentiation, and synaptic plasticity. Although posttranslational modifications have received much attention as a source of cellular memory, the mechanisms directing such alterations have not been fully uncovered. It may be possible to embed memory in multiple stable states in dynamical systems governing modifications. However, several experiments on modifications of proteins suggest long-term relaxation depending on experienced external conditions, without explicit switches over multi-stable states. As an alternative to a multistability memory scheme, we propose "kinetic memory" for epigenetic cellular memory, in which memory is stored as a slow-relaxation process far from a stable fixed state. Information from previous environmental exposure is retained as the long-term maintenance of a cellular state, rather than switches over fixed states. To demonstrate this kinetic memory, we study several models in which multimeric proteins undergo catalytic modifications (e.g., phosphorylation and methylation), and find that a slow relaxation process of the modification state, logarithmic in time, appears when the concentration of a catalyst (enzyme) involved in the modification reactions is lower than that of the substrates. Sharp transitions from a normal fast-relaxation phase into this slow-relaxation phase are revealed, and explained by enzyme-limited competition among modification reactions. The slow-relaxation process is confirmed by simulations of several models of catalytic reactions of protein modifications, and it enables the memorization of external stimuli, as its time course depends crucially on the history of the stimuli. This kinetic memory provides novel insight into a broad class of cellular memory and functions. In particular, applications for long-term potentiation are discussed, including dynamic modifications of calcium-calmodulin kinase II and cAMP-response element-binding protein essential for synaptic plasticity.
| S-EPMC4133053 | biostudies-literature
Project description:Biased-competition models assert that spatial attention facilitates visual perception by biasing competitive interactions in favor of relevant input. In line with this view, past work has shown that the benefits of covert spatial attention are greatest when targets must compete with interfering stimuli. Here we propose a boundary condition for the resolution of interference via exogenous attention: Attention resolves visual interference between targets and distractors, but only when they can be individuated into distinct representations. Thus, we propose that biased competition may be object-based. We replicated previous observations of larger attention effects when targets were flanked by irrelevant distractors (interference-present displays) than when targets were presented alone (interference-absent displays). Critically, we then showed that this amplification of cueing effects in the presence of interference is eliminated when strong crowding hampers individuation of the targets and distractors. Likewise, when targets were embedded within a noise mask that did not evoke the percept of an individuated distractor, the attention effects were equivalent across noise and lone-target displays. Thus, we conclude that exogenous spatial attention resolves interference in an object-based fashion that depends on the perception of individuated targets and distractors.
| S-EPMC6635026 | biostudies-literature
Project description:Acoustic-based proton range verification (protoacoustics) is a potential in vivo technique for determining the Bragg peak position. Previous measurements and simulations have been restricted to homogeneous water tanks. Here, a CT-based simulation method is proposed and applied to a liver and prostate case to model the effects of tissue heterogeneity on the protoacoustic amplitude and time-of-flight range verification accuracy. For the liver case, posterior irradiation with a single proton pencil beam was simulated for detectors placed on the skin. In the prostate case, a transrectal probe measured the protoacoustic pressure generated by irradiation with five separate anterior proton beams. After calculating the proton beam dose deposition, each CT voxel's material properties were mapped based on Hounsfield Unit values, and thermoacoustically-generated acoustic wave propagation was simulated with the k-Wave MATLAB toolbox. By comparing the simulation results for the original liver CT to homogenized variants, the effects of heterogeneity were assessed. For the liver case, 1.4 cGy of dose at the Bragg peak generated 50 mPa of pressure (13 cm distal), a 2× lower amplitude than simulated in a homogeneous water tank. Protoacoustic triangulation of the Bragg peak based on multiple detector measurements resulted in 0.4 mm accuracy for a δ-function proton pulse irradiation of the liver. For the prostate case, higher amplitudes are simulated (92-1004 mPa) for closer detectors (<8 cm). For four of the prostate beams, the protoacoustic range triangulation was accurate to ⩽1.6 mm (δ-function proton pulse). Based on the results, application of protoacoustic range verification to heterogeneous tissue will result in decreased signal amplitudes relative to homogeneous water tank measurements, but accurate range verification is still expected to be possible.
| S-EPMC5815855 | biostudies-literature