Search

Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies are known to be susceptible to bugs. Despite significant progress in DNN verification, there has been little work demonstrating the use of modern verification tools on real-world, DRL-controlled systems. In this case study, we attempt to begin bridging this gap, and focus on the important task of mapless robotic navigation — a classic robotics problem, in which a robot, usually controlled by a DRL agent, needs to efficiently and safely navigate through an unknown arena towards a target. We demonstrate how modern verification engines can be used for effective model selection, i.e., selecting the best available policy for the robot in question from a pool of candidate policies. Specifically, we use verification to detect and rule out policies that may demonstrate suboptimal behavior, such as collisions and infinite loops. We also apply verification to identify models with overly conservative behavior, thus allowing users to choose superior policies, which might be better at finding shorter paths to a target. To validate our work, we conducted extensive experiments on an actual robot, and confirmed that the suboptimal policies detected by our method were indeed flawed. We also demonstrate the superiority of our verification-driven approach over state-of-the-art, gradient attacks. Our work is the first to establish the usefulness of DNN verification in identifying and filtering out suboptimal DRL policies in real-world robots, and we believe that the methods presented here are applicable to a wide range of systems that incorporate deep-learning-based agents.

Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches for DNNs are focused on non-semantic perturbations and are not suited to the occlusion case. In this paper, we propose the first efficient, SMT-based approach for formally verifying the occlusion robustness of DNNs. We formulate the occlusion robustness verification problem and prove it is NP-complete. Then, we devise a novel approach for encoding occlusions as a part of neural networks and introduce two acceleration techniques so that the extended neural networks can be efficiently verified using off-the-shelf, SMT-based neural network verification tools. We implement our approach in a prototype called OccRob and extensively evaluate its performance on benchmark datasets with various occlusion variants. The experimental results demonstrate our approach’s effectiveness and efficiency in verifying DNNs’ robustness against various occlusions, and its ability to generate counterexamples when these DNNs are not robust.

With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are “black-boxes”, and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, researchers have begun working on explainable AI (XAI) methods, which can identify a subset of input features that are the cause of a DNN’s decision for a given input. Most existing techniques are heuristic, and cannot guarantee the correctness of the explanation provided. In contrast, recent and exciting attempts have shown that formal methods can be used to generate provably correct explanations. Although these methods are sound, the computational complexity of the underlying verification problem limits their scalability; and the explanations they produce might sometimes be overly complex. Here, we propose a novel approach to tackle these limitations. We (i) suggest an efficient, verification-based method for finding minimal explanations, which constitute a provable approximation of the global, minimum explanation; (ii) show how DNN verification can assist in calculating lower and upper bounds on the optimal explanation; (iii) propose heuristics that significantly improve the scalability of the verification process; and (iv) suggest the use of bundles, which allows us to arrive at more succinct and interpretable explanations. Our evaluation shows that our approach significantly outperforms state-of-the-art techniques, and produces explanations that are more useful to humans. We thus regard this work as a step toward leveraging verification technology in producing DNNs that are more reliable and comprehensible.

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.

In-vivo single cell clonal analysis in the adult mouse kidney has previously shown lineage-restricted clonal proliferation within varying nephron segments as a mechanism responsible for cell replacement and local regeneration. To analyze ex-vivo clonal growth, we now preformed limiting dilution to generate genuine clonal cultures from one single human renal epithelial cell, which can give rise to up to 3.4 * 106 cells, and analyzed their characteristics using transcriptomics. A comparison between clonal cultures revealed restriction to either proximal or distal kidney sub-lineages with distinct cellular and molecular characteristics; rapidly amplifying de-differentiated clones and a stably proliferating cuboidal epithelial-appearing clones, respectively. Furthermore, each showed distinct molecular features including cell-cycle, epithelial-mesenchymal transition, oxidative phosphorylation, BMP signaling pathway and cell surface markers. In addition, analysis of clonal versus bulk cultures show early clones to be more quiescent, with elevated expression of renal developmental genes and overall reduction in renal identity markers, but with an overlapping expression of nephron segment identifiers and multiple identity. Thus, ex-vivo clonal growth mimics the in-vivo situation displaying lineage-restricted precursor characteristics of mature renal cells. These data suggest that for reconstruction of varying renal lineages with human adult kidney based organoid technology and kidney regeneration ex-vivo, use of multiple heterogeneous precursors is warranted.

