bluuebunny/crossref_metadata_2025 huggingface dataset:
Early arrival at the emergency department is associated with better collaterals, smaller established infarcts and better clinical outcomes with endovascular stroke therapy: SWIFT study
Authors: Liebeskind David S , Jahan Reza , Nogueira Raul G , Jovin Tudor G , Lutsep Helmi L , Saver Jeffrey L
Published: May 2015

Background and purpose

Increasing time from symptom onset to emergency department arrival may incur greater ischemic injury and decreased likelihood of good outcomes after acute stroke therapy. The impact of time may be assessed bythe extent of acute CT changes, status of collateral vessels, and clinical outcomes.

Methods

The SOLITAIRE FR With the Intention For Thrombectomy (SWIFT) trial comparing two neurothrombectomy treatments was analyzed by time, Alberta Stroke Program Early CT Scores (ASPECTS), angiographic collaterals, and 90-day modified Rankin Scale outcomes. We determined the interaction of time with ASPECTS, collateral grade, reperfusion, and clinical outcomes, with established determinants of angiographic and clinical outcomes as covariates.

Results

137 patients (52% female) of mean age 67±12 years and median pretreatment NIH Stroke Scale score 18 (range 8–28) were enrolled. Median onset to door (OTD) time was 180 min (IQR 95–250). Presentation within 3 h of last known well was associated with absence of any prestroke disability and presence of atrial fibrillation but was unrelated to age, sex, other vascular risk factors, deficit severity, glucose level, or blood pressure. Worse collaterals were noted with longer OTD intervals: collateral grade 0–1 (n=32): mean 232±84 min; grade 2 (n=48): 164±99 min; grade 3 (n=35): 155±104 min; grade 4 (n=4): 54±16 min (p<0.001). Later presentation was associated with more extensive early infarct imaging changes (median ASPECTS 8 (IQR 7–9) >3 h vs 9 (IQR 8–10) <3 h, p=0.015). Multivariable analyses identified time >3 h as the only predictor of extensive infarct on imaging (ASPECTS ≤7), p=0.003. Earlier presentation was strongly associated with better 90-day modified Rankin Scale outcomes (p<0.001).

Conclusions

Time was a critical factor in successful clinical outcomes for neurothrombectomy in the SWIFT trial. Shorter times to presentation were associated with better collaterals, smaller established infarcts, and better clinical outcome after revascularization.
Sodium bicarbonate supplementation improved MAOD but is not correlated with 200- and 400-m running performances: a double-blind, crossover, and placebo-controlled study
Authors: Brisola Gabriel Motta Pinheiro , Miyagi Willian Eiji , da Silva Henrique Santos , Zagatto Alessandro Moura
Published: May 2015

The aim of the study was to investigate the effects of acute supplementation of sodium bicarbonate (NaHCO3) on maximal accumulated oxygen deficit (MAOD) determined by a single supramaximal effort (MAODALT) in running and the correlation with 200- and 400-m running performances. Fifteen healthy men (age, 23 ± 4 years; maximal oxygen uptake, 50.6 ± 6.1 mL·kg−1·min−1) underwent a maximal incremental exercise test and 2 supramaximal efforts at 110% of the intensity associated with maximal oxygen uptake, which was carried out after ingesting either 0.3 g·kg−1body weight NaHCO3or a placebo (dextrose) and completing 200- and 400-m performance tests. The study design was double-blind, crossover, and placebo-controlled. Significant differences were found between the NaHCO3and placebo conditions for MAODALT(p = 0.01) and the qualitative inference for substantial changes showed a very likely positive effect (98%). The lactic anaerobic contribution in the NaHCO3ingestion condition was significantly higher (p < 0.01) and showed a very likely positive effect (99% chance), similar to that verified for peak blood lactate concentration (p < 0.01). No difference was found for time until exhaustion (p = 0.19) or alactic anaerobic contribution (p = 0.81). No significant correlations were observed between MAODALTand 200- and 400-m running performance tests. Therefore, we can conclude that both MAODALTand the anaerobic lactic metabolism are modified after acute NaHCO3ingestion, but it is not correlated with running performance.
Multi-scale hydrogeologic characterization of a leaky till–mantled fractured bedrock aquifer system
Authors: Lukas William G. , DeGroot Don J. , Ostendorf David W. , Hinlein Erich S.
Published: May 2015

