bluuebunny/crossref_metadata_2025 huggingface dataset:
My Life as a Boson: The Story of "The Higgs"
Authors: Higgs Peter
Published: October 2012

The story begins in 1960, when Nambu, inspired by the BCS theory of superconductivity, formulated chirally invariant relativistic models of interacting massless fermions in which spontaneous symmetry breaking generates fermionic masses (the analogue of the BCS gap). Around the same time Jeffrey Goldstone discussed spontaneous symmetry breaking in models containing elementary scalar fields (as in Ginzburg-Landau theory). I became interested in the problem of how to avoid a feature of both kinds of model, which seemed to preclude their relevance to the real world, namely the existence in the spectrum of massless spin-zero bosons (Goldstone bosons). By 1962 this feature of relativistic field theories had become the subject of the Goldstone theorem.
Towards negotiation as a framework for health promoting technology
Authors: Maitland Julie
Published: October 2012

In this paper we reflect on the findings of three empirical studies of health-related behavioural change and existing work in the technological and sociomedical domains, to critique emerging technological approaches to promoting health-related behavioural change. The critique challenges what appear to be implicit assumptions about technology's role in promoting health-related behavioural change. It prompts a consideration of whose agenda in being pursued, whose values are being encapsulated, and argues for a rethink and reorientation of technological interventions in this domain. As an alternative to the existing approach we suggest a shift in focus from behavioural change to health promotion, and offer negotiation as a potential framework for future innovations in this area.
Predictive Models in Personalized Medicine
Authors: Farooq Faisal , Krishnapuram Balaji , Rosales Romer , Yu Shipeng , Shavlik Jude , Kucherlapati Raju
Published: October 2012

This workshop report is an overview of the Predictive Models in Personalized Medicine workshop held on Dec. 11, 2010 at 2010 Neural Information Processing Systems (NIPS) Conference in Whistler, Canada. The workshop included 3 keynote talks and 6 oral and 5 poster presentations on peer reviewed submissions. The workshop also featured a panel discussion on the growing trends of the field. The workshop was very well received and attended. Based on the response and multiple requests received, it is planned to organize the workshop again at NIPS 2011.
Mobile Devices in the Enterprise: CTO Roundtable Overview
Authors: Creeger Mache
Published: October 2012

The CTO Roundtable on Mobile Devices in the Enterprise focuses on the implications of the widespread use of mobile devices, such as smartphones, in the enterprise computing environment. These new personal devices have presented great challenges and opportunities for the protection of valuable information assets and creation of business value. What follows are the key points from that broader conversation.
A low-cost wear-leveling algorithm for block-mapping solid-state disks
Authors: Chang Li-Pin , Huang Li-Chun
Published: October 2012

Multilevel flash memory cells double or even triple storage density, producing affordable solid-state disks for end users. However, flash lifetime is becoming a critical issue in the popularity of solid-state disks. Wear-leveling methods can prevent flash-storage devices from prematurely retiring any portions of flash memory. The two practical challenges of wear-leveling design are implementation cost and tuning complexity. This study proposes a new wear-leveling design that features both simplicity and adaptiveness. This design requires no new data structures, but utilizes the intelligence available in sector-translating algorithms. Using an on-line tuning method, this design adaptively tunes itself to reach good balance between wear evenness and overhead. A series of trace-driven simulations show that the proposed design outperforms a competitive existing design in terms of wear evenness and overhead reduction. This study also presents a prototype that proves the feasibility of this wear-leveling design in real solid-state disks.
An approach to improving the structure of error-handling code in the linux kernel
Authors: Saha Suman , Lawall Julia , Muller Gilles
Published: October 2012

The C language does not provide any abstractions for exception handling or other forms of error handling, leaving programmers to devise their own conventions for detecting and handling errors. The Linux coding style guidelines suggest placing error handling code at the end of each function, where it can be reached by gotos whenever an error is detected. This coding style has the advantage of putting all of the error-handling code in one place, which eases understanding and maintenance, and reduces code duplication. Nevertheless, this coding style is not always applied. In this paper, we propose an automatic program transformation that transforms error-handling code into this style. We have applied our transformation to the Linux 2.6.34 kernel source code, on which it reorganizes the error handling code of over 1800 functions, in about 25 minutes.
Targeting complex embedded architectures by combining the multicore communications API (mcapi) with compile-time virtualisation
Authors: Gray Ian , Audsley Neil C.
Published: October 2012