Depression, anxiety, and chronic pain are common comorbidities in patients with rheumatoid arthritis (RA), psoriatic arthritis (PsA), and ankylosing spondylitis (AS) and may substantially impact patient outcomes. We aimed to determine whether these comorbidities were associated with earlier TNF-inhibitor (TNFi) discontinuation.This retrospective cohort study using Optum's de-identified Clinformatics® Data Mart Database 2000-2014 identified patients with RA, PsA, and AS initiating a first TNFi. Depression/anxiety, chronic pain, and opioid use were identified using diagnosis codes and prescription fill data. Cox proportional hazards models were used to compare time to medication discontinuation in patients with or without each of these risk factors and to assess the additive effect of having multiple risk factors.Among 33,744 patients initiating a TNFi (23,888 RA, 6443 PsA, 3413 AS), depression/anxiety, chronic pain, and opioid use were common, with ≥ 1 risk factor in 48.1%, 42.5%, and 55.4% of patients with RA, PsA, and AS respectively. Each risk factor individually was associated with a 5-7-month lower median treatment persistence in each disease (all p 0.001). Presence of multiple risk factors had an additive effect on time to discontinuation with HR (95% CI) 1.19 (1.14-1.24), 1.41 (1.33-1.49), and 1.47 (1.43-1.73) for 1, 2, or 3 risk factors respectively in RA. Findings were similar in PsA and AS.Depression, anxiety, chronic pain, and opioid use are common in inflammatory arthritis and associated with earlier TNFi discontinuation. Recognizing and managing these risk factors may improve treatment persistence, patient outcomes, and cost of care. Key Points • Depression, anxiety, chronic pain, and opioid use are common in patients with inflammatory arthritis. • In patients initiating treatment with a TNF-inhibitor, depression, anxiety, chronic pain, or recent opioid use are associated with sooner discontinuation of TNFi therapy. • Patients with multiple of these risk factors are even more likely to discontinue therapy sooner.

Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on neural networks with piecewise-linear activation functions. Given a convex relaxation which over-approximates the non-convex activation functions, we encode the violations of activation functions as a cost function and optimize it with respect to the convex relaxation. The cost function, referred to as the Sum-of-Infeasibilities (SoI), is designed so that its minimum is zero and achieved only if all the activation functions are satisfied. We propose a stochastic procedure, , to efficiently minimize the SoI. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with . Extending the complete search with achieves multiple simultaneous goals: 1) it guides the search towards a counter-example; 2) it enables more informed branching decisions; and 3) it creates additional opportunities for bound derivation. An extensive evaluation across different benchmarks and solvers demonstrates the benefit of the proposed techniques. In particular, we demonstrate that SoI significantly improves the performance of an existing complete search procedure. Moreover, the SoI-based implementation outperforms other state-of-the-art complete verifiers. We also show that our technique can efficiently improve upon the perturbation bound derived by a recent adversarial attack algorithm.

Neural networks are very successful at detecting patterns in noisy data, and have become the technology of choice in many fields. However, their usefulness is hampered by their susceptibility to adversarial attacks. Recently, many methods for measuring and improving a network’s robustness to adversarial perturbations have been proposed, and this growing body of research has given rise to numerous explicit or implicit notions of robustness. Connections between these notions are often subtle, and a systematic comparison between them is missing in the literature. In this paper we begin addressing this gap, by setting up general principles for the empirical analysis and evaluation of a network’s robustness as a mathematical property—during the network’s training phase, its verification, and after its deployment. We then apply these principles and conduct a case study that showcases the practical benefits of our general approach.

