bluuebunny/crossref_metadata_2025_split huggingface dataset:
Interventions associated with drowning prevention in children and adolescents: systematic literature review
Authors: Wallis Belinda A , Watt Kerrianne , Franklin Richard C , Taylor Monica , Nixon James W , Kimble Roy M 
Published: September 2014

IntroductionDrowning remains a leading cause of preventable death in children across the world. This systematic review identifies and critically analyses studies of interventions designed to reduce fatal and non-fatal drowning events among children and adolescents or reduce the injury severity incurred by such incidents.MethodsA systematic search was undertaken on literature published between 1980 and 2010 relating to interventions around fatal and non-fatal drowning prevention in children and adolescents 0–19 years of age. Search methods and protocols developed and used by the WHO Global Burden of Disease Injury Expert Group were applied.ResultsSeven studies fulfilled the inclusion criteria. Interventions were categorised into three themes of Education, Swimming Lessons and Water Safety, and Pool Fencing. All are possible effective strategies to prevent children from drowning, particularly young children aged 2–4 years, but very little evidence exists for interventions to reduce drowning in older children and adolescents. There were methodological limitations associated with all studies, so results need to be interpreted in the context of these.ConclusionsRelatively few studies employ rigorous methods and high levels of evidence to assess the impact of interventions designed to reduce drowning. Studies are also limited by lack of consistency in measured outcomes and drowning terminology. Further work is required to establish efficacy of interventions for older children and adolescents. There is a need for rigorous, well-designed studies that use consistent terminology to demonstrate effective prevention solutions.
Care pathways for UK and US service personnel who are visually impaired
Authors: Malcolm Estelle , Stevelink S A M , Fear N T 
Published: September 2014

ObjectivesThe aim of this paper is to outline the different care pathways for sudden and gradual vision loss within UK and US military systems, as well as the provision of support by the main third-sector organisations looking after visually impaired (ex-) service personnel.MethodsThe Defence Medical Rehabilitation Centre, Headley Court and Queen Elizabeth Hospital Birmingham were consulted to obtain information and relevant documentation on UK care pathways. Experts in the field of visual impairment and the military-provided information on care pathways for US service personnel were consulted. The majority of the information on US care pathways was gathered from the Department of Veterans Affairs website and unclassified documents.ResultsThe care pathways for UK and US service personnel with a visual impairment vary depending on the cause of visual impairment. Blind Veterans UK and the Blinded Veterans Association are the main organisations that support UK and US (ex-) service personnel, often filling in the gaps that other services do not have the resources to provide. The main difference between the two pathways, other than the UK healthcare system being free at the point of service, is that the Veteran Health Administration is one of the first national healthcare systems to integrate rehabilitation services for personnel with a visual impairment into the health services provided.DiscussionThe UK could benefit from having specific care coordinators for service personnel that specifically integrate rehabilitation, medical care and treatment for their visual impairment.
A Refinement Technique for Duplication and Collision Between Features in Software Product Line Engineering
Authors: Song Cheeyang , Lee Soonbok , Lee Woojin 
Published: September 2014

In software product line engineering (SPLE), many studies have been conducted on commonality- and variability-based feature extraction methods and on the reasoning and refinement of feature models (FMs), aiming to enhance the appropriateness and reusability of the constructed FMs in compliance with feature-oriented development. The existing methods, however, failed to assure the developed applications that contain ambiguities between the features generated in FMs by analyzers' intuitions, and hindered the reuse of such applications. Moreover, the accuracy measurements of models based on mathematics-based theoretical verification methods are difficult to apply in practice. Therefore, a refinement technique is demanded to enhance the FM accuracy. This paper aims to identify abnormal feature duplications and collisions based on the feature attributes to address the potential ambiguities between the features in an FM generated for a target domain, and to construct more precise FMs by presenting a technique for eliminating such abnormalities. For this purpose, the profiles of the formalized attributes were first defined based on MDR. Based on the semantics and relationships between the attributes, the duplications and collisions were identified using an analysis matrix, and were generalized to formulate rules by level. Such rules were evaluated to remove the duplications and collisions. In addition, using a supporting analyzer, the features in the initial FM were registered on a repository and were analyzed for feature duplications and collisions based on the saved attribute data. The refinements of the ambiguities between such features are likely to enable the construction of more precise application FMs and the generation of common features with higher reusability. Further, the environments using support tools are expected to provide convenience in the similarity analysis and reuse of features.
Bounded model checking of high-integrity software
Authors: Chaki Sagar 
Published: September 2014

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. One of the most successful variants of model checking is Bounded Model Checking (BMC) [2] which leverages the power of state-of-the-art satisfiability (SAT)
1
and satisfiability-modulo-theory (SMT)
2
to push the boundaries of automated verification. Like model checking, BMC was developed originally for hardware, but has since been extended and applied successfully to verify sequential [4], multi-threaded [1, 10], as well as real-time software [3].