Within the domain of embedded systems, hardware architectures are commonly characterised by application-specific heterogeneity. Systems may contain multiple dissimilar processing elements, non-standard memory architectures, and custom hardware elements. The programming of such systems is a considerable challenge, not only because of the need to exploit large degrees of parallelism but also because hardware architectures change from system to system. To solve this problem, this paper proposes the novel combination of a new industry standard for communication across multicore architectures (MCAPI), with a minimal-overhead technique for targeting complex architectures with standard programming languages (Compile-Time Virtualisation).

The Multicore Association have proposed MCAPI as an industry standard for on-chip communications. MCAPI abstracts the on-chip physical communication to provide the application with logical point-to-point unidirectional channels between nodes (software thread, hardware core, etc.). Compile-Time Virtualisation is used to provide an extremely lightweight implementation of MCAPI, that supports a much wider range of architectures than its specification normally considers. Overall, this unique combination enhances programmability by abstracting on-chip communication whilst also exposing critical parts of the target architecture to the programming language.
Divide and recycle
Authors: Benveniste Albert , Bourke Timothy , Caillaud Benoît , Pouzet Marc
Published: October 2012

Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the Sundials library.
Static analysis of synchronous programs in signal for efficient design of multi-clocked embedded systems
Authors: Gamatie Abdoulaye , Gonnord Laure
Published: October 2012

In this paper, we propose a sound abstraction for an efficient static analysis of synchronous programs describing multi-clock embedded systems in Signal. This abstraction combines the Boolean theory and numeric interval approximation to adequately address clock relations defined as combinations of logical and numerical expressions. Through a few examples, we show how the proposed solution is used to determine absence of reaction captured by empty clocks; mutual exclusion captured by two or more clocks whose associated signals never occur at the same time; or hierarchical control of component activations via clock inclusion. We also show this analysis improves the quality of the code generated automatically by the Signal compiler, e.g., a code with smaller footprint, or a code executed more efficiently thanks to optimizations enabled by the new abstraction.
Lowering overhead in sampling-based execution monitoring and tracing
Authors: Thomas Johnson J. , Fischmeister Sebastian , Kumar Deepak
Published: October 2012

Debugging is an important phase in the embedded software development cycle because of its high proportion in the overall cost in the product development. Debugging is difficult for real-time applications as such programs are time-sensitive and must meet deadlines in often a resource constrained environment.

A common approach for real-time systems is to monitor the execution instead of stepping through the program, because stepping will usually violate all deadline constraints. We consider a sampling-based approach for monitoring, because of its predictable overhead for the system compared to traditional monitoring. However, the sampling-based approach can easily have high overhead depending on the length of branches and the granularity of the monitoring effort. To reduce this overhead, we instrument the program with markers that will permit us to sample less frequently and thus reduce the overhead.

This leads to the interesting problems of (a) where to place the markers in the code and (b) how to manipulate the markers. While related work investigates the first part, in this work, we investigate the second component of the problem. We investigate different instrumentation schemes and propose two new schemes based on bitvectors that significantly reduce the overhead for sampling-based execution monitoring.
Software debugging and testing using the abstract diagnosis theory
Authors: Navabpour Samaneh , Bonakdarpour Borzoo , Fischmeister Sebastian
Published: October 2012

In this paper, we present a notion of
observability
and
controllability
in the context of software testing and debugging. Our view of observability is based on the ability of developers, testers, and debuggers to trace back a data dependency chain and observe the value of a variable by starting from a set of variables that are naturally observable (e.g., input/output variables). Likewise, our view of controllability enables one to modify and control the value of a variable through a data dependency chain by starting from a set of variables that can be modified (e.g., input variables). Consequently, the problem that we study in this paper is to identify the minimum number of variables that have to be made observable/controllable in order for a tester or debugger to observe/control the value of another set of variables of interest, given the source code. We show that our problem is an instance of the well-known
abstract diagnosis problem
, where the objective is to find the minimum number of faulty components in a digital circuit, given the system description and value of input/output variables. We show that our problem is NP-complete even if the length of data dependencies is at most
2
. In order to cope with the inevitable exponential complexity, we propose a mapping from the general problem, where the length of data dependency chains is unknown a priori, to
integer linear programming
. Our method is fully implemented in a tool chain for MISRA-C compliant source codes. Our experiments with several real-world applications show that in average, a significant number of debugging points can be reduced using our methods. This result is our motivation to apply our approach in debugging and instrumentation of embedded software, where changes must be minimal as they can perturb the timing constraints and resource consumption. Another interesting application of our results is in data logging of non-terminating embedded systems, where axillary data storage devices are slow and have limited size.
Predictable task migration for locked caches in multi-core systems
Authors: Sarkar Abhik , Mueller Frank , Ramaprasad Harini
Published: October 2012

