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: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
Project description:Streptomyces spp. produce a variety of valuable secondary metabolites, which are regulated in a spatio-temporal manner by a complex network of inter-connected gene products. Using a compilation of genome-scale temporal transcriptome data for the model organism, Streptomyces coelicolor, under different environmental and genetic perturbations, we have developed a supervised machine-learning method for operon prediction in this microorganism. We demonstrate that, using features dependent on transcriptome dynamics and genome sequence, a support vector machines (SVM)-based classification algorithm can accurately classify >90% of gene pairs in a set of known operons. Based on model predictions for the entire genome, we verified the co-transcription of more than 250 gene pairs by RT-PCR. These results vastly increase the database of known operons in S. coelicolor and provide valuable information for exploring gene function and regulation to harness the potential of this differentiating microorganism for synthesis of natural products.
| S-EPMC2175336 | biostudies-literature
Project description:Cloud computing is a recent tendency in IT that moves computing and data away from desktop and hand-held devices into large scale processing hubs and data centers respectively. It has been proposed as an effective solution for data outsourcing and on demand computing to control the rising cost of IT setups and management in enterprises. However, with Cloud platforms user's data is moved into remotely located storages such that users lose control over their data. This unique feature of the Cloud is facing many security and privacy challenges which need to be clearly understood and resolved. One of the important concerns that needs to be addressed is to provide the proof of data integrity, i.e., correctness of the user's data stored in the Cloud storage. The data in Clouds is physically not accessible to the users. Therefore, a mechanism is required where users can check if the integrity of their valuable data is maintained or compromised. For this purpose some methods are proposed like mirroring, checksumming and using third party auditors amongst others. However, these methods use extra storage space by maintaining multiple copies of data or the presence of a third party verifier is required. In this paper, we address the problem of proving data integrity in Cloud computing by proposing a scheme through which users are able to check the integrity of their data stored in Clouds. In addition, users can track the violation of data integrity if occurred. For this purpose, we utilize a relatively new concept in the Cloud computing called "Data Provenance". Our scheme is capable to reduce the need of any third party services, additional hardware support and the replication of data items on client side for integrity checking.
| S-EPMC5435237 | biostudies-literature
Project description:Proton radiotherapy has the potential to provide state-of-the-art dose conformality in the tumor area, reducing possible adverse effects on surrounding organs at risk. However, uncertainties in the exact location of the proton Bragg peak inside the patient prevent this technique from achieving full clinical potential. In this context, in vivo verification of the range of protons in patients is key to reduce uncertainty margins. Protoacoustic range verification employs acoustic pressure waves generated by protons due to the radio-induced thermoacoustic effect to reconstruct the dose deposited in a patient during proton therapy. In this paper, we propose to use the a priori knowledge of the shape of the proton dose distribution to create a dictionary with the expected ultrasonic signals at predetermined detector locations. Using this dictionary, the reconstruction of deposited dose is performed by matching pre-calculated dictionary acoustic signals with data acquired online during treatment. The dictionary method was evaluated on a single-field proton plan for a prostate cancer patient. Dose calculation was performed with the open-source treatment planning system matRad, while acoustic wave propagation was carried out with k-Wave. We studied the ability of the proposed dictionary method to detect range variations caused by anatomical changes in tissue density, and alterations of lateral and longitudinal beam position. Our results show that the dictionary-based protoacoustic method was able to identify the changes in range originated by all the alterations introduced, with an average accuracy of 1.4?mm. This procedure could be used for in vivo verification, comparing the measured signals with the precalculated dictionary.
| S-EPMC7820918 | biostudies-literature