Search

Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks that could be verified previously.

Patients with systemic lupus erythematosus (SLE) presenting with chest pain pose a unique diagnostic challenge, with causes ranging from cardiopulmonary disease to esophageal disorders and musculoskeletal chest wall pain. The most common biomarkers for myocardial injury are cardiac troponin T and I (cTnT and cTnI) due to their high sensitivity for the early detection of myocardial infarction. In the idiopathic inflammatory myopathies, cTnT is commonly elevated, and this reflects skeletal muscle breakdown rather than myocardial damage. Similar observations have not been reported in SLE myositis to date. We present two cases of patients with SLE and associated myositis who presented with chest pain and elevated cTnT. Both patients had a normal cTnI, transthoracic echocardiogram, and cardiac magnetic resonance imaging, likely indicating noncardiac chest pain. Clinicians should be aware that the specificity of cTnT might be lower in SLE myositis and that cTnI elevation may be more specific in detecting myocardial insult.

Immunoglobulin G4-related disease (IgG4-RD) is a systemic immune-mediated fibroinflammatory disease. Since its discovery nearly two decades ago, our understanding of its pathophysiology and clinical manifestations has grown substantially. Early diagnosis and treatment of this elusive disease can prevent substantial organ damage from end-stage fibrosis, emphasizing the need for prompt recognition and accurate characterization of IgG4-RD. The classification criteria endorsed by the American College of Rheumatology and the European Alliance of Associations for Rheumatology in 2019 provide a framework for establishing the diagnosis in the clinical setting. This process involves recognizing the typical manifestations of the disease and incorporating clinical, radiological, serological, and histopathological information as well as excluding disease mimickers. Glucocorticoids and rituximab are effective at inducing remission in IgG4-RD in most patients, but the optimal approach to long-term management of IgG4-RD remains an area of active clinical research. Expected final online publication date for the Annual Review of Medicine, Volume 73 is January 2022. Please see http://www.annualreviews.org/page/journal/pubdates for revised estimates.

The application of deep reinforcement learning (DRL) to computer and networked systems has recently gained significant popularity. However, the obscurity of decisions by DRL policies renders it hard to ascertain that learning-augmented systems are safe to deploy, posing a significant obstacle to their real-world adoption. We observe that specific characteristics of recent applications of DRL to systems contexts give rise to an exciting opportunity: applying formal verification to establish that a given system provably satisfies designer/user-specified requirements, or to expose concrete counter-examples. We present whiRL, a platform for verifying DRL policies for systems, which combines recent advances in the verification of deep neural networks with scalable model checking techniques. To exemplify its usefulness, we employ whiRL to verify natural equirements from recently introduced learning-augmented systems for three real-world environments: Internet congestion control, adaptive video streaming, and job scheduling in compute clusters. Our evaluation shows that whiRL is capable of guaranteeing that natural requirements from these systems are satisfied, and of exposing specific scenarios in which other basic requirements are not.

High-grade ovarian cancer (HGOC) is the leading cause of mortality from gynecological malignancies, because of diagnosis at a metastatic stage. Current screening options fail to improve mortality because of the absence of early-stage-specific biomarkers. We postulated that a liquid biopsy, such as utero-tubal lavage (UtL), may identify localized lesions better than systemic approaches of serum/plasma analysis. Further, while mutation-based assays are challenged by the rarity of tumor DNA within nonmutated DNA, analyzing the proteomic profile, is expected to enable earlier detection, as it reveals perturbations in both the tumor as well as in its microenvironment. To attain deep proteomic coverage and overcome the high dynamic range of this body fluid, we applied our method for microvesicle proteomics to the UtL samples. Liquid biopsies from HGOC patients (n = 49) and controls (n = 127) were divided into a discovery and validation sets. Data-dependent analysis of the samples on the Q-Exactive mass spectrometer provided depth of 8578 UtL proteins in total, and on average ∼3000 proteins per sample. We used support vector machine algorithms for sample classification, and crossed three feature-selection algorithms, to construct and validate a 9-protein classifier with 70% sensitivity and 76.2% specificity. The signature correctly identified all Stage I lesions. These results demonstrate the potential power of microvesicle-based proteomic biomarkers for early cancer diagnosis.

Deep learning (DL) [4] is dramatically changing the world of software. The rapid improvement in deep neural network (DNN) technology now enables engineers to train models that achieve superhuman results, often surpassing algorithms that have been carefully hand-crafted by domain experts [19, 20]. There is even an intensifying trend of incorporating DNNs in safety-critical systems, e.g. as controllers for autonomous vehicles and drones [1, 12].