The paper presents hydrogeologic properties for a leaky till–mantled fractured bedrock aquifer system based on geophysical and hydraulic tests performed at a drumlin located in northeastern Massachusetts, USA. The site profile consists of a fractured bedrock aquifer overlain by a 30 m thick unweathered, coarse-grained till aquitard. Steady state, decadal scale, hydraulics varied little until seasonal irrigation pumping was initiated in recent years, causing a substantial annual drawdown in the aquifer and leakage from the overlying till. High frequency hydraulic head data sets collected in monitoring wells record the hydraulic response to the irrigation pumping. These data sets, together with results from small scale slug and purge tests performed in monitoring wells, are used to characterize the hydrogeologic behavior of this groundwater system. Geophysical logging performed in bedrock wells confirmed the presence of numerous flowing fractures. The large-scale continuum analysis of the fractured bedrock aquifer response to the irrigation pumping yields transmissivity values consistent with those determined from the small-scale, short-term purge test results. The low hydraulic conductivity till has a significant impact on the drawdown behavior of the fractured bedrock aquifer. Calibrated values from the collective data sets and analyses result in the following properties for the 30 m thick unweathered till: hydraulic conductivity K′ = 7.2 × 10−9m/s, transmissivity T′ = 2.3 × 10−8m2/s, and storativity S′ = 2.7 × 10−4, and for the underlying fractured bedrock aquifer: T = 6.5 × 10−6m2/s with an average fracture aperture of 46 μm and hydraulic conductivity Kf= 1.3 × 10−3m/s. These results should describe similar unweathered coarse-grained till–mantled fractured bedrock aquifer systems and provide useful data for preliminary analyses prior to any site-specific investigations.
Early root and aboveground biomass development of hybrid poplars (Populusspp.) under drought conditions
Authors: Krabel Doris , Meyer Matthias , Solger Alexander , Müller Rosi , Carvalho Pedro , Foulkes John
Published: May 2015

Currently, the genus Populus is one of the favourite objects for research of molecular genetics of woody plants. A high growth rate and the broadly applicable timber as raw material for different types of products made of wood make poplar attractive for industrial usage. Despite the positive aspect of its growth capacity and wood composition, one major problem in cultivating fast-growing tree species in a forestry plantation system is the comparably high water demand of the plants. In this context, a rapid development of an efficient adventitious root system from dormant hardwood cuttings is an essential requirement for the successful establishment of short-rotation cultures. It reduces the establishment costs of plantations, and the developing plant can be transferred into favourable conditions due to varying environmental conditions. Results of greenhouse pot and soil-column experiments on the development of shoots and adventitious roots from hardwood cuttings of seven hybrid poplar cultivars and the reaction of the plants performance on varying water availability will be presented. We estimated root and shoot length, root and shoot growth and biomass accumulation over time, root-to-shoot length ratio, and root morphological traits.
History of hadrontherapy
Authors: Amaldi Ugo
Published: May 2015

Hadrontherapy is today an established modality in cancer radiation therapy. Based on the superior ballistic and radiobiological properties of accelerated ions, this discipline experienced a remarkable growth in the last 20 years. This paper reviews the history of hadrontherapy, from the early days to the most recent developments. In particular, the evolution of proton and carbon ion therapy is presented together with a glance at future solutions such as single-room facilities.
Nonlocal quantum field theory without acausality and nonunitarity at quantum level: Is SUSY the key?
Authors: Addazi Andrea , Esposito Giampiero
Published: May 2015

The realization of a nonlocal quantum field theory without losing unitarity, gauge invariance and causality is investigated. It is commonly retained that such a formulation is possible at tree level, but at quantum level acausality is expected to reappear at one loop. We suggest that the problem of acausality is, in a broad sense, similar to the one about anomalies in quantum field theory. By virtue of this analogy, we suggest that acausal diagrams resulting from the fermionic sector and the bosonic one might cancel each other, with a suitable content of fields and suitable symmetries. As a simple example, we show how supersymmetry can alleviate this problem in a simple and elegant way, i.e. by leading to exact cancellations of harmful diagrams, to all orders of perturbation theory. An infinite number of divergent diagrams cancel each other by virtue of the nonrenormalization theorem of supersymmetry. However, supersymmetry is not enough to protect a theory from all acausal divergences. For instance, acausal contributions to supersymmetric corrections to D-terms are not protected by supersymmetry. On the other hand, we show in detail how supersymmetry also helps in dealing with D-terms: divergences are not canceled but they become softer than in the nonsupersymmetric case. The supergraphs' formalism turns out to be a powerful tool to reduce the complexity of perturbative calculations.
Impurity-related nonlinear optical absorption under combined effects of intense laser field and band-edge nonparabolicity on InGaN QW
Authors: El Ghazi Haddou , Peter A. John
Published: May 2015