Introduction: Long non-coding RNAs (lncRNAs) are important regulators of gene expression and are involved in cancer progression and metastasis. Although studies have shown that aberrant expression of lncRNAs mediates disease progression in ovarian cancer (OC), the role of lncRNA ADAMTS9-AS2 has not been well studied. Objective: To determine the role of ADAMTS9-AS2 on OC pathogenesis. Methods: We examined ADAMTS9-AS2 expression in human OC cells and tumor tissues using in situ hybridization (ISH). ADAMTS9-AS2 was overexpressed in A2780cp20 and IGROV1cp20 cells and evaluated its effects on cell proliferation, viability and apoptosis. To evaluate the role of ADAMTS9-AS2 in tumor suppression, nude mice were injected with ADAMTS9-AS2 over expressing cells. Reverse phase protein array (RPPA) was performed to identify the downstream regulators. Luciferase reporter assay was performed to confirm the interaction of targeted protein with ADAMTS9-AS2. In addition, epigenetic regulation of ADAMTS9-AS2 was studied using 5-Azacytidine. Results: A2780cp20 and IGROV1cp20 cells expressed lower amounts of ADAMTS9-AS2, while SKOV3 and PEO4 cells showed higher expression levels. ISH analysis showed dense nuclear staining of ADAMTS9-AS2 in normal fallopian tube sections, whereas OC sections showed reduced expression. Kaplan-Meier survival analysis showed that patients with high expression of ADAMTS9-AS2 had significantly better overall survival (p=0.0079) and progression-free survival (p=0.00018) than those with low ADAMTS9-AS2 expression. Overexpression of ADAMTS9-AS2 in A2780cp20 cells resulted in decreased proliferation (p Conclusion: ADAMTS9-AS2 acts as a tumor suppressor, by enhancing the expression of ANNEXIN A1, and thereby regulating tumor growth. Thus, ADAMTS9-AS2-ANNEXIN A1 axis may represent a novel therapeutic target in OC. Citation Format: Emine Bayraktar, Guy Katz, Dahai Jiang, Cristian Rodriguez-Aguayo, Lingegowda S. Mangala, Santosh K. Dasari, Elaine Stur, Cristina Ivan, Gabriel Lopez-Berestein, Anil K. Sood. Elucidating the role of ADAMTS9AS2 lncRNA in ovarian cancer [abstract]. In: Proceedings of the American Association for Cancer Research Annual Meeting 2022; 2022 Apr 8-13. Philadelphia (PA): AACR; Cancer Res 2022;82(12_Suppl):Abstract nr 1550.

Neural networks can learn complex, non-convex functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. Verification algorithms address this need and provide formal guarantees about a neural network by answering "yes or no" questions. For example, they can answer whether a violation exists within certain bounds. However, individual "yes or no" questions cannot answer qualitative questions such as "what is the largest error within these bounds"; the answers to these lie in the domain of optimization. Therefore, we propose strategies to extend existing verifiers to perform optimization and find: (i) the most extreme failure in a given input region and (ii) the minimum input perturbation required to cause a failure. A naive approach using a bisection search with an off-the-shelf verifier results in many expensive and overlapping calls to the verifier. Instead, we propose an approach that tightly integrates the optimization process into the verification procedure, achieving better runtime performance than the naive approach. We evaluate our approach implemented as an extension of Marabou, a state-of-the-art neural network verifier, and compare its performance with the bisection approach and MIPVerify, an optimization-based verifier. We observe complementary performance between our extension of Marabou and MIPVerify., 27 pages, 7 figures

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.

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 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.

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.

ScenarioTools is an Eclipse-based tool suite for the scenario-based modeling and analysis of reactive systems. ScenarioTools especially targets the modeling and analysis of systems where the behavior of the components is sensitive to changes in the component structure that can occur at run-time. For example, in a system of communicating cars, the cars' relationships can change due to their movement and influence how cars must interact. The modeling in ScenarioTools is based on the Scenario Modeling Language (SML), an extended variant of Live Sequence Charts (LSCs). For modeling structural changes and conditions, graph transformation rules can be combined with SML. The specifications are executable and can be analyzed by simulation. ScenarioTools further supports a formal synthesis procedure that can find specification inconsistencies or prove the specification's realizability. In this article, we illustrate the features of ScenarioTools by an example and describe its architecture.

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%.

Deep neural networks are increasingly being used as controllers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network verification approaches have recently been proposed. However, these approaches afford limited scalability, and applying them to large networks can be challenging. In this paper, we propose a framework that can enhance neural network verification techniques by using over-approximation to reduce the size of the network—thus making it more amenable to verification. We perform the approximation such that if the property holds for the smaller (abstract) network, it holds for the original as well. The over-approximation may be too coarse, in which case the underlying verification tool might return a spurious counterexample. Under such conditions, we perform counterexample-guided refinement to adjust the approximation, and then repeat the process. Our approach is orthogonal to, and can be integrated with, many existing verification techniques. For evaluation purposes, we integrate it with the recently proposed Marabou framework, and observe a significant improvement in Marabou’s performance. Our experiments demonstrate the great potential of our approach for verifying larger neural networks.

In-vivo single cell clonal analysis in the adult mouse kidney has previously shown lineage-restricted clonal proliferation within varying nephron segments as a mechanism responsible for cell replacement and local regeneration. To analyze ex-vivo clonal growth, we now preformed limiting dilution to generate genuine clonal cultures from one single human renal epithelial cell, which can give rise to up to 3.4 * 10

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 are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network’s properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks. We describe the system architecture and main components, evaluate the technique and discuss ongoing work.

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.

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.

As part of expanding the implementation and use of the behavioral programming (BP) approach in a variety of languages and configurations, we tackle some of the challenges associated with applying the approach in a truly distributed, decentralized manner, where different modules run on separate machines. BP supports the development of reactive applications from modules that are aligned with the desired and undesired scenarios of system behaviors as described, say, in a requirements document, in an enhancement request, or a field problem report. A key advantage of this approach is that it facilitates incremental development where loosely coupled modules are added as requirements are introduced, and meaningful prototype execution can be carried out from early stages of development. In BP, each behavioral module (called a behavior thread) takes care of a separate facet of the requirements, thus control is conceptually decentralized. However, as the underlying principles of BP call for constant synchronization of, and "consultation" with, all behavior threads, efficient implementation in a physically distributed environment is a significant challenge on the road to broader acceptance of BP as a viable new way to develop systems. We begin by describing an implementation of BP in Erlang, where the coordination protocol is implemented via message passing. We demonstrate through examples how developing distributed systems in Erlang can benefit from BP advantages of incremental development and alignment of the code modules with the requirements. Next, we propose general BP design patterns (not limited to Erlang) for using BP in distributed applications, showing how to design applications using BP without forcing full synchronization among all threads at each step of the execution. This allows modules to run at different time scales and to wait for external input without stalling the entire system. Finally, we propose ways to alter the execution mechanism of BP so that execution can progress without necessarily waiting for the synchronization of all the threads. The enhanced execution algorithm has the potential of accelerating the distributed execution of behavioral programs. We present a design pattern for programming behaviorally in Erlang.We present a proof-of-concept for a BP execution infrastructure in Erlang.We present BP design patterns for interfacing with unsynchronized environments.We present BP design patterns for coordinating behaviors at different time scales.We present mechanisms for eager execution in BP.

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

When assembling a nephron during development a multipotent stem cell pool becomes restricted as differentiation ensues. A faulty differentiation arrest in this process leads to transformation and initiation of a Wilms’ tumor. Mapping these transitions with respective surface markers affords accessibility to specific cell subpopulations. NCAM1 and CD133 have been previously suggested to mark human renal progenitor populations. Herein, using cell sorting, RNA sequencing, in vitro studies with serum-free media and in vivo xenotransplantation we demonstrate a sequential map that links human kidney development and tumorigenesis; In nephrogenesis, NCAM1+CD133− marks SIX2+ multipotent renal stem cells transiting to NCAM1+CD133+ differentiating segment-specific SIX2− epithelial progenitors and NCAM1−CD133+ differentiated nephron cells. In tumorigenesis, NCAM1+CD133− marks SIX2+ blastema that includes the ALDH1+ WT cancer stem/initiating cells, while NCAM1+CD133+ and NCAM1−CD133+ specifying early and late epithelial differentiation, are severely restricted in tumor initiation capacity and tumor self-renewal. Thus, negative selection for CD133 is required for defining NCAM1+ nephron stem cells in normal and malignant nephrogenesis.

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.

Rationale - The plateau phase of the ventricular action potential is the result of balanced Ca2+ influx and K+ efflux. The action potential is terminated by repolarizing K+ currents. Under β-adrenergic stimulation, both the Ca2+-influx and the delayed rectifier K+ currents IK are stimulated to adjust the cardiac action potential duration to the enhanced heart rate and to ascertain adequate increase in net Ca2+ influx. Intracellularly, a Calsequestrin2 (CASQ2)-ryanodine receptor complex serves as the most effective Ca2+ reservoir/release system to aid the control of intracellular Ca2+ levels. Currently, it is unclear if disease-associated CASQ2 gene variants alter intracellular free Ca2+ concentrations and if cardiac ion channels are affected by it. Objective – The goal of this study is to test if CASQ2 determines intracellular free Ca2+ concentrations and to identify cardiac ion channels that are affected by it. Further, we aim to study disease-associated CASQ2 gene variants in this context. Methods and Results - Here, we study the effects of the CASQ2 mutations R33Q, F189L, and D307H, located in highly conserved regions, on the functions of cardiac potassium channels in Xenopus oocytes using two electrode voltage clamp. As a result, CASQ2 wild type and CASQ2-mutants modulated hERG functions differently. Free Ca2+ measurements and molecular dynamics simulations imply alterations in Ca2+ buffer capacity paralled by changes in the dynamic behavior of the CASQ2-mutants compared to CASQ2 wild type. Conclusions - These in vitro and in silico data suggest a regulatory role of CASQ2 on cytosolic Ca2+ and hERG channels which may contribute to the etiology of CPVT.

Cyber-physical systems are found in many areas, e.g., manufacturing or smart cities. They consist of multiple components that cooperate to provide the desired functionality. This need for cooperation causes complex interactions between components, which makes developing cyber-physical systems difficult, especially systems whose component structure changes dynamically at runtime. We have created a formal, scenario-based specification method which makes it easier to develop distributed cyber-physical systems. We previously presented an approach for the distributed execution of such specifications based on naive and inefficient broadcasting. In this paper we propose a more efficient approach which uses the available network resources more economically.

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 + + .

Humans and genetically engineered mice with recessively inherited CPVT develop arrhythmia which may arise due to malfunction or degradation of calsequestrin (CASQ2). We investigated the relation between protein level and arrhythmia severity in CASQ2(D307H/D307H) (D307H), compared to CASQ2(Δ/Δ) (KO) and wild type (WT) mice. CASQ2 expression and Ca²⁺ transients were recorded in cardiomyocytes from neonatal or adult mice. Arrhythmia was studied in vivo using heart rhythm telemetry at rest, exercise and after epinephrine injection. CASQ2 protein was absent in KO heart. Neonatal D307H and WT hearts expressed significantly less CASQ2 protein than the level found in the adult WT. Adult D307H expressed only 20% of CASQ2 protein found in WT. Spontaneous Ca²⁺ release was more prevalent in neonatal KO cardiomyocytes (89%) compared to 33-36% of either WT or D307H, respectively, p

In this demo we present a recommender benchmark framework that serves as an infrastructure for comparing and examining the performance and feasibility of different recommender algorithms on various datasets with a variety of measures. The extendable infrastructure aims to provide easy plugging of novel recommendation-algorithms, datasets and compare their performance using visual tools and metrics with other algorithms in the benchmark. It also aims at generating a WEKA-type workbench [1] for the recommender systems field to enable usage and application of common recommender systems (RS) algorithms for research and practice. The demo movie is available at: http://www.youtube.com/watch?v=fsDITf6s0WY