Repairing legacy systems is a difficult and error-prone task: often, limited knowledge of the intricacies of these systems could make an attempted repair result in new errors. Consequently, it is desirable to repair such systems in an automated and sound way. Here, we discuss our ongoing work on the automated repair of scenario-based models: fully executable models that describe a system using scenario objects that model its individual behaviors. We show how rich, scenario-based models can be model-checked, and then repaired to prevent various safety violations. The actual repair is performed by adding new scenario objects to the model, and without altering existing ones - in a way that is well aligned with the principles of scenario-based modeling. In order to automate our repair approach, we leverage off-the-shelf SMT solvers. We describe the main principles of our approach, and discuss our plans for future work., This is a preprint version of a paper that will appear at Modelsward 2021

Deep learning has emerged as an effective approach for creating modern software systems, with neural networks often surpassing hand-crafted systems. Unfortunately, neural networks are known to suffer from various safety and security issues. Formal verification is a promising avenue for tackling this difficulty, by formally certifying that networks are correct. We propose an SMT-based technique for verifyingbinarized neural networks— a popular kind of neural network, where some weights have been binarized in order to render the neural network more memory and energy efficient, and quicker to evaluate. One novelty of our technique is that it allows the verification of neural networks that include both binarized and non-binarized components. Neural network verification is computationally very difficult, and so we propose here various optimizations, integrated into our SMT procedure as deduction steps, as well as an approach for parallelizing verification queries. We implement our technique as an extension to the Marabou framework, and use it to evaluate the approach on popular binarized neural network architectures.

Deep neural networks (DNNs) are becoming widespread, and can often outperform manually-created systems. However, these networks are typically opaque to humans, and may demonstrate undesirable behavior in corner cases that were not encountered previously. In order to mitigate this risk, one approach calls for augmenting DNNs with hand-crafted override rules. These override rules serve to prevent the DNN from making certain decisions, when certain criteria are met. Here, we build on this approach and propose to bring together DNNs and the well-studied scenario-based modeling paradigm, by encoding override rules as simple and intuitive scenarios. We demonstrate that the scenario-based paradigm can render override rules more comprehensible to humans, while keeping them sufficiently powerful and expressive to increase the overall safety of the model. We propose a method for applying scenario-based modeling to this new setting, and apply it to multiple DNN models. (This paper substantially extends the paper titled “Guarded Deep Learning using Scenario-Based Modeling”, published in Modelsward 2020 [47]. Most notably, it includes an additional case study, extends the approach to recurrent neural networks, and discusses various aspects of the proposed paradigm more thoroughly).

Deep neural networks (DNNs) are revolutionizing the way complex systems are de- signed, developed and maintained. As part of the life cycle of DNN-based systems, there is often a need to modify a DNN in subtle ways that affect certain aspects of its behav- ior, while leaving other aspects of its behavior unchanged (e.g., if a bug is discovered and needs to be fixed, without altering other functionality). Unfortunately, retraining a DNN is often difficult and expensive, and may produce a new DNN that is quite different from the original. We leverage recent advances in DNN verification and propose a technique for modifying a DNN according to certain requirements, in a way that is provably minimal, does not require any retraining, and is thus less likely to affect other aspects of the DNN’s behavior. Using a proof-of-concept implementation, we demonstrate the usefulness and potential of our approach in addressing two real-world needs: (i) measuring the resilience of DNN watermarking schemes; and (ii) bug repair in already-trained DNNs.