Conduction band-edge nonparabolicity effect on linear and nonlinear optical properties related to 1s–1p intra-conduction band transition in unstrained wurtzite (In, Ga)N–GaN symmetric quantum well (QW) is investigated incorporating an additional external probe as well as the nonresonant intense laser field (ILF) effect. Using the compact density matrix approach and the iterative procedure, the analytical expressions of optical absorption coefficients (ACs) are calculated. The numerical results are obtained within the single-band effective mass and the one-parabolic-band approximations under finite potential barrier. It is found that the internal and external perturbations show an important impact on the optical spectrum. A critical value of the laser-dressed parameter (LDP) is obtained by limiting two behaviors. Moreover, the ILF can be used as a way to control the optical properties of the QW structures and to reduce the lift of the conduction band-edge.
Estimation of Reliability for Parallel Networked Phased Mission Systems with Unobserved Subsystem Operational Times
Authors: Rani Monika , Jain Kanchan , Dewan Isha
Published: May 2015

A complex system consisting of k phases is considered in this study. Its functioning is such that the control shifts sequentially within different phases to complete their assigned task. Missiles, rockets and electronic exploders used to fire electric detonators are examples of such systems. The components in different subsystems are in a parallel configuration. Their lifetimes are assumed to be independent and identical random variables that follow exponential distribution. The distribution function of system operational time is obtained when all subsystem operational times are unobserved. The method of maximum likelihood is used to estimate unknown parameter of system operational time's distribution. An estimate of system reliability is provided through simulations.
Comparing Feature Selection Techniques for Software Quality Estimation Using Data-Sampling-Based Boosting Algorithms
Authors: Khoshgoftaar Taghi M. , Gao Kehan , Chen Ye , Napolitano Amri
Published: May 2015

Software defect prediction is a classification technique that utilizes software metrics and fault data collected during the software development process to identify fault-prone modules before the testing phase. It aims to optimize project resource allocation and eventually improve the quality of software products. However, two factors, high dimensionality and class imbalance, may cause low quality training data and subsequently degrade classification models. Feature (software metric) selection and data sampling are frequently used to overcome these problems. Feature selection (FS) is a process of choosing a subset of relevant features so that the quality of prediction models can be maintained or improved. Data sampling alters the dataset to change its balance level, therefore alleviating the problem of traditional classification models that are biased toward the overrepresented (majority) class. A recent study shows that another method, called boosting (building multiple models, with each model tuned to work better on instances misclassified by previous models), is also effective for addressing the class imbalance problem. In this paper, we present a technique that uses FS followed by a boosting algorithm in the context of software quality estimation. We investigate four FS approaches: individual FS, repetitive sampled FS, sampled ensemble FS, and repetitive sampled ensemble FS, and study the impact of the four approaches on the quality of the prediction models. Ten base feature ranking techniques are examined in the case study. We also employ the boosting algorithm to construct classification models with no FS and use the results as the baseline for further comparison. The empirical results demonstrate that (1) FS is important and necessary prior to the learning process; (2) the repetitive sampled FS method generally has similar performance to the individual FS technique; and (3) the ensemble filter (including sampled ensemble filter and repetitive sampled ensemble filter) performs better than or similarly to the average of the corresponding individual base rankers.
Exploiting FPGA Block Memories for Protected Cryptographic Implementations
Authors: Bhasin Shivam , Danger Jean-Luc , Guilley Sylvain , He Wei
Published: May 2015

Modern field programmable gate arrays (FPGAs) are power packed with features to facilitate designers. Availability of features like large block memory (BRAM), digital signal processing cores, and embedded CPU makes the design strategy of FPGAs quite different from ASICs. FPGAs are also widely used in security-critical applications where protection against known attacks is of prime importance. We focus on physical attacks that target physical implementations. To design countermeasures against such attacks, the strategy for FPGA designers should be different from that in ASIC. The available features should be exploited to design compact and strong countermeasures. In this article, we propose methods to exploit the BRAMs in FPGAs for designing compact countermeasures. Internal BRAM can be used to optimize intrinsic countermeasures such as masking and dual-rail logics, which otherwise have significant overhead (at least 2 × ) compared to unprotected ones. The optimizations are applied on a real AES-128 co-processor and tested for area overhead and resistance on Xilinx Virtex-5 chips. The presented masking countermeasure has an overhead of only 16% when applied on AES. Moreover, the dual-rail precharge logic (DPL) countermeasure has been optimized to pack the whole sequential part in the BRAM, hence enhancing the security. Proper robustness evaluations are conducted to analyze the optimization in terms of area and security.
Smoothed Complexity Theory
Authors: Bläser Markus , Manthey Bodo
Published: May 2015

Smoothed analysis is a new way of analyzing algorithms introduced by Spielman and Teng. Classical methods like worst-case or average-case analysis have accompanying complexity classes, such as P and Avg-P, respectively. Whereas worst-case or average-case analysis give us a means to talk about the running time of a particular algorithm, complexity classes allow us to talk about the inherent difficulty of problems.