Locking cache lines in hard real-time systems is a common means of achieving predictability of cache access behavior and tightening as well as reducing worst case execution time, especially in a multitasking environment. However, cache locking poses a challenge for multi-core hard real-time systems since theoretically optimal scheduling techniques on multi-core architectures assume zero cost for task migration. Tasks with locked cache lines need to proactively migrate these lines before the next invocation of the task. Otherwise, cache locking on multi-core architectures becomes useless as predictability is compromised.

This paper proposes hardware-based push-assisted cache migration as a means to retain locks on cache lines across migrations. We extend the push-assisted migration model with several cache migration techniques to efficiently retain locked cache lines on a bus-based chip multi-processor architecture. We also provide deterministic migration delay bounds that help the scheduler decide which migration technique(s) to utilize to relocate a single or multiple tasks. This information also allows the scheduler to determine feasibility of task migrations, which is critical for the safety of any hard real-time system. Such proactive migration of locked cache lines in multi-cores is unprecedented to our knowledge.
Improving Consumer Health IT Application Development
Authors: Zayas-Cabán Teresa , Chaney Kevin
Published: October 2012

This paper is a summary of the Improving Consumer Health Information Technology (IT) Application Development: Lessons from Other Industries, Background Report (available at http://healthit.ahrq.gov/developmentmethodsbackgroundreport). originally published on July 2011. The report was commissioned by the Agency for Healthcare Research and Quality (AHRQ) as a key deliverable for the task order entitled "Understanding Development Methods from Other Industries to Improve the Design of Consumer Health IT" and is an outgrowth of the Building Bridges: Consumer Needs and the Design of Health IT workshop sponsored by AHRQ. The workshop was held at AHRQ's facilities on July 27--28, 2009.
New health systems using network information technologies
Authors: Schatz Bruce R.
Published: October 2012

A new health system is coming based on network information technologies. It consists of health measurement across the full spectrum of health determinants, using mobile devices such as smartphones. This measurement generates personal health records for each individual within a population, which can then be analyzed to identify cohorts, using statistical clustering on supercomputers. These cohorts determine "which persons have which outcomes", so health management can be supported for higher quality at lower cost. This tutorial concisely summarizes the arguments in the recent book Healthcare Infrastructure: Health Systems for Individuals and Populations.
I/O Virtualization
Authors: Rosenblum Mendel , Waldspurger Carl
Published: October 2012

The term
virtual
is heavily overloaded, evoking everything from virtual machines running in the cloud to avatars running across virtual worlds. Even within the narrowfigureer context of computer I/O, virtualization has a long, diverse history, exemplified by logical devices that are deliberately separate from their physical instantiations.
Freefinement
Authors: van Staden Stephan , Calcagno Cristiano , Meyer Bertrand
Published: October 2012

Freefinement is an algorithm that constructs a sound refinement calculus from a verification system under certain conditions. In this paper, a verification system is any formal system for establishing whether an inductively defined term, typically a program, satisfies a specification. Examples of verification systems include Hoare logics and type systems. Freefinement first extends the term language to include specification terms, and builds a verification system for the extended language that is a sound and conservative extension of the original system. The extended system is then transformed into a sound refinement calculus. The resulting refinement calculus can interoperate closely with the verification system - it is even possible to reuse and translate proofs between them. Freefinement gives a semantics to refinement at an abstract level: it associates each term of the extended language with a set of terms from the original language, and refinement simply reduces this set. The paper applies freefinement to a simple type system for the lambda calculus and also to a Hoare logic.
Towards a program logic for JavaScript
Authors: Gardner Philippa Anne , Maffeis Sergio , Smith Gareth David
Published: October 2012

JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts. We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and "with". We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.
The marriage of bisimulations and Kripke logical relations
Authors: Hur Chung-Kil , Dreyer Derek , Neis Georg , Vafeiadis Viktor
Published: October 2012

There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged are *bisimulations* and *Kripke logical relations (KLRs)*. While both approaches are powerful, their complementary advantages have led us and other researchers to wonder whether there is an essential tradeoff between them. Furthermore, both approaches seem to suffer from fundamental limitations if one is interested in scaling them to inter-language reasoning. In this paper, we propose *relation transition systems (RTSs)*, which marry together some of the most appealing aspects of KLRs and bisimulations. In particular, RTSs show how bisimulations' support for reasoning about recursive features via *coinduction* can be synthesized with KLRs' support for reasoning about local state via *state transition systems*. Moreover, we have designed RTSs to avoid the limitations of KLRs and bisimulations that preclude their generalization to inter-language reasoning. Notably, unlike KLRs, RTSs are transitively composable.
Probabilistic relational reasoning for differential privacy
Authors: Barthe Gilles , Köpf Boris , Olmedo Federico , Zanella Béguelin Santiago
Published: October 2012

Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential privacy guarantees for real programs is a difficult and error-prone task that calls for principled approaches and tool support. Approaches based on linear types and static analysis have recently emerged; however, an increasing number of programs achieve privacy using techniques that cannot be analyzed by these approaches. Examples include programs that aim for weaker, approximate differential privacy guarantees, programs that use the Exponential mechanism, and randomized programs that achieve differential privacy without using any standard mechanism. Providing support for reasoning about the privacy of such programs has been an open problem.

We report on CertiPriv, a machine-checked framework for reasoning about differential privacy built on top of the Coq proof assistant. The central component of CertiPriv is a quantitative extension of a probabilistic relational Hoare logic that enables one to derive differential privacy guarantees for programs from first principles. We demonstrate the expressiveness of CertiPriv using a number of examples whose formal analysis is out of the reach of previous techniques. In particular, we provide the first machine-checked proofs of correctness of the Laplacian and Exponential mechanisms and of the privacy of randomized and streaming algorithms from the recent literature.
Symbolic finite state transducers
Authors: Veanes Margus , Hooimeijer Pieter , Livshits Benjamin , Molnar David , Bjorner Nikolaj
Published: October 2012

Finite automata and finite transducers are used in a wide range of applications in software engineering, from regular expressions to specification languages. We extend these classic objects with symbolic alphabets represented as parametric theories. Admitting potentially infinite alphabets makes this representation strictly more general and succinct than classical finite transducers and automata over strings. Despite this, the main operations, including composition, checking that a transducer is single-valued, and equivalence checking for single-valued symbolic finite transducers are effective given a decision procedure for the background theory. We provide novel algorithms for these operations and extend composition to symbolic transducers augmented with registers. Our base algorithms are unusual in that they are nonconstructive, therefore, we also supply a separate model generation algorithm that can quickly find counterexamples in the case two symbolic finite transducers are not equivalent. The algorithms give rise to a complete decidable algebra of symbolic transducers. Unlike previous work, we do not need any syntactic restriction of the formulas on the transitions, only a decision procedure. In practice we leverage recent advances in satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on four case studies, covering a wide range of applications. Our techniques can synthesize string pre-images in excess of 8,000 bytes in roughly a minute, and we find that our new encodings significantly outperform previous techniques in succinctness and speed of analysis.
Deciding choreography realizability
Authors: Basu Samik , Bultan Tevfik , Ouederni Meriem
Published: October 2012

Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several application domains, message-based communication is used as the interaction mechanism, and the communication contract among the components of the system is specified semantically as a state machine. In the service-oriented computing domain such communication contracts are called "choreography" specifications. A choreography specification identifies allowable ordering of message exchanges in a distributed system. A fundamental question about a choreography specification is determining its realizability, i.e., given a choreography specification, is it possible to build a distributed system that communicates exactly as the choreography specifies? Checking realizability of choreography specifications has been an open problem for several years and it was not known if this was a decidable problem. In this paper we give necessary and sufficient conditions for realizability of choreographies. We implemented the proposed realizability check and our experiments show that it can efficiently determine the realizability of 1) web service choreographies, 2) Singularity OS channel contracts, and 3) UML collaboration (communication) diagrams.
A compiler and run-time system for network programming languages
Authors: Monsanto Christopher , Foster Nate , Harrison Rob , Walker David
Published: October 2012