A key benefit of BMC-based software model checkers, such as CBMC [4], is that they are able to handle bit-level semantics of programs precisely. Thus, they are able to detect errors due to integer overflows, and prove correctness of programs that use bit-level operations, without reporting false warnings, or missing bugs. This makes BMC ideal for verifying high-integrity software, where the cost of failure is substantial. Indeed, CBMC has been used to verify a wide variety of low-level safety and security-critical systems, such as co-pilots [8], OS schedulers [7], and hypervisors [11] (see url{http://www.cprover.org/cbmc/applications.shtml} for a more expansive list).
This tutorial will provide an introduction to BMC, its underlying technical principles, and applications to verifying sequential, multi-threaded, and real-time software. The tutorial will be hands-on, with live demonstrations of using BMC tools for verifying sample programs written in C.
Modular control-flow integrity
Authors: Niu Ben , Tan Gang 
Published: September 2014

Control-Flow Integrity (CFI) is a software-hardening technique. It inlines checks into a program so that its execution always follows a predetermined Control-Flow Graph (CFG). As a result, CFI is effective at preventing control-flow hijacking attacks. However, past fine-grained CFI implementations do not support separate compilation, which hinders its adoption.
We present Modular Control-Flow Integrity (MCFI), a new CFI technique that supports separate compilation. MCFI allows modules to be independently instrumented and linked statically or dynamically. The combined module enforces a CFG that is a combination of the individual modules' CFGs. One challenge in supporting dynamic linking in multithreaded code is how to ensure a safe transition from the old CFG to the new CFG when libraries are dynamically linked. The key technique we use is to have the CFG represented in a runtime data structure and have reads and updates of the data structure wrapped in transactions to ensure thread safety. Our evaluation on SPECCPU2006 benchmarks shows that MCFI supports separate compilation, incurs low overhead of around 5%, and enhances security.
Don't sweat the small stuff
Authors: Greenaway David , Lim Japheth , Andronick June , Klein Gerwin 
Published: September 2014

We present an approach for automatically generating
provably correct
abstractions from C source code that are useful for practical implementation verification. The abstractions are easier for a human verification engineer to reason about than the implementation and increase the productivity of interactive code proof. We guarantee soundness by automatically generating proofs that the abstractions are correct.

In particular, we show two key abstractions that are critical for verifying systems-level C code: automatically turning potentially overflowing machine-word arithmetic into ideal integers, and transforming low-level C pointer reasoning into separate abstract heaps. Previous work carrying out such transformations has either done so using unverified translations, or required significant proof engineering effort.
We implement these abstractions in an existing proof-producing specification transformation framework named AutoCorres, developed in Isabelle/HOL, and demonstrate its effectiveness in a number of case studies. We show scalability on multiple OS microkernels, and we show how our changes to AutoCorres improve productivity for total correctness by porting an existing high-level verification of the Schorr-Waite algorithm to a low-level C implementation with minimal effort.
Compiler-assisted detection of transient memory errors
Authors: Tavarageri Sanket , Krishnamoorthy Sriram , Sadayappan P. 
Published: September 2014

The probability of bit flips in hardware memory systems is projected to increase significantly as memory systems continue to scale in size and complexity. Effective hardware-based error detection and correction require that the complete data path, involving all parts of the memory system, be protected with sufficient redundancy. First, this may be costly to employ on commodity computing platforms, and second, even on high-end systems, protection against multi-bit errors may be lacking. Therefore, augmenting hardware error detection schemes with software techniques is of considerable interest.
In this paper, we consider software-level mechanisms to comprehensively detect transient memory faults. We develop novel compile-time algorithms to instrument application programs with checksum computation codes to detect memory errors. Unlike prior approaches that employ checksums on computational and architectural states, our scheme verifies every data access and works by tracking variables as they are produced and consumed. Experimental evaluation demonstrates that the proposed comprehensive error detection solution is viable as a completely software-only scheme. We also demonstrate that with limited hardware support, overheads of error detection can be further reduced.
FlowDroid
Authors: Arzt Steven , Rasthofer Siegfried , Fritz Christian , Bodden Eric , Bartel Alexandre , Klein Jacques , Le Traon Yves , Octeau Damien , McDaniel Patrick 
Published: September 2014

Today's smartphones are a ubiquitous source of private and confidential data. At the same time, smartphone users are plagued by carelessly programmed apps that leak important data by accident, and by malicious apps that exploit their given privileges to copy such data intentionally. While existing static taint-analysis approaches have the potential of detecting such data leaks ahead of time, all approaches for Android use a number of coarse-grain approximations that can yield high numbers of missed leaks and false alarms.
In this work we thus present FlowDroid, a novel and highly precise static taint analysis for Android applications. A precise model of Android's lifecycle allows the analysis to properly handle callbacks invoked by the Android framework, while context, flow, field and object-sensitivity allows the analysis to reduce the number of false alarms. Novel on-demand algorithms help FlowDroid maintain high efficiency and precision at the same time.
We also propose DroidBench, an open test suite for evaluating the effectiveness and accuracy of taint-analysis tools specifically for Android apps. As we show through a set of experiments using SecuriBench Micro, DroidBench, and a set of well-known Android test applications, FlowDroid finds a very high fraction of data leaks while keeping the rate of false positives low. On DroidBench, FlowDroid achieves 93% recall and 86% precision, greatly outperforming the commercial tools IBM AppScan Source and Fortify SCA. FlowDroid successfully finds leaks in a subset of 500 apps from Google Play and about 1,000 malware apps from the VirusShare project.
A theory of changes for higher-order languages
Authors: Cai Yufei , Giarrusso Paolo G. , Rendel Tillmann , Ostermann Klaus 
Published: September 2014

If the result of an expensive computation is invalidated by a small change to the input, the old result should be updated incrementally instead of reexecuting the whole computation. We incrementalize programs through their
derivative
. A derivative maps changes in the program's input directly to changes in the program's output, without reexecuting the original program. We present a program transformation taking programs to their derivatives, which is fully static and automatic, supports first-class functions, and produces derivatives amenable to standard optimization.

We prove the program transformation correct in Agda for a family of simply-typed λ-calculi, parameterized by base types and primitives. A precise interface specifies what is required to incrementalize the chosen primitives.
We investigate performance by a case study: We implement in Scala the program transformation, a plugin and improve performance of a nontrivial program by orders of magnitude.
Fast
Authors: D'Antoni Loris , Veanes Margus , Livshits Benjamin , Molnar David 
Published: September 2014

Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML processing to language type-checking. While these formalisms are of immense practical use, they can only model finite alphabets, and since many real-world applications operate over infinite domains such as integers, this is often a limitation. To overcome this problem we augment tree automata and transducers with symbolic alphabets represented as parametric theories. Admitting infinite alphabets makes these models more general and succinct than their classical counterparts. Despite this, we show how the main operations, such as composition and language equivalence, remain computable given a decision procedure for the alphabet theory.
We introduce a high-level language called Fast that acts as a front-end for the above formalisms. Fast supports symbolic alphabets through tight integration with state-of-the-art satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on practical case studies, covering a wide range of applications.
Surgical precision JIT compilers
Authors: Rompf Tiark , Sujeeth Arvind K. , Brown Kevin J. , Lee HyoukJoong , Chafi Hassan , Olukotun Kunle 
Published: September 2014

Just-in-time (JIT) compilation of running programs provides more optimization opportunities than offline compilation. Modern JIT compilers, such as those in virtual machines like Oracle's HotSpot for Java or Google's V8 for JavaScript, rely on dynamic profiling as their key mechanism to guide optimizations. While these JIT compilers offer good average performance, their behavior is a black box and the achieved performance is highly unpredictable.
In this paper, we propose to turn JIT compilation into a precision tool by adding two essential and generic metaprogramming facilities: First, allow programs to invoke JIT compilation explicitly. This enables controlled specialization of arbitrary code at run-time, in the style of partial evaluation. It also enables the JIT compiler to report warnings and errors to the program when it is unable to compile a code path in the demanded way. Second, allow the JIT compiler to call back into the program to perform compile-time computation. This lets the program itself define the translation strategy for certain constructs on the fly and gives rise to a powerful JIT macro facility that enables "smart" libraries to supply domain-specific compiler optimizations or safety checks.
We present Lancet, a JIT compiler framework for Java bytecode that enables such a tight, two-way integration with the running program. Lancet itself was derived from a high-level Java bytecode interpreter: staging the interpreter using LMS (Lightweight Modular Staging) produced a simple bytecode compiler. Adding abstract interpretation turned the simple compiler into an optimizing compiler. This fact provides compelling evidence for the scalability of the staged-interpreter approach to compiler construction.
In the case of Lancet, JIT macros also provide a natural interface to existing LMS-based toolchains such as the Delite parallelism and DSL framework, which can now serve as accelerator macros for arbitrary JVM bytecode.
Selective context-sensitivity guided by impact pre-analysis
Authors: Oh Hakjoo , Lee Wonchan , Heo Kihong , Yang Hongseok , Yi Kwangkeun 
Published: September 2014

We present a method for selectively applying context-sensitivity during interprocedural program analysis. Our method applies context-sensitivity only when and where doing so is likely to improve the precision that matters for resolving given queries. The idea is to use a pre-analysis to estimate the impact of context-sensitivity on the main analysis's precision, and to use this information to find out when and where the main analysis should turn on or off its context-sensitivity. We formalize this approach and prove that the analysis always benefits from the pre-analysis-guided context-sensitivity. We implemented this selective method for an existing industrial-strength interval analyzer for full C. The method reduced the number of (false) alarms by 24.4%, while increasing the analysis cost by 27.8% on average.
The use of the selective method is not limited to context-sensitivity. We demonstrate this generality by following the same principle and developing a selective relational analysis.
Code completion with statistical language models
Authors: Raychev Veselin , Vechev Martin , Yahav Eran 
Published: September 2014

We address the problem of synthesizing code completions for programs using APIs. Given a program with holes, we synthesize completions for holes with the most likely sequences of method calls.
Our main idea is to reduce the problem of code completion to a natural-language processing problem of predicting probabilities of sentences. We design a simple and scalable static analysis that extracts sequences of method calls from a large codebase, and index these into a statistical language model. We then employ the language model to find the highest ranked sentences, and use them to synthesize a code completion. Our approach is able to synthesize sequences of calls across multiple objects together with their arguments.
Experiments show that our approach is fast and effective. Virtually all computed completions typecheck, and the desired completion appears in the top 3 results in 90% of the cases.
Natural proofs for data structure manipulation in C using separation logic
Authors: Pek Edgar , Qiu Xiaokang , Madhusudan P. 
Published: September 2014

The natural proof technique for heap verification developed by Qiu et al. [32] provides a platform for powerful sound reasoning for specifications written in a dialect of separation logic called Dryad. Natural proofs are proof tactics that enable automated reasoning exploiting recursion, mimicking common patterns found in human proofs. However, these proofs are known to work only for a simple toy language [32].
In this work, we develop a framework called VCDryad that extends the Vcc framework [9] to provide an automated deductive framework against separation logic specifications for C programs based on natural proofs. We develop several new techniques to build this framework, including (a) a novel tool architecture that allows encoding natural proofs at a higher level in order to use the existing Vcc framework (including its intricate memory model, the underlying type-checker, and the SMT-based verification infrastructure), and (b) a synthesis of ghost-code annotations that captures natural proof tactics, in essence forcing Vcc to find natural proofs using primarily decidable theories.

We evaluate our tool extensively, on more than 150 programs, ranging from code manipulating standard data structures, well-known open source library routines (Glib, OpenBSD), Linux kernel routines, customized OS data structures, etc. We show that all these C programs can be fully automatically verified using natural proofs (given pre/post conditions and loop invariants) without
any user-provided proof tactics
. VCDryad is perhaps the first deductive verification framework for heap-manipulating programs in a real language that can prove such a wide variety of programs automatically.
Compositional solution space quantification for probabilistic software analysis
Authors: Borges Mateus , Filieri Antonio , d'Amorim Marcelo , Păsăreanu Corina S. , Visser Willem 
Published: September 2014

Probabilistic software analysis aims at quantifying how likely a target event is to occur during program execution. Current approaches rely on symbolic execution to identify the conditions to reach the target event and try to quantify the fraction of the input domain satisfying these conditions. Precise quantification is usually limited to linear constraints, while only approximate solutions can be provided in general through statistical approaches. However, statistical approaches may fail to converge to an acceptable accuracy within a reasonable time.
We present a compositional statistical approach for the efficient quantification of solution spaces for arbitrarily complex constraints over bounded floating-point domains. The approach leverages interval constraint propagation to improve the accuracy of the estimation by focusing the sampling on the regions of the input domain containing the sought solutions. Preliminary experiments show significant improvement on previous approaches both in results accuracy and analysis time.
Improving JavaScript performance by deconstructing the type system
Authors: Ahn Wonsun , Choi Jiho , Shull Thomas , Garzarán María J. , Torrellas Josep 
Published: September 2014

Increased focus on JavaScript performance has resulted in vast performance improvements for many benchmarks. However, for actual code used in websites, the attained improvements often lag far behind those for popular benchmarks.
This paper shows that the main reason behind this short-fall is how the compiler understands types. JavaScript has no concept of types, but the compiler assigns types to objects anyway for ease of code generation. We examine the way that the Chrome V8 compiler defines types, and identify two design decisions that are the main reasons for the lack of improvement: (1) the inherited prototype object is part of the current object's type definition, and (2) method bindings are also part of the type definition. These requirements make types very unpredictable, which hinders type specialization by the compiler. Hence, we modify V8 to remove these requirements, and use it to compile the JavaScript code assembled by JSBench from real websites. On average, we reduce the execution time of JSBench by 36%, and the dynamic instruction count by 49%.