Smoothed analysis is a hybrid of worst-case and average-case analysis and compensates some of their drawbacks. Despite its success for the analysis of single algorithms and problems, there is no embedding of smoothed analysis into computational complexity theory, which is necessary to classify problems according to their intrinsic difficulty.

We propose a framework for smoothed complexity theory, define the relevant classes, and prove some first hardness results (of bounded halting and tiling) and tractability results (binary optimization problems, graph coloring, satisfiability) within this framework.
Experience report
Authors: Blanchette Jasmin Christian , Hupel Lars , Nipkow Tobias , Noschinski Lars , Traytel Dmitriy
Published: May 2015

We report on our experience teaching a Haskell-based functional programming course to over 1100 students for two winter terms. The syllabus was organized around selected material from various sources. Throughout the terms, we emphasized correctness through QuickCheck tests and proofs by induction. The submission architecture was coupled with automatic testing, giving students the possibility to correct mistakes before the deadline. To motivate the students, we complemented the weekly assignments with an informal competition and gave away trophies in a award ceremony.
Promoting functions to type families in Haskell
Authors: Eisenberg Richard A. , Stolarek Jan
Published: May 2015

Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including
case
expressions, anonymous functions, partially-applied functions, and
let
expressions. In this paper, we present an algorithm - with a proof of correctness - to encode these term-level constructs at the type level. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement.

We believe that delineating the mismatch between GHC's term level and its type level is a key step toward supporting dependently typed programming.
Experience report
Authors: Muranushi Takayuki , Eisenberg Richard A.
Published: May 2015

Many of the bugs in scientific programs have their roots in mistreatment of physical dimensions, via erroneous expressions in the quantity calculus. Now that the type system in the Glasgow Haskell Compiler is rich enough to support type-level integers and other promoted datatypes, we can type-check the quantity calculus in Haskell. In addition to basic dimension-aware arithmetic and unit conversions, our units library features an extensible system of dimensions and units, a notion of dimensions apart from that of units, and unit polymorphism designed to describe the laws of physics. We demonstrate the utility of units by writing an astrophysics research paper. This work is free of unit concerns because every quantity expression in the paper is rigorously type-checked.
SmartCheck
Authors: Pike Lee
Published: May 2015

QuickCheck is a powerful library for automatic test-case generation. Because QuickCheck performs random testing, some of the counterexamples discovered are very large. QuickCheck provides an interface for the user to write shrink functions to attempt to reduce the size of counter examples. Hand-written implementations of shrink can be complex, inefficient, and consist of significant boilerplate code. Furthermore, shrinking is only one aspect in debugging: counterexample generalization is the process of extrapolating from individual counterexamples to a class of counterexamples, often requiring a flash of insight from the programmer. To improve counterexample reduction and generalization, we introduce
SmartCheck
. SmartCheck is a debugging tool that reduces algebraic data using generic search heuristics to efficiently find smaller counterexamples. In addition to shrinking, SmartCheck also automatically generalizes counterexamples to formulas representing classes of counterexamples. SmartCheck has been implemented for Haskell and is freely available.
Embedding effect systems in Haskell
Authors: Orchard Dominic , Petricek Tomas
Published: May 2015

Monads are now an everyday tool in functional programming for abstracting and delimiting effects. The link between monads and effect systems is well-known, but in their typical use, monads provide a much more coarse-grained view of effects. Effect systems capture fine-grained information about the effects, but monads provide only a binary view:
effectful
or
pure
.

Recent theoretical work has unified fine-grained effect systems with monads using a monad-like structure indexed by a monoid of effect annotations (called parametric effect monads). This aligns the power of monads with the power of effect systems.

This paper leverages recent advances in Haskell's type system (as provided by GHC) to embed this approach in Haskell, providing user-programmable effect systems. We explore a number of practical examples that make Haskell even better and safer for effectful programming. Along the way, we relate the examples to other concepts, such as Haskell's implicit parameters and
coeffects
.
Demo proposal
Authors: Levy Amit A. , Terei David , Stefan Deian , Maziéres David
Published: May 2015

Simple is a web framework for Haskell. Simple came out of our work on Hails, a platform for secure web applications. For Hails, we needed a flexible web framework that uses no unsafe language features and can be used to build apps outside the IO monad. Unlike many mainstream web frameworks, Simple does not enforce a particular structure or paradigm. Instead, it simply provides a set of composable building blocks to help developers structure and organize their web applications.

We've used Simple to build both traditional web applications as well as applications with explicit, strong safety and security guarantees. In the demonstration, we'll focus on the former -- introducing the framework and motivating it's utility for traditional web apps -- and show how we can leverage the LIO information flow control library to add mandatory security policies to apps.
Sound Modular Verification of C Code Executing in an Unverified Context
Authors: Agten Pieter , Jacobs Bart , Piessens Frank
Published: May 2015