Assisted hatching (AH) involves artificial disruption of the zona pellucida prior to embryo transfer. The purpose of this study is to examine the safety of AH technique and its effect on obstetrical, perinatal and neonatal outcomes and risk of developmental delay. This is a retrospective cohort of ART cycles using laser AH technique. The study group consisted of 120 cases of AH cycles resulting in singleton pregnancies and live births compared with 113 control cases. A current phone questionnaire was conducted to assess child development in the first year of life. AH was not associated with increased risk for all obstetrical and perinatal outcomes examined including PPROM, gestational diabetes, hypertensive diseases of pregnancy, delivery by cesarean section, gestational age at delivery, low birth weight (LBW), preterm birth and neonatal Apgar score (

A broad, long-term research project is described, which will lead to the computer becoming an equal member of the system-development team, continuously making proactive contributions, akin to those expected from an experienced and knowledgeable customer or user, a conscientious QA engineer, a strict regulatory auditor, an engineering -team leader, or the organization’s CTO. The web extra at https://youtu.be/mmrv8ZACbpU describes the authors’ novel “wise computing” approach and demonstrates one possible application. The second web extra at https://youtu.be/DtpvMxMwYPM extends the discussion of the authors’ novel “wise computing” approach and presents a case study.

Autonomous vehicles are highly complex systems, required to function reliably in a wide variety of situations. Manually crafting software controllers for these vehicles is difficult, but there has been some success in using deep neural networks generated using machine-learning. However, deep neural networks are opaque to human engineers, rendering their correctness very difficult to prove manually; and existing automated techniques, which were not designed to operate on neural networks, fail to scale to large systems. This paper focuses on proving the adversarial robustness of deep neural networks, i.e. proving that small perturbations to a correctly-classified input to the network cannot cause it to be misclassified. We describe some of our recent and ongoing work on verifying the adversarial robustness of networks, and discuss some of the open questions we have encountered and how they might be addressed., In Proceedings FVAV 2017, arXiv:1709.02126

Deep neural networks are revolutionizing the way complex systems are developed. However, these automatically-generated networks are opaque to humans, making it difficult to reason about them and guarantee their correctness. Here, we propose a novel approach for verifying properties of a widespread variant of neural networks, called recurrent neural networks. Recurrent neural networks play a key role in, e.g., speech recognition, and their verification is crucial for guaranteeing the reliability of many critical systems. Our approach is based on the inference of invariants, which allow us to reduce the complex problem of verifying recurrent networks into simpler, non-recurrent problems. Experiments with a proof-of-concept implementation of our approach demonstrate that it performs orders-of-magnitude better than the state of the art.

Deep neural networks (DNNs) are becoming prevalent, often outperforming manually-created systems. Unfortunately, DNN models are opaque to humans, and may behave in unexpected ways when deployed. One approach for allowing safer deployment of DNN models calls for augmenting them with hand-crafted override rules, which serve to override decisions made by the DNN model when certain criteria are met. Here, we propose to bring together DNNs and the well-studied scenario-based modeling paradigm, by expressing these override rules as simple and intuitive scenarios. This approach can lead to override rules that are comprehensible to humans, but are also sufficiently expressive and powerful to increase the overall safety of the model. We describe how to extend and apply scenario-based modeling to this new setting, and demonstrate our proposed technique on multiple DNN models., Comment: This is a preprint version of the paper that appeared at Modelsward 2020

Deep neural network (DNN) verification is an emerging field, with diverse verification engines quickly becoming available. Demonstrating the effectiveness of these engines on real-world DNNs is an important step towards their wider adoption. We present a tool that can leverage existing verification engines in performing a novel application: neural network simplification, through the reduction of the size of a DNN without harming its accuracy. We report on the work-flow of the simplification process, and demonstrate its potential significance and applicability on a family of real-world DNNs for aircraft collision avoidance, whose sizes we were able to reduce by as much as 10%.

Objectives The purpose of this study was to describe the characteristics and outcomes of fetuses with a diagnosis of nonobstructive diffuse dilated bowel loops. Methods We conducted a retrospective study of all pregnancies with fetal diagnosis of nonobstructive diffuse dilated bowel loops over 14 years in a large tertiary referral center. Fetomaternal and neonatal characteristics and outcomes were assessed. Results Seven fetuses had sonograms showing diffuse dilated bowel loops; none of them had intestinal obstruction after labor. The median gestational age at diagnosis was 33 weeks 1 day (range, 27 weeks–34 weeks 1 day). The median gestational age at delivery was 34 weeks 1 day (range, 32 weeks 4 days–39 weeks 1 day). Four cases had premature rupture of membranes beyond 32 weeks. Four among the 7 had gastrointestinal manifestations. Three cases presented with hematochezia, which resolved with conservative treatment. One fetus had intractable diarrhea, had a diagnosis of rare microvillus inclusion disease, and died of sepsis after 92 days. Not a single case of Hirschsprung disease was observed in our group. Conclusions Nonobstructive diffuse dilated bowel loops diagnosed in the second half of pregnancy are associated with premature rupture of membranes and premature labor. As neonatal gastrointestinal complications may be anticipated, prenatal parental counseling with a neonatologist and pediatric gastroenterologist should be conducted.

The authors present an initial wise development framework: a development environment that proactively and interactively assists the software engineer in modeling complex reactive systems. Their framework repeatedly analyzes models of the system under development at various levels of abstraction, and then reasons about these models in order to detect possible errors, to derive emergent properties of interest, and to assist in system testing and debugging. Upon request, the environment can instrument the system model in order to monitor or test the execution for certain behaviors, or even augment it in order to repair or avoid detected behavior that is undesired. The direction and prioritization of the analysis and related tasks is based on the relevance of the observed properties and the expected impact of actions to be taken, and is performed by specialized automated and human-assisted techniques that have been incorporated into the framework. The authors' development environment is an initial step in the direction of their recent Wise Computing vision, which calls for turning the computer (namely, the development environment) into an equal member of the development team: knowledgeable, independent, concerned and proactively involved in the development process. They have implemented their tool within the context of behavioral programming (BP) – a scenario-based modeling approach, in which components are aligned with how humans often describe desired system behavior. The authors' work thus further enhances the naturalness and incrementality of developing in BP.

Deep reinforcement learning (RL) has recently been successfully applied to networking contexts including routing, flow scheduling, congestion control, packet classification, cloud resource management, and video streaming. Deep-RL-driven systems automate decision making, and have been shown to outperform state-of-the-art handcrafted systems in important domains. However, the (typical) non-explainability of decisions induced by the deep learning machinery employed by these systems renders reasoning about crucial system properties, including correctness and security, extremely difficult. We show that despite the obscurity of decision making in these contexts, verifying that deep-RL-driven systems adhere to desired, designer-specified behavior, is achievable. To this end, we initiate the study of formal verification of deep RL and present Verily, a system for verifying deep-RL-based systems that leverages recent advances in verification of deep neural networks. We employ Verily to verify recently-introduced deep-RL-driven systems for adaptive video streaming, cloud resource management, and Internet congestion control. Our results expose scenarios in which deep-RL-driven decision making yields undesirable behavior. We discuss guidelines for building deep-RL-driven systems that are both safer and easier to verify.

Deep neural networks have achieved impressive results in many complex applications, including classification tasks for image and speech recognition, pattern analysis or perception in self-driving vehicles. However, it has been observed that even highly trained networks are very vulnerable to adversarial perturbations. Adding minimal changes to inputs that are correctly classified can lead to wrong predictions, raising serious security and safety concerns. Existing techniques for checking robustness against such perturbations only consider searching locally around a few individual inputs, providing limited guarantees. We propose DeepSafe, a novel approach for automatically assessing the overall robustness of a neural network. DeepSafe applies clustering over known labeled data and leverages off-the-shelf constraint solvers to automatically identify and check safe regions in which the network is robust, i.e. all the inputs in the region are guaranteed to be classified correctly. We also introduce the concept of targeted robustness, which ensures that the neural network is guaranteed not to misclassify inputs within a region to a specific target (adversarial) label. We evaluate DeepSafe on a neural network implementation of a controller for the next-generation Airborne Collision Avoidance System for unmanned aircraft (ACAS Xu) and for the well known MNIST network. For these networks, DeepSafe identified many regions which were safe, and also found adversarial perturbations of interest.

Background Spontaneous calcium release evoking delayed afterdepolarization is believed to cause catecholaminergic polymorphic ventricular tachycardia (CPVT), a lethal human arrhythmia provoked by exercise or emotional stress. β-Adrenergic blockers are the drug of choice, but fail to achieve complete arrhythmia control in some patients. These individuals often require flecainide, device implantation, and/or sympathetic denervation. Objective To optimize the arrhythmia therapy by pharmacological inhibition of the sympathetic nervous system in the homozygous calsequestrin knockout (CASQ2 Δ/Δ ) mouse model of CPVT2. Methods A heart telemetry device was implanted for continuous electrocardiographic recording at rest and during provocation testing. Calcium transients and abnormal calcium release were studied in cardiomyocytes isolated from adult mice. Adrenergic receptor expression was determined by using Western blotting and confocal microscopy. Results Adult CASQ2 Δ/Δ mice suffer from complex ventricular arrhythmia at rest and ventricular tachycardia during treadmill exercise and after epinephrine injection. β-Adrenergic blockers, propranolol and metoprolol, attenuated arrhythmia at rest but not after stress. Reserpine had no efficacy in controlling arrhythmia. Agents with α-blocking activity, phentolamine or labetalol, abolished both exercise- and epinephrine-induced arrhythmia. In contrast, injection of α-adrenergic agonist phenylephrine reproducibly provoked ventricular tachycardia. Isolated cardiomyocytes from CASQ2 Δ/Δ mice had delayed calcium release waves upon exposure to sympathetic agonists, which were abolished by phentolamine. Hearts of calsequestrin-mutant mice expressed more α1-adrenergic receptor than did wild type control mice ( P Conclusion We identified a contribution of the α-adrenergic pathway to the pathogenesis of catecholamine-induced arrhythmia. α-Blockade emerges as an effective therapy in the murine model of CPVT2 and should be tried in humans resistant to β-blockers.

Objectives To assess the safety and effectiveness of performing percutaneous coronary intervention (PCI) before transcatheter aortic valve implantation (TAVI). Background The presence of coronary artery disease (CAD) negatively impact procedural outcomes and long-term survival after (TAVI). The management of obstructive CAD before TAVI is not yet well established. Methods Patients with severe symptomatic aortic stenosis (AS) (n = 249) that underwent TAVI were divided into two groups: patients with CAD (subdivided to patients treated with TAVI alone and to patients that underwent PCI before TAVI) and patients with isolated AS. Procedural endpoints, device success and adverse events were considered according to the Valve Academic Research Consortium (VARC) definitions. Results Of a cohort of 249 consecutive patients with mean age of 83.2 ± 5.5 years, 83 patients with AS + CAD were treated with TAVI alone, 61 patients with AS + CAD underwent PCI before TAVI and 105 patients underwent TAVI for isolated AS. The mean duration of follow-up was 17 months (range: 6–36 months). Despite a significantly higher logistic EuroScore of the AS+CAD group compared to the AS alone group (30.1 vs. 21.1 P

International audience; This paper describes SMTCoq, a plug-in for the integration of external solvers into the Coq proof assistant. Based on a checker for generic first-order proof certificates fully implemented and proved correct in Coq, SMTCoq offers facilities to check answers from external SAT and SMT solvers and to increase Coq's automation using such solvers, all in a safe way. The current version supports proof certificates produced by the SAT solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier-free fragment of the combined theory of fixed-size bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols.

Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods.

This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors., In Proceedings HaTT 2016, arXiv:1606.05427

Catecholaminergic polymorphic ventricular tachycardia (CPVT) is a lethal ventricular arrhythmia evoked by physical or emotional stress. Recessively inherited CPVT is caused by either missense or null-allele mutations in the cardiac calsequestrin (CASQ2) gene. It was suggested that defects in CASQ2 cause protein deficiency and impair Ca2+ uptake to the sarcoplasmic reticulum and Ca2+-dependent inhibition of ryanodine channels, leading to diastolic Ca2+ leak, after-depolarizations, and arrhythmia. To examine the effect of exercise training on left ventricular remodeling and arrhythmia, CASQ2 knockout (KO) mice and wild-type controls underwent echocardiography and heart rhythm telemetry before and after 6 wk of training by treadmill exercise. qRT-PCR and Western blotting were used to measure gene and protein expression. Left ventricular fractional shortening was impaired in KO (33 ± 5 vs. 51 ± 7% in controls, P < 0.05) and improved after training (43 ± 12 and 51 ± 9% in KO and control mice, respectively, P = nonsignificant). The exercise tolerance was low in KO mice (16 ± 1 vs. 29 ± 2 min in controls, P < 0.01), but improved in trained animals (26 ± 2 vs. 30 ± 3 min, P = nonsignificant). The hearts of KO mice had a higher basal expression of the brain natriuretic peptide gene. After training, the expression of natriuretic peptide genes markedly decreased, with no difference between KO and controls. Exercise training was not associated with a change in ventricular tachycardia prevalence, but appeared to reduce arrhythmia load, as manifested by a decrease in ventricular beats during stress. We conclude that, in KO mice, which recapitulate the phenotype of human CPVT2, exercise training is well tolerated and could offer a strategy for heart conditioning against stress-induced arrhythmia.

Catecholaminergic polymorphic ventricular tachycardia (CPVT) is a primary electrical myocardial disease characterized by exercise- and stress-related ventricular tachycardia manifested as syncope and sudden death. The disease has a heterogeneous genetic basis, with mutations in the cardiac Ryanodine Receptor channel (RyR2) gene accounting for an autosomal-dominant form (CPVT1) in approximately 50% and mutations in the cardiac calsequestrin gene (CASQ2) accounting for an autosomal-recessive form (CPVT2) in up to 2% of CPVT cases. Both RyR2 and calsequestrin are important participants in the cardiac cellular calcium homeostasis. We review the physiology of the cardiac calcium homeostasis, including the cardiac excitation contraction coupling and myocyte calcium cycling. The pathophysiology of cardiac arrhythmias related to myocyte calcium handling and the effects of different modulators are discussed. The putative derangements in myocyte calcium homeostasis responsible for CPVT, as well as the clinical manifestations and therapeutic options available, are described.

We present a development environment that proactively and interactively assists the software engineer in modeling complex reactive systems. Our framework repeatedly analyzes models of the system under development at various levels of abstraction, and then reasons about these models in order to detect possible errors and to derive emergent properties of interest. Upon request, the environment can then augment the system model in order to repair or avoid detected behavior that is undesired, or instrument it in order to monitor the execution for certain behaviors. Specialized automated and human-assisted techniques are incorporated to direct and prioritize the analysis and related tasks, based on the relevance of the observed properties and the expected impact of actions to be taken. Our development environment is an initial step in the direction of the very recent Wise Computing vision, which calls for turning the computer (namely, the development environment) into an equal member of the development team: knowledgeable, independent, concerned and proactively involved in the development process. Our tool is implemented within the context of behavioral programming (BP), a scenario-based modeling approach, where components are aligned with how humans often describe desired system behavior. Thus, our work further enhances the naturalness and incrementality of developing in BP.

In recent years formal verification techniques have become an important part of the development cycle of concurrent software. In order to tackle the state explosion problem and verify larger systems, a great deal of work has been put into improving the scalability of verification tools. In this work, we seek to draw attention to an alternative/complementary approach to improving scalability, which sometimes receives less notice: the effect the concurrent programming model itself has on one’s ability to verify programs encoded within it. Recent work suggests that a suitable choice of model, tailored to the problem at hand, may render the produced software more amenable to verification techniques. We recapitulate some recent and new results demonstrating this effect in programming models for discrete, synchronous reactive systems, and outline some directions for future work. We hope that the paper will trigger additional research on this important topic.

In behavioral programming, a program consists of separate modules called behavior threads, each representing a part of the system’s allowed, necessary or forbidden behavior. An execution of the program is a series of synchronizations between these threads, where at each synchronization point an event is selected to be carried out. As a result, the execution speed is dictated by the slowest thread. We propose an eager execution mechanism for such programs, which builds upon the realization that it is often possible to predict the outcome of a synchronization point even without waiting for slower threads to synchronize. This allows faster threads to continue running uninterrupted, whereas slower ones catch up at a later time. Consequently, eager execution brings about increased system performance, better support for the modular design of programs, and the ability to distribute programs across several machines. It also allows to apply behavioral programming to a variety of problems that were previously outside its scope. We illustrate the method by concrete examples, implemented in a behavioral programming framework in C + + .

Background Catecholaminergic polymorphic ventricular tachycardia (CPVT) is a lethal arrhythmia provoked by physical or emotional stress and mediated by spontaneous Ca 2+ release and delayed after-depolarizations. Beta-adrenergic blockers are the therapy of choice but fail to control arrhythmia in up to 50% of patients. Objective To optimize antiarrhythmic therapy in recessively inherited CPVT caused by calsequestrin (CASQ2) mutations. Methods Murine heart rhythm telemetry was obtained at rest, during treadmill exercise, and after injection of epinephrine. The protocol was repeated after injection of different antiarrhythmic drugs. Results were then validated in human patients. Results Adult CASQ2 mutant mice had complex ventricular arrhythmia at rest and developed bidirectional and polymorphic ventricular tachycardia on exertion. Class I antiarrhythmic agents (procainamide, lidocaine, flecainide) were ineffective in controlling arrhythmia. Propranolol and sotalol attenuated arrhythmia at rest but failed to prevent VT during sympathetic stimulation. The calcium channel blocker verapamil showed a dose-dependent protection against CPVT. Verapamil was more effective than the dihydropyridine L-type Ca 2+ channel blocker nifedipine, and its activity was markedly enhanced when combined with propranolol. Human patients homozygous for CASQ2 D307H mutation, remaining symptomatic despite chronic β-blocker therapy, underwent exercise testing according to the Bruce protocol with continuous electrocardiogram recording. Verapamil was combined with propranolol at maximum tolerated doses. Adding verapamil attenuated ventricular arrhythmia and prolonged exercise duration in five of 11 patients. Conclusion Verapamil is highly effective against catecholamine-induced arrhythmia in mice with CASQ2 mutations and may potentiate the antiarrhythmic activity of β-blockers in humans with CPVT2.