JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution)
Ontology highlight
ABSTRACT:
SUBMITTER: Biere A
PROVIDER: S-EPMC7480698 | biostudies-literature | 2020 Mar
REPOSITORIES: biostudies-literature
Similar Datasets
Project description:Formal techniques have been devoted to analyzing whether network protocol specifications violate security policies; however, these methods cannot detect vulnerabilities in the implementations of the network protocols themselves. Symbolic execution can be used to analyze the paths of the network protocol implementations, but for stateful network protocols, it is difficult to reach the deep states of the protocol. This paper proposes a novel model-guided approach to detect vulnerabilities in network protocol implementations. Our method first abstracts a finite state machine (FSM) model, then utilizes the model to guide the symbolic execution. This approach achieves high coverage of both the code and the protocol states. The proposed method is implemented and applied to test numerous real-world network protocol implementations. The experimental results indicate that the proposed method is more effective than traditional fuzzing methods such as SPIKE at detecting vulnerabilities in the deep states of network protocol implementations.
| S-EPMC5690638 | biostudies-literature
Project description:GACAL verifies C programs by searching over the space of possible invariants, using traces of the input program to identify potential invariants. GACAL uses the ACL2s theorem prover to verify these potential invariants, using an interface provided by ACL2s for connecting with external tools. GACAL iteratively searches for and proves invariants of increasing complexity until the program is verified.
| S-EPMC7480696 | biostudies-literature
Project description:Striatal activity is necessary to initiate and execute sequences of actions. The main excitatory input to the striatum comes from the cortex. While it is hypothesized that motor and premotor cortico-striatal projections are important to guide striatal activity during the execution of sequences of actions, technical limitations have made this challenging to address. Here, we implemented a task in mice that allows for the study of different moments to execute a serial order sequence consisting of two subsequences of actions. Using this task, we performed electrophysiological recordings in the premotor (M2) and primary motor (M1) cortices, and state-dependent optogenetic inhibitions of their cortico-striatal projections. We show that while both M2 and M1 contain activity modulations related to the execution of self-paced sequences, mainly, the premotor cortico-striatal projections contribute to the proper execution/structuring of these sequences.
| S-EPMC8457420 | 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:In an error-prone development process, the ability to localize faults is a crucial one. Generally speaking, detecting and repairing errant behavior at an early stage of the development cycle considerably reduces costs and development time. The debugging of the Verilog program takes much time to read the waveform and capture the signal, and in many cases, problem-solving relies heavily on experienced developers. Most existing Verilog fault localization methods utilize the static analysis method to find faults. However, using static analysis methods exclusively may result in some types of faults being inevitably ignored. The use of dynamic analysis could help resolve this issue. Accordingly, in this work, we propose a new fault localization approach for Verilog, named Detraque. After obtaining dynamic execution through test cases, Detraque traces these executions to localize faults; subsequently, it can determine the likelihood of any Verilog statement being faulty and sort the statements in descending order by suspicion score. Through conducting empirical research on real Verilog programs with 61 faulty versions, Detraque can achieve an EXAM score of 18.3%. Thus, Detraque is verified as able to improve Verilog fault localization effectiveness when used as a supplement to static analysis methods.
| S-EPMC9481022 | biostudies-literature
Project description:Human movements are flexible as they continuously adapt to changes in the environment. The recalibration of corrective responses to sustained perturbations (e.g., constant force) altering one's movement contributes to this flexibility. We asked whether the recalibration of corrective actions involve cerebral structures using stroke as a disease model. We characterized changes in muscle activity in stroke survivors and control subjects before, during, and after walking on a split-belt treadmill moving the legs at different speeds. The recalibration of corrective muscle activity was comparable between stroke survivors and control subjects, which was unexpected given the known deficits in feedback responses poststroke. Also, the intact recalibration in stroke survivors contrasted their limited ability to adjust their muscle activity during steady-state split-belt walking. Our results suggest that the recalibration and execution of motor commands are partially dissociable: cerebral lesions interfere with the execution, but not the recalibration, of motor commands on novel movement demands.
| S-EPMC7053171 | biostudies-literature
Project description:In multicellular organisms cells compete for resources or growth factors. If any one cell type wins, the co-existence of diverse cell types disappears. Existing dynamic Flux Balance Analysis (dFBA) does not accommodate changes in cell density caused by competition. Therefore we here develop 'dynamic competition Flux Balance Analysis' (dcFBA). With total biomass synthesis as objective, lower-growth-yield cells were outcompeted even when cells synthesized mutually required nutrients. Signal transduction between cells established co-existence, which suggests that such 'socialness' is required for multicellularity. Whilst mutants with increased specific growth rate did not outgrow the other cell types, loss of social characteristics did enable a mutant to outgrow the other cells. We discuss that 'asocialness' rather than enhanced growth rates, i.e., a reduced sensitivity to regulatory factors rather than enhanced growth rates, may characterize cancer cells and organisms causing ecological blooms. Therapies reinforcing cross-regulation may therefore be more effective than those targeting replication rates.
| S-EPMC10613221 | 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:During apoptosis, the interphase microtubule network is dismantled then later replaced by a novel, non-centrosomal microtubule array. These microtubules assist in the peripheral redistribution of nuclear fragments in the apoptotic cell; however, the regulation of apoptotic microtubule assembly is not understood. Here, we demonstrate that microtubule assembly depends upon the release of nuclear RanGTP into the apoptotic cytoplasm because this process is blocked in apoptotic cells overexpressing dominant-negative GDP-locked Ran (T24N). Actin-myosin-II contractility provides the impetus for Ran release and, consequently, microtubule assembly is blocked in blebbistatin- and Y27632-treated apoptotic cells. Importantly, the spindle-assembly factor TPX2 (targeting protein for Xklp2), colocalises with apoptotic microtubules, and siRNA silencing of TPX2, but not of the microtubule motors Mklp1 and Kid, abrogates apoptotic microtubule assembly. These data provide a molecular explanation for the assembly of the apoptotic microtubule network, and suggest important similarities with the process of RanGTP- and TPX2-mediated mitotic spindle formation.
| S-EPMC2720920 | biostudies-literature
Project description:An implicit mapping of number to space via a "mental number line" occurs automatically in adulthood. Here, we systematically explore the influence of differing representations of quantity (no quantity, non-symbolic magnitudes, and symbolic numbers) and directional flow of stimuli (random flow, left-to-right, or right-to-left) on learning and attention via a match-to-sample working memory task. When recalling a cognitively demanding string of spatial locations, subjects performed best when information was presented right-to-left. When non-symbolic or symbolic numerical arrays were embedded in these spatial locations, and mental number line congruency prompted, this effect was attenuated and in some cases reversed. In particular, low-performing female participants who viewed increasing non-symbolic number arrays paired with the spatial locations exhibited better recall for left-to-right directional flow information relative to right-to-left, and better processing for the left side of space relative to the right side of space. The presence of symbolic number during spatial learning enhanced recall to a greater degree than non-symbolic number--especially for female participants, and especially when cognitive load is high--and this difference was independent of directional flow of information. We conclude that quantity representations have the potential to scaffold spatial memory, but this potential is subtle, and mediated by the nature of the quantity and the gender and performance level of the learner.
| S-EPMC4351879 | biostudies-literature