Software-defined networks (SDNs) are a new kind of network architecture in which a controller machine manages a distributed collection of switches by instructing them to install or uninstall packet-forwarding rules and report traffic statistics. The recently formed Open Networking Consortium, whose members include Google, Facebook, Microsoft, Verizon, and others, hopes to use this architecture to transform the way that enterprise and data center networks are implemented.

In this paper, we define a high-level, declarative language, called NetCore, for expressing packet-forwarding policies on SDNs. NetCore is expressive, compositional, and has a formal semantics. To ensure that a majority of packets are processed efficiently on switches---instead of on the controller---we present new compilation algorithms for NetCore and couple them with a new run-time system that issues rule installation commands and traffic-statistics queries to switches. Together, the compiler and run-time system generate efficient rules whenever possible and outperform the simple, manual techniques commonly used to program SDNs today. In addition, the algorithms we develop are generic, assuming only that the packet-matching capabilities available on switches satisfy some basic algebraic laws.

Overall, this paper delivers a new design for a high-level network programming language; an improved set of compiler algorithms; a new run-time system for SDN architectures; the first formal semantics and proofs of correctness in this domain; and an implementation and evaluation that demonstrates the performance benefits over traditional manual techniques.
Nested refinements
Authors: Chugh Ravi , Rondon Patrick M. , Jhala Ranjit
Published: October 2012

Programs written in dynamic languages make heavy use of features --- run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions --- that are beyond the reach of type systems that employ either purely syntactic or purely semantic reasoning. We present a core calculus, System D, that merges these two modes of reasoning into a single powerful mechanism of nested refinement types wherein the typing relation is itself a predicate in the refinement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested refinements with McCarthy's theory of finite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the refinement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratification approach that we use to prove the soundness of System D.
An abstract interpretation framework for termination
Authors: Cousot Patrick , Cousot Radhia
Published: October 2012

Proof, verification and analysis methods for termination all rely on two induction principles: (1) a variant function or induction on data ensuring progress towards the end and (2) some form of induction on the program structure. The abstract interpretation design principle is first illustrated for the design of new forward and backward proof, verification and analysis methods for safety. The safety collecting semantics defining the strongest safety property of programs is first expressed in a constructive fixpoint form. Safety proof and checking/verification methods then immediately follow by fixpoint induction. Static analysis of abstract safety properties such as invariance are constructively designed by fixpoint abstraction (or approximation) to (automatically) infer safety properties. So far, no such clear design principle did exist for termination so that the existing approaches are scattered and largely not comparable with each other.

For (1), we show that this design principle applies equally well to potential and definite termination. The trace-based termination collecting semantics is given a fixpoint definition. Its abstraction yields a fixpoint definition of the best variant function. By further abstraction of this best variant function, we derive the Floyd/Turing termination proof method as well as new static analysis methods to effectively compute approximations of this best variant function.

For (2), we introduce a generalization of the syntactic notion of struc- tural induction (as found in Hoare logic) into a semantic structural induction based on the new semantic concept of inductive trace cover covering execution traces by segments, a new basis for formulating program properties. Its abstractions allow for generalized recursive proof, verification and static analysis methods by induction on both program structure, control, and data. Examples of particular instances include Floyd's handling of loop cutpoints as well as nested loops, Burstall's intermittent assertion total correctness proof method, and Podelski-Rybalchenko transition invariants.
Static and user-extensible proof checking
Authors: Stampoulis Antonis , Shao Zhong
Published: October 2012

Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely time-consuming. We argue that this can be attributed to two profound shortcomings in the architecture of modern proof assistants. The first is that proofs need to include a large amount of minute detail; this is due to the rigidity of the proof checking process, which cannot be extended with domain-specific knowledge. In order to avoid these details, we rely on developing and using tactics, specialized procedures that produce proofs. Unfortunately, tactics are both hard to write and hard to use, revealing the second shortcoming of modern proof assistants. This is because there is no static knowledge about their expected use and behavior. As has recently been demonstrated, languages that allow type-safe manipulation of proofs, like Beluga, Delphin and VeriML, can be used to partly mitigate this second issue, by assigning rich types to tactics. Still, the architectural issues remain. In this paper, we build on this existing work, and demonstrate two novel ideas: an extensible conversion rule and support for static proof scripts. Together, these ideas enable us to support both user-extensible proof checking, and sophisticated static checking of tactics, leading to a new point in the design space of future proof assistants. Both ideas are based on the interplay between a light-weight staging construct and the rich type information available.
Verification of parameterized concurrent programs by modular reasoning about data and control
Authors: Farzan Azadeh , Kincaid Zachary
Published: October 2012

In this paper, we consider the problem of verifying thread-state properties of multithreaded programs in which the number of active threads cannot be statically bounded. Our approach is based on decomposing the task into two modules, where one reasons about data and the other reasons about control. The data module computes thread-state invariants (e.g., linear constraints over global variables and local variables of one thread) using the thread interference information computed by the control module. The control module computes a representation of thread interference, as an incrementally constructed
data flow graph
, using the data invariants provided by the data module. These invariants are used to rule out patterns of thread interference that can not occur in a real program execution. The two modules are incorporated into a feedback loop, so that the abstractions of data and interference are iteratively coarsened as the algorithm progresses (that is, they become weaker) until a fixed point is reached. Our approach is sound and terminating, and applicable to programs with infinite state (e.g., unbounded integers) and unboundedly many threads. The verification method presented in this paper has been implemented into a tool, called Duet. We demonstrate the effectiveness of our technique by verifying properties of a selection of Linux device drivers using Duet, and also compare Duet with previous work on verification of parameterized Boolean program using the Boolean abstractions of these drivers.
Programming with binders and indexed data-types
Authors: Cave Andrew , Pientka Brigitte
Published: October 2012

We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from contextual LF. This allows the user to specify formal systems within the logical framework LF and index ML types with contextual LF objects. Our language design keeps the index language generic only requiring decidability of equality of the index language providing a modular design. To illustrate the elegance and effectiveness of our language, we give programs for closure conversion and normalization by evaluation.

Our three key technical contribution are: 1) We give a bi-directional type system for our core language which is centered around refinement substitutions instead of constraint solving. As a consequence, type checking is decidable and easy to trust, although constraint solving may be undecidable. 2) We give a big-step environment based operational semantics with environments which lends itself to efficient implementation. 3) We prove our language to be type safe and have mechanized our theoretical development in the proof assistant Coq using the fresh approach to binding.
Randomized accuracy-aware program transformations for efficient approximate computations
Authors: Zhu Zeyuan Allen , Misailovic Sasa , Kelner Jonathan A. , Rinard Martin
Published: October 2012

Despite the fact that approximate computations have come to dominate many areas of computer science, the field of program transformations has focused almost exclusively on traditional semantics-preserving transformations that do not attempt to exploit the opportunity, available in many computations, to acceptably trade off accuracy for benefits such as increased performance and reduced resource consumption.

We present a model of computation for approximate computations and an algorithm for optimizing these computations. The algorithm works with two classes of transformations: substitution transformations (which select one of a number of available implementations for a given function, with each implementation offering a different combination of accuracy and resource consumption) and sampling transformations (which randomly discard some of the inputs to a given reduction). The algorithm produces a (1+ε) randomized approximation to the optimal randomized computation (which minimizes resource consumption subject to a probabilistic accuracy specification in the form of a maximum expected error or maximum error variance).
Clarifying and compiling C/C++ concurrency
Authors: Batty Mark , Memarian Kayvan , Owens Scott , Sarkar Susmit , Sewell Peter
Published: October 2012

The upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory behaviours of mainstream multiprocessors, combining simple semantics for most code with high-performance *low-level atomics* for concurrency libraries. In this paper, we first establish two simpler but provably equivalent models for C++11, one for the full language and another for the subset without consume operations. Subsetting further to the fragment without low-level atomics, we identify a subtlety arising from atomic initialisation and prove that, under an additional condition, the model is equivalent to sequential consistency for race-free programs.

We then prove our main result, the correctness of two proposed compilation schemes for the C++11 load and store concurrency primitives to Power assembly, having noted that an earlier proposal was flawed. (The main ideas apply also to ARM, which has a similar relaxed memory architecture.)

This should inform the ongoing development of production compilers for C++11 and C1x, clarifies what properties of the machine architecture are required, and builds confidence in the C++11 and Power semantics.
A mechanized semantics for C++ object construction and destruction, with applications to resource management
Authors: Ramananandro Tahina , Dos Reis Gabriel , Leroy Xavier
Published: October 2012

We present a formal operational semantics and its Coq mechanization for the C++ object model, featuring object construction and destruction, shared and repeated multiple inheritance, and virtual function call dispatch. These are key C++ language features for high-level system programming, in particular for predictable and reliable resource management. This paper is the first to present a formal mechanized account of the metatheory of construction and destruction in C++, and applications to popular programming techniques such as "resource acquisition is initialization". We also report on irregularities and apparent contradictions in the ISO C++03 and C++11 standards.
Self-certification
Authors: Strub Pierre-Yves , Swamy Nikhil , Fournet Cedric , Chen Juan
Published: October 2012

Well-established dependently-typed languages like Agda and Coq provide reliable ways to build and check formal proofs. Several other dependently-typed languages such as Aura, ATS, Cayenne, Epigram, F*, F7, Fine, Guru, PCML5, and Ur also explore reliable ways to develop and verify programs. All these languages shine in their own regard, but their implementations do not themselves enjoy the degree of safety provided by machine-checked verification. We propose a general technique called self-certification that allows a typechecker for a suitably expressive language to be certified for correctness. We have implemented this technique for F*, a dependently typed language on the .NET platform. Self-certification involves implementing a typechecker for F* in F*, while using all the conveniences F* provides for the compiler-writer (e.g., partiality, effects, implicit conversions, proof automation, libraries). This typechecker is given a specification (in~F*) strong enough to ensure that it computes valid typing derivations. We obtain a typing derivation for the core typechecker by running it on itself, and we export it to Coq as a type-derivation certificate. By typechecking this derivation (in Coq) and applying the F* metatheory (also mechanized in Coq), we conclude that our type checker is correct. Once certified in this manner, the F* typechecker is emancipated from Coq.

Self-certification leads to an efficient certification scheme---we no longer depend on verifying certificates in Coq---as well as a more broadly applicable one. For instance, the self-certified F* checker is suitable for use in adversarial settings where Coq is not intended for use, such as run-time certification of mobile code.
A heuristic for bottleneck crossing minimization and its performance on general crossing minimization
Authors: Stallmann Matthias F.
Published: October 2012

Extensive research over the last 20 or more years has been devoted to the problem of minimizing the total number of crossings in layered directed acyclic graphs (dags). Algorithms for this problem are used for graph drawing, to implement one of the stages in the multistage approach proposed by Sugiyama et al. [1981]. In some applications, such as minimizing the deleterious effects of crosstalk in VLSI circuits, it may be more appropriate to minimize the maximum number of crossings over all the edges. We refer to this as the
bottleneck crossing problem
. This article proposes a new heuristic,
maximum crossings edge (MCE)
, designed specifically for the bottleneck problem. It is no surprise that MCE universally outperforms other heuristics with respect to bottleneck crossings. What is surprising, and the focus of this article, is that, in many settings, the MCE heuristic excels at minimizing the total number of crossings. Experiments on sparse graphs support the hypothesis that MCE gives better results (vis a vis barycenter) when the maximum degree of the dag is large. In contrast to barycenter, the number of crossings yielded by MCE is further reduced as runtime is increased. Even better results are obtained when the two heuristics are combined and/or barycenter is followed by the sifting heuristic reported in Matuszewski et al. [1999].
Constructing and sampling graphs with a prescribed joint degree distribution
Authors: Stanton Isabelle , Pinar Ali
Published: October 2012

One of the most influential recent results in network analysis is that many natural networks exhibit a power-law or log-normal degree distribution. This has inspired numerous generative models that match this property. However, more recent work has shown that while these generative models do have the right degree distribution, they are not good models for real-life networks due to their differences on other important metrics like conductance. We believe this is, in part, because many of these real-world networks have very differentjoint degree distributions, that is, the probability that a randomly selected edge will be between nodes of degreekandl. Assortativity is a sufficient statistic of the joint degree distribution, and it has been previously noted that social networks tend to be assortative, while biological and technological networks tend to be disassortative.

We suggest understanding the relationship between network structure and the joint degree distribution of graphs is an interesting avenue of further research. An important tool for such studies are algorithms that can generate random instances of graphs with the same joint degree distribution. This is the main topic of this article, and we study the problem from both a theoretical and practical perspective. We provide an algorithm for constructing simple graphs from a given joint degree distribution, and a Monte Carlo Markov chain method for sampling them. We also show that the state space of simple graphs with a fixed degree distribution is connected viaendpoint switches. We empirically evaluate the mixing time of this Markov chain by using experiments based on the autocorrelation of each edge. These experiments show that our Markov chain mixes quickly on these real graphs, allowing for utilization of our techniques in practice.
Discrete range searching primitive for the GPU and its applications
Authors: Soman Jyothish , Kothapalli Kishore , Narayanan P. J.
Published: October 2012

Graphics processing units (GPUs) provide large computational power at a very low price, which position GPUs well as an ubiquitous accelerator. However, GPUs are space constrained, and hence applications developed for GPUs are space sensitive.

Space-constrained computational devices such as GPUs can greatly benefit from representations that reduce space consumption drastically. One such representation is the succinct representation of trees. Succinct representation of trees generally allows for operations such as parent queries, least common ancestor queries, and so on. Mapping such a robust representation to the GPU for targeted applications can lead to substantial improvement in problem sizes that are processed at a given point of time. Space-saving methods such as succinct data structures remain largely unexplored on the GPU. In this work, a succinct representation of ordered trees on the GPU is explored, with application to discrete range searching (DRS).

Based on the succinct representations found applicable, a space--saving solution for DRS is presented here. In our method, DRS is mapped to a least common ancestor query on a Cartesian tree. For space-efficient DRS queries, we store the succinct representation of the Cartesian tree of an array. Our method uses a maximum of 7.5 bits of additional space per element. Furthermore, the speed-up achieved by our method is in the range of 20--25 for preprocessing and 25--35 for batch querying over a sequential implementation. Compared to an 8-threaded implementation, our preprocessing and querying methods obtain a speed-up of 6--8.

We also study the applications of the DRS on the GPU. Efficient primitives expand the range of applications performed on the GPU. DRS is one such primitive with direct applications to string processing, document and text retrieval systems, and least common ancestor queries. We suggest that graph algorithms that use the least common ancestor, can be enabled on the GPU based on DRS primitive. We also show some applications of DRS in tree queries and string querying.
Effect of measuring number of steps with a digital pedometer on female student physical activity
Authors: Sugano Masashi , Hirano Rika
Published: October 2012

In recent years, various attempts have been made to improve lifestyle by means of a life log, which records behavior and patterns of life by using digital equipment. Small digital pedometers are useful for obtaining life log data since it is possible to record not only number of steps or energy consumption, but also activity time [1]. Here we assess the effect of number of steps, measured with a digital pedometer, on increasing the frequency of walking. In this study, we modified a standard pedometer so that the display was not visible and then carried out a crossover examination by dividing candidates into two groups. In addition, we issued a questionnaire to candidates to investigate their awareness of the pedometer display.
Migration of a pre-hospital cardiology emergency system from data model to multilevel modeling
Authors: Alvernaz Christiano , Cook Timothy W. , Cavalini Luciana Tricai
Published: October 2012

This paper presents the migration of a prehospital cardiology emergency system from a data model to multilevel modeling. The clinical concepts of data model-based system were identified and modeled according to the Multilevel Healthcare Information Modeling (MLHIM) specifications. This migration is been developed in order to provide the system with the required features of interoperability and semantic coherence.
Modeling of nursing knowledge for multilevel information systems
Authors: Matos Nogueira Joyce R. , Cook Timothy W. , Cavalini Luciana Tricai
Published: October 2012

This paper presents the modeling strategy of nursing knowledge, based on multilevel modeling of health systems. Through a systematic review, nursing record instruments were obtained. and one was chose for knowledge modeling according to the Multilevel Healthcare Information Modeling (MLHIM) specifications.
Implementing a specification for exceptional data in multilevel modeling of healthcare applications
Authors: Cook Timothy W. , Cavalini Luciana Tricai
Published: October 2012

Missing information are key issues for interoperability and semantic coherence in healthcare information systems. This paper presents the implementation of the Exceptional Package in the Multilevel Healthcare Information Modeling (MLHIM) specifications, and it describes two use cases where missing information is critical for decision-making and healthcare technology assessment.