Search

PDF file - 42K, Quizartinib inhibition of MV4-11 tumor grwoth in vivo

PDF file - 279K, Immunoblots of MV4-11, MOLM14, and SEM-K2 with quizartinib DR

PDF file - 116K, Elevation of pro-apoptotic BimEL mirrors loss of anti-apoptotic Mcl-1

PDF file - 46K, Durability of quizartinib inhibition translates to loss of viability after brief exposure

PDF file - 54K, DMSO and DR to quizartinib, percent apoptotic cells is percent of cells with

PDF file - 74K, CEP-32496 Supplemental Data.

PDF file - 54K, Inhibition of FLT3 phosphorylation and cell viability by FLT3 inhibitors

Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods. Open image in new window , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage Open image in new window tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Open image in new window refinements and suggest a solution. We outline how safety and liveness properties could be verified.

The aggregation of attractive colloids has been extensively studied from both theoretical and experimental perspectives as the fraction of solid particles is changed, and the range, type, and strength of attractive or repulsive forces between particles varies. The resulting gels, consisting of disordered assemblies of attractive colloidal particles, have also been investigated with regards to percolation, phase separation, and the mechanical characteristics of the resulting fractal networks. Despite tremendous progress in our understanding of the gelation process, and the exploration of different routes for arresting the dynamics of attractive colloids, the complex interplay between convective transport processes and many-body effects in such systems has limited our ability to drive the system toward a specific configuration. Here, we study a model attractive colloidal system over a wide range of particle characteristics and flow conditions undergoing aggregation far from equilibrium. The complex multiscale dynamics of the system can be understood using a time-rate-transformation diagram adapted from understanding of materials processing in block copolymers, supercooled liquids, and much stiffer glassy metals to direct targeted assembly of attractive colloidal particles. Keywords: Colloidal gels, Directed assembly, Rheology, Attractive colloids, Targeted-design of colloids

Although popular in industry, state-chart notations with ‘run to completion’ semantics lack formal refinement and rigorous verification methods. State-chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage Event-B ’s tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how critical (e.g. safety) invariant properties can be verified by proof despite the reactive nature of the system. We also show how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic model checking approach.

We discuss techniques for efficient local detection of silent data corruption in parallel scientific computations, leveraging physical quantities such as momentum and energy that may be conserved by discretized PDEs. The conserved quantities are analogous to “algorithm-based fault tolerance” checksums for linear algebra but, due to their physical foundation, are applicable to both linear and nonlinear equations and have efficient local updates based on fluxes between subdomains. These physics-based checksums enable precise intermittent detection of errors and recovery by rollback to a checkpoint, with very low overhead when errors are rare. We present applications to both explicit hyperbolic and iterative elliptic (unstructured finite-element) solvers with injected memory bit flips.