Over the past decade, great progress has been made in the static modular verification of C code by means of separation logic-based program logics. However, the runtime guarantees offered by such verification are relatively limited when the verified modules are part of a whole program that also contains unverified modules. In particular, a memory safety error in an unverified module can corrupt the runtime state, leading to assertion failures or invalid memory accesses in the verified modules. This paper develops runtime checks to be inserted at the boundary between the verified and the unverified part of a program, to guarantee that no assertion failures or invalid memory accesses can occur at runtime in any verified module. One of the key challenges is enforcing the separation logic frame rule, which we achieve by checking the integrity of the footprint of the verified part of the program on each control flow transition from the unverified to the verified part. This in turn requires the presence of some support for module-private memory at runtime. We formalize our approach and prove soundness. We implement the necessary runtime checks by means of a program transformation that translates C code with separation logic annotations into plain C, and that relies on a protected module architecture for providing module-private memory and restricted module entry points. Benchmarks show the performance impact of this transformation depends on the choice of boundary between the verified and unverified parts of the program, but is below 4% for real-world applications.
A Meta Lambda Calculus with Cross-Level Computation
Authors: Tobisawa Kazunori
Published: May 2015

We propose meta lambda calculus Lambda-* as a basic model of textual substitution via metavariables. The most important feature of the calculus is that every beta-redex can be reduced regardless of whether the beta-redex contains meta-level variables or not. Such a meta lambda calculus has never been achieved before due to difficulty to manage binding structure consistently with alpha-renaming in the presence of meta-level variables. We overcome the difficulty by introducing a new mechanism to deal with substitution and binding structure in a systematic way without the notion of free variables and alpha-renaming.

Calculus Lambda-* enables us to investigate cross-level terms that include a certain type of level mismatch. Cross-level terms have been regarded as meaningless terms and left out of consideration thus far. We find that some cross-level terms behave as quotes and `eval' command in programming languages. With these terms, we show a procedural language as an application of the calculus, which sheds new light on the notions of stores and recursion via meta-level variables.
A Calculus for Relaxed Memory
Authors: Crary Karl , Sullivan Michael J.
Published: May 2015

We propose a new approach to programming multi-core, relaxed-memory architectures in imperative, portable programming languages. Our memory model is based on explicit, programmer-specified requirements for order of execution and the visibility of writes. The compiler then realizes those requirements in the most efficient manner it can. This is in contrast to existing memory models, which---if they allow programmer control over synchronization at all---are based on inferring the execution and visibility consequences of synchronization operations or annotations in the code.

We formalize our memory model in a core calculus called RMC\@. Outside of the programmer's specified requirements, RMC is designed to be strictly more relaxed than existing architectures. It employs an aggressively nondeterministic semantics for expressions, in which actions can be executed in nearly any order, and a store semantics that generalizes Sarkar et al.'s and Alglave et al.'s models of the Power architecture. We establish several results for RMC, including sequential consistency for two programming disciplines, and an appropriate notion of type safety. All our results are formalized in Coq.
Compositional CompCert
Authors: Stewart Gordon , Beringer Lennart , Cuellar Santiago , Appel Andrew W.
Published: May 2015

This paper reports on the development of Compositional CompCert, the first verified separate compiler for C.

Specifying and proving separate compilation for C is made challenging by the coincidence of: compiler optimizations, such as register spilling, that introduce compiler-managed (private) memory regions into function stack frames, and C's stack-allocated addressable local variables, which may leak portions of stack frames to other modules when their addresses are passed as arguments to external function calls. The CompCert compiler, as built/proved by Leroy
etal
2006--2014, has proofs of correctness for whole programs, but its simulation relations are too weak to specify or prove separately compiled modules.

Our technical contributions that make Compositional CompCert possible include: language-independent linking, a new operational model of multilanguage linking that supports strong semantic contextual equivalences; and structured simulations, a refinement of Beringer
etal
logical simulation relations that enables expressive module-local invariants on the state communicated between compilation units at runtime. All the results in the paper have been formalized in Coq and are available for download together with the Compositional CompCert compiler.
Decentralizing SDN Policies
Authors: Padon Oded , Immerman Neil , Karbyshev Aleksandr , Lahav Ori , Sagiv Mooly , Shoham Sharon
Published: May 2015

Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically-centralized control over network devices through a "controller" --- software that operates independently of the network hardware. Network operators can run both in-house and third-party SDN programs on top of the controller, e.g., to specify routing and access control policies.

In practice, having the controller handle events limits the network scalability. Therefore, the feasibility of SDN depends on the ability to efficiently decentralize network event-handling by installing forwarding rules on the switches. However, installing a rule too early or too late may lead to incorrect behavior, e.g., (1) packets may be forwarded to the wrong destination or incorrectly dropped; (2) packets handled by the switch may hide vital information from the controller, leading to incorrect forwarding behavior. The second issue is subtle and sometimes missed even by experienced programmers.

The contributions of this paper are two fold. First, we formalize the correctness and optimality requirements for decentralizing network policies. Second, we identify a useful class of network policies which permits automatic synthesis of a controller which performs optimal forwarding rule installation.
Dependent Information Flow Types
Authors: Lourenço Luísa , Caires Luís
Published: May 2015

In this paper, we develop a novel notion of dependent information flow types. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values.

Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs, including programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields, still considered a challenge to security enforcement in software systems such as data-centric web-based applications.

We base our development on the very general setting of a minimal lambda-calculus with references and collections. We illustrate its expressiveness, showing how secure operations on relevant scenarios can be modelled and analysed using our dependent information flow type system, which is also shown to be amenable to algorithmic type checking. Our main results include type-safety and non-interference theorems ensuring that well-typed programs do not violate prescribed security policies.
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it
Authors: Vafeiadis Viktor , Balabonski Thibaut , Chakraborty Soham , Morisset Robin , Zappa Nardelli Francesco
Published: May 2015

We show that the weak memory model introduced by the 2011 C and C++ standards does not permit many common source-to-source program transformations (such as expression linearisation and "roach motel" reorderings) that modern compilers perform and that are deemed to be correct. As such it cannot be used to define the semantics of intermediate languages of compilers, as, for instance, LLVM aimed to. We consider a number of possible local fixes, some strengthening and some weakening the model. We evaluate the proposed fixes by determining which program transformations are valid with respect to each of the patched models. We provide formal Coq proofs of their correctness or counterexamples as appropriate.
Manifest Contracts for Datatypes
Authors: Sekiyama Taro , Nishida Yuki , Igarashi Atsushi
Published: May 2015

We study algebraic data types in a manifest contract system, a software contract system where contract information occurs as refinement types. We first compare two simple approaches: refinements on type constructors and refinements on data constructors. For example, lists of positive integers can be described by {l:int list | for_all (lambda y. y > 0) l} in the former, whereas by a user-defined datatype pos_list with cons of type {x:int | x > 0} X pos_list -> pos_list in the latter. The two approaches are complementary: the former makes it easier for a programmer to write types and the latter enables more efficient contract checking. To take the best of both worlds, we propose (1) a syntactic translation from refinements on type constructors to equivalent refinements on data constructors and (2) dynamically checked casts between different but compatible datatypes such as int list and pos_list. We define a manifest contract calculus to formalize the semantics of the casts and prove that the translation is correct.
Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks
Authors: Tang Hao , Wang Xiaoyin , Zhang Lingming , Xie Bing , Zhang Lu , Mei Hong
Published: May 2015

Building a summary for library code is a common approach to speeding up the analysis of client code. In presence of callbacks, some reachability relationships between library nodes cannot be obtained during library-code summarization. Thus, the library code may have to be analyzed again during the analysis of the client code with the library summary. In this paper, we propose to summarize library code with tree-adjoining-language (TAL) reachability. Compared with the summary built with context-free-language (CFL) reachability, the summary built with TAL reachability further contains conditional reachability relationships. The conditional reachability relationships can lead to much lighter analysis of the library code during the client code analysis with the TAL-reachability-based library summary. We also performed an experimental comparison of context-sensitive data-dependence analysis with the TAL-reachability-based library summary and context-sensitive data-dependence analysis with the CFL-reachability-based library summary using 15 benchmark subjects. Our experimental results demonstrate that the former has an 8X speed-up over the latter on average.
From Network Interface to Multithreaded Web Applications
Authors: Chlipala Adam
Published: May 2015

Many verifications of realistic software systems are monolithic, in the sense that they define single global invariants over complete system state. More modular proof techniques promise to support reuse of component proofs and even reduce the effort required to verify one concrete system, just as modularity simplifies standard software development. This paper reports on one case study applying modular proof techniques in the Coq proof assistant. To our knowledge, it is the first modular verification certifying a system that combines infrastructure with an application of interest to end users. We assume a nonblocking API for managing TCP networking streams, and on top of that we work our way up to certifying multithreaded, database-backed Web applications. Key verified components include a cooperative threading library and an implementation of a domain-specific language for XML processing. We have deployed our case-study system on mobile robots, where it interfaces with off-the-shelf components for sensing, actuation, and control.
Differential Privacy
Authors: Ebadi Hamid , Sands David , Schneider Gerardo
Published: May 2015

Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge.

Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction.

This paper is about a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy (PDP). In PDP each individual has its own personal privacy level. We describe ProPer, a interactive system for implementing PDP which maintains a privacy budget for each individual. When a primitive query is made on data derived from individuals, the provenance of the involved records determines how the privacy budget of an individual is affected: the number of records derived from Alice determines the multiplier for the privacy decrease in Alice's budget. This offers some advantages over previous systems, in particular its fine-grained character allows better utilisation of the privacy budget than mechanisms based purely on the concept of global sensitivity, and it applies naturally to the case of a live database where new individuals are added over time.

We provide a formal model of the ProPer approach, prove that it provides personalised differential privacy, and describe a prototype implementation based on McSherry's PINQ system.
Fiat
Authors: Delaware Benjamin , Pit-Claudel Clément , Gross Jason , Chlipala Adam
Published: May 2015

We present Fiat, a library for the Coq proof assistant supporting refinement of declarative specifications into efficient functional programs with a high degree of automation. Each refinement process leaves a proof trail, checkable by the normal Coq kernel, justifying its soundness. We focus on the synthesis of abstract data types that package methods with private data. We demonstrate the utility of our framework by applying it to the synthesis of query structures -- abstract data types with SQL-like query and insert operations. Fiat includes a library for writing specifications of query structures in SQL-inspired notation, expressing operations over relations (tables) in terms of mathematical sets. This library includes a suite of tactics for automating the refinement of specifications into efficient, correct-by-construction OCaml code. Using these tactics, a programmer can generate such an implementation completely automatically by only specifying the equivalent of SQL indexes, data structures capturing useful views of the abstract data. Throughout we speculate on the new programming modularity possibilities enabled by an automated refinement system with proved-correct rules.
Predicting Program Properties from "Big Code"
Authors: Raychev Veselin , Vechev Martin , Krause Andreas
Published: May 2015

We present a new approach for predicting program properties from massive codebases (aka "Big Code"). Our approach first learns a probabilistic model from existing data and then uses this model to predict properties of new, unseen programs.

The key idea of our work is to transform the input program into a representation which allows us to phrase the problem of inferring program properties as structured prediction in machine learning. This formulation enables us to leverage powerful probabilistic graphical models such as conditional random fields (CRFs) in order to perform joint prediction of program properties.

As an example of our approach, we built a scalable prediction engine called JSNice for solving two kinds of problems in the context of JavaScript: predicting (syntactic) names of identifiers and predicting (semantic) type annotations of variables. Experimentally, JSNice predicts correct names for 63% of name identifiers and its type annotation predictions are correct in 81% of the cases. In the first week since its release, JSNice was used by more than 30,000 developers and in only few months has become a popular tool in the JavaScript developer community.

By formulating the problem of inferring program properties as structured prediction and showing how to perform both learning and inference in this context, our work opens up new possibilities for attacking a wide range of difficult problems in the context of "Big Code" including invariant generation, decompilation, synthesis and others.
Databases and Programming
Authors: Buneman Peter
Published: May 2015

The 1990s saw a hugely productive interaction between database and programming language research. Ideas about type systems from programming languages played a central role in generalizing and adapting relational database systems to new data models. At the same time databases provided some of the best concrete examples of the application of concurrency theory and of the benefits of high-level optimization in functional programming languages. One of the driving ambitions behind this research was the idea that database access should be properly embedded in programming languages: one should not have to be bilingual in order to use a database from a programming language; and that goal has to some extent been realized.

In the past fifteen years, new data models, both for data storage and for data exchange have appeared with depressing regularity and with each such model, the inevitable query language. Does programming language research have anything to contribute to these new languages? Should we take the time to to worry about embedding these models in conventional languages? Over the same period, some interesting new connections between databases and programming languages have emerged, notably in the areas of scientific databases, annotation and provenance. Will this provide new opportunities for cross-fertilization?
Automating Repetitive Tasks for the Masses
Authors: Gulwani Sumit
Published: May 2015

The programming languages (PL) research community has traditionally catered to the needs of professional programmers in the continuously evolving technical industry. However, there is a new opportunity that knocks our doors. The recent IT revolution has resulted in the masses having access to personal computing devices. More than 99% of these computer users are non-programmers and are today limited to being passive consumers of the software that is made available to them. Can we empower these users to more effectively leverage computers for their daily tasks? The formalisms, techniques, and tools developed in the PL and the formal methods research communities can play a pivotal role!
Comparative Study of Malaria Prevalence among Travellers in Nigeria (West Africa) Using Slide Microscopy and a Rapid Diagnosis Test
Authors: Dougnon T. V. , Bankole H. S. , Hounmanou Y. M. G. , Echebiri S. , Atchade P. , Mohammed J.
Published: May 2015

Malaria is a major disease in Africa and leads to various public health problems. A study was carried out at the Aviation Medical Clinic Laboratory, Murtala Mohammed Airport, Ikeja, Lagos State, Nigeria, in 2014. The work aimed to determine the prevalence of malaria among patients attending the laboratory. Blood samples were therefore collected from 51 patients and subjected to both blood smear microscopy and a rapid immunochromatographic diagnostic test (SD BIOLINE Malaria Ag) for detection of, respectively, malaria parasites and antigens. At the end of the study, 22% of the patients were detected positive by the microscopic examination while 9.8% were tested positive when using SD BIOLINE Malaria Ag. The outcomes of the study show a high prevalence of malaria at the airport. This represents a serious risk factor leading to a high likelihood of spread and occurrence of malaria in other countries including Western countries whereby the disease is nonendemic. It also pointed out that the blood smear microscopy seems to be better than Rapid Diagnosis Test (RDT) for malaria diagnosis.
Power Forecasting of Combined Heating and Cooling Systems Based on Chaotic Time Series
Authors: Hai Liu , Yong Song , Qingfu Du
Published: May 2015

Theoretic analysis shows that the output power of the distributed generation system is nonlinear and chaotic. And it is coupled with the microenvironment meteorological data. Chaos is an inherent property of nonlinear dynamic system. A predicator of the output power of the distributed generation system is to establish a nonlinear model of the dynamic system based on real time series in the reconstructed phase space. Firstly, chaos should be detected and quantified for the intensive studies of nonlinear systems. If the largest Lyapunov exponent is positive, the dynamical system must be chaotic. Then, the embedding dimension and the delay time are chosen based on the improved C-C method. The attractor of chaotic power time series can be reconstructed based on the embedding dimension and delay time in the phase space. By now, the neural network can be trained based on the training samples, which are observed from the distributed generation system. The neural network model will approximate the curve of output power adequately. Experimental results show that the maximum power point of the distributed generation system will be predicted based on the meteorological data. The system can be controlled effectively based on the prediction.
Evaluation of Ovarian Reserve with Anti-Müllerian Hormone in Familial Mediterranean Fever
Authors: Şahin Ali , Karakuş Savaş , Durmaz Yunus , Yıldız Çağlar , Aydın Hüseyin , Cengiz Ahmet Kıvanç , Güler Duygu
Published: May 2015

Objective. To investigate ovarian reserves in attack-free familial Mediterranean fever (AF-FMF) patients at the reproductive age by anti-Müllerian hormone (AMH), antral follicle count (AFC), ovarian volume, and hormonal parameters.Methods. Thirty-three AF-FMF patients aging 18–45 years and 34 healthy women were enrolled and FSH, LH, E2, PRL, and AMH levels were measured in the morning blood samples at 2nd–4th days of menstruation by ELISA. Concomitant pelvic ultrasonography was performed to calculate AFC and ovarian volumes.Results. In FMF patient group, median AMH levels were statistically significantly lower in the M69V mutation positive group than in the negative ones (P=0.018). There was no statistically significant difference in median AMH levels between E148Q mutation positive patients and the negative ones (P=0.920). There was also no statistically significant difference in median AMH levels between M680I mutation positive patients and the negative ones (P=0.868). No statistically significant difference was observed in median AMH levels between patients who had at least one mutation and those with no mutations (P=0.868). We realized that there was no difference in comparisons between ovarian volumes, number of follicles, and AMH levels ovarian reserves when compared with FMF patients and healthy individuals.Conclusions. Ovarian reserves of FMF pateints were similar to those of healthy subjects according to AMH. However, AMH levels were lower in FMF patients with M694V mutation.
The Characteristics of Antioxidant Activity after Liver Transplantation in Biliary Atresia Patients
Authors: Chen Chih-Jen , Tang Kuo-Shu , Huang Ying-Hsien , Chen Chao-Long , Huang Li-Tung , Chuang Jiin-Haur , Tiao Mao-Meng
Published: May 2015

Purpose. Cholestatic liver injury is associated with a high production of free radicals. The pathogenesis of liver injury in biliary atresia (BA) patients is largely undefined. The goal of the present study was to clarify the oxidative damage and the changes in antioxidant enzyme activities that occur during the development of BA and after liver transplantation (LT).Methods. We enrolled BA patients and control subjects and collected their clinical information. The activities of antioxidant enzymes in BA patients before LT (BA group) and after LT (LT group) were analyzed.Results. The number of mitochondrial DNA copies had increased in the LT group compared with the BA group. Similarly, the activity of glutathione peroxidase had increased in the LT group compared with the BA group. The level of glutathione was higher in the LT group than in the BA group. Malondialdehyde levels were decreased in the LT group compared with the BA group.Conclusions. These data indicate that LT is associated with increased antioxidant enzyme activities and decreased malondialdehyde levels in BA patients. The manipulation of mitochondria-associated antioxidative activity might be an important future management strategy for BA.