bluuebunny/crossref_metadata_2025 huggingface dataset:
Bufferbloat: Dark Buffers in the Internet
Authors: Gettys Jim , Nichols Kathleen
Published: October 2012

Today’s networks are suffering from unnecessary latency and poor system performance. The culprit is bufferbloat, the existence of excessively large and frequently full buffers inside the network. Large buffers have been inserted all over the Internet without sufficient thought or testing. They damage or defeat the fundamental congestion-avoidance algorithms of the Internet’s most common transport protocol. Long delays from bufferbloat are frequently attributed incorrectly to network congestion, and this misinterpretation of the problem leads to the wrong solutions being proposed.
Information effects
Authors: James Roshan P. , Sabry Amr
Published: October 2012

Computation is a physical process which, like all other physical processes, is fundamentally reversible. From the notion of type isomorphisms, we derive a typed, universal, and reversible computational model in which information is treated as a linear resource that can neither be duplicated nor erased. We use this model as a semantic foundation for computation and show that the "gap" between conventional irreversible computation and logically reversible computation can be captured by a type-and-effect system. Our type-and-effect system is structured as an arrow metalanguage that exposes creation and erasure of information as explicit effect operations. Irreversible computations arise from interactions with an implicit information environment, thus making them a derived notion, much like open systems in Physics. We sketch several applications which can benefit from an explicit treatment of information effects, such as quantitative information-flow security and differential privacy.
A language for automatically enforcing privacy policies
Authors: Yang Jean , Yessenov Kuat , Solar-Lezama Armando
Published: October 2012

It is becoming increasingly important for applications to protect sensitive data. With current techniques, the programmer bears the burden of ensuring that the application's behavior adheres to policies about where sensitive values may flow. Unfortunately, privacy policies are difficult to manage because their global nature requires coordinated reasoning and enforcement. To address this problem, we describe a programming model that makes the system responsible for ensuring adherence to privacy policies. The programming model has two components: 1) core programs describing functionality independent of privacy concerns and 2) declarative, decentralized policies controlling how sensitive values are disclosed. Each sensitive value encapsulates multiple views; policies describe which views are allowed based on the output context. The system is responsible for automatically ensuring that outputs are consistent with the policies. We have implemented this programming model in a new functional constraint language named Jeeves. In Jeeves, sensitive values are introduced as symbolic variables and policies correspond to constraints that are resolved at output channels. We have implemented Jeeves as a Scala library using an SMT solver as a model finder. In this paper we describe the dynamic and static semantics of Jeeves and the properties about policy enforcement that the semantics guarantees. We also describe our experience implementing a conference management system and a social network.
Access permission contracts for scripting languages
Authors: Heidegger Phillip , Bieniusa Annette , Thiemann Peter
Published: October 2012

The ideal software contract fully specifies the behavior of an operation. Often, in particular in the context of scripting languages, a full specification may be cumbersome to state and may not even be desired. In such cases, a partial specification, which describes selected aspects of the behavior, may be used to raise the confidence in an implementation of the operation to a reasonable level.

We propose a novel kind of contract for object-based languages that specifies the side effects of an operation with
access permissions
. An access permission contract uses sets of access paths to express read and write permissions for the properties of the objects accessible from the operation.

We specify a monitoring semantics for access permission contracts and implement this semantics in a contract system for JavaScript. We prove soundness and stability of violation under increasing aliasing for our semantics.

Applications of access permission contracts include enforcing modularity, test-driven development, program understanding, and regression testing. With respect to testing and understanding, we find that adding access permissions to contracts increases the effectiveness of error detection through contract monitoring by 6-13%.
Recursive proofs for inductive tree data-structures
Authors: Madhusudan Parthasarathy , Qiu Xiaokang , Stefanescu Andrei
Published: October 2012

We develop logical mechanisms and procedures to facilitate the verification of full functional properties of inductive tree data-structures using recursion that are sound, incomplete, but terminating. Our contribution rests in a new extension of first-order logic with recursive definitions called Dryad, a syntactical restriction on pre- and post-conditions of recursive imperative programs using Dryad, and a systematic methodology for accurately unfolding the footprint on the heap uncovered by the program that leads to finding simple recursive proofs using formula abstraction and calls to SMT solvers. We evaluate our methodology empirically and show that several complex tree data-structure algorithms can be checked against full functional specifications automatically, given pre- and post-conditions. This results in the first automatic terminating methodology for proving a wide variety of annotated algorithms on tree data-structures correct, including max-heaps, treaps, red-black trees, AVL trees, binomial heaps, and B-trees.
Multiple facets for dynamic information flow
Authors: Austin Thomas H. , Flanagan Cormac
Published: October 2012

JavaScript has become a central technology of the web, but it is also the source of many security problems, including cross-site scripting attacks and malicious advertising code. Central to these problems is the fact that code from untrusted sources runs with full privileges. We implement information flow controls in Firefox to help prevent violations of data confidentiality and integrity. Most previous information flow techniques have primarily relied on either static type systems, which are a poor fit for JavaScript, or on dynamic analyses that sometimes get stuck due to problematic implicit flows, even in situations where the target web application correctly satisfies the desired security policy. We introduce faceted values, a new mechanism for providing information flow security in a dynamic manner that overcomes these limitations. Taking inspiration from secure multi-execution, we use faceted values to simultaneously and efficiently simulate multiple executions for different security levels, thus providing non-interference with minimal overhead, and without the reliance on the stuck executions of prior dynamic approaches.
Programming languages for programmable networks
Authors: Rexford Jennifer
Published: October 2012

Today's computer networks perform a bewildering array of tasks, from routing and access control, to traffic monitoring and load balancing. To support wireless users accessing services hosted in the cloud, enterprise and data-center networks are under increasing pressure to support client mobility, virtual-machine migration, resource isolation between cloud services, and energy-efficient operation. Yet, network administrators must configure the network through closed and proprietary interfaces to heterogeneous devices, such as routers, switches, firewalls, load balancers, network address translators, and intrusion detection systems. Not surprisingly, configuring these complex networks is expensive and error-prone, and innovation in network management proceeds at a snail's pace.

During the past several years, the networking industry and research community have pushed for greater openness in networking software, and a clearer separation between networking devices and the software that controls them. This broad trend is known as Software Defined Networking (SDN). A hallmark of SDN is having an open interface for controller software running on a commodity computer to install packet-processing rules in the underlying switches. In particular, the OpenFlow protocol (see www.openflow.org) has significant momentum. Many commercial switches support OpenFlow, and a number of campus, data-center, and backbone networks have deployed the new technology.

With the emergence of open interfaces to network devices, the time is ripe to rethink the design of network software, to put networking on a stronger foundation and foster innovation in networked services. The programming languages community can play a vital role in this transformation, by creating languages, compilers, run-time systems, and testing and verification techniques that raise the level of abstraction for programming the network. In this talk, we give an overview of Software Defined Networking, and survey the early programming-languages research in this area. We also outline exciting opportunities for interdisciplinary research at the intersection of programming languages and computer networks.
Run your research
Authors: Klein Casey , Clements John , Dimoulas Christos , Eastlund Carl , Felleisen Matthias , Flatt Matthew , McCarthy Jay A. , Rafkind Jon , Tobin-Hochstadt Sam , Findler Robert Bruce
Published: October 2012

Formal models serve in many roles in the programming language community. In its primary role, a model communicates the idea of a language design; the architecture of a language tool; or the essence of a program analysis. No matter which role it plays, however, a faulty model doesn't serve its purpose.

One way to eliminate flaws from a model is to write it down in a mechanized formal language. It is then possible to state theorems about the model, to prove them, and to check the proofs. Over the past nine years, PLT has developed and explored a lightweight version of this approach, dubbed Redex. In a nutshell, Redex is a domain-specific language for semantic models that is embedded in the Racket programming language. The effort of creating a model in Redex is often no more burdensome than typesetting it with LaTeX; the difference is that Redex comes with tools for the semantics engineering life cycle.
Canonicity for 2-dimensional type theory
Authors: Licata Daniel R. , Harper Robert
Published: October 2012

Higher-dimensional dependent type theory enriches conventional one-dimensional dependent type theory with additional structure expressing equivalence of elements of a type. This structure may be employed in a variety of ways to capture rather coarse identifications of elements, such as a universe of sets considered modulo isomorphism. Equivalence must be respected by all families of types and terms, as witnessed computationally by a type-generic program. Higher-dimensional type theory has applications to code reuse for dependently typed programming, and to the formalization of mathematics. In this paper, we develop a novel judgemental formulation of a two-dimensional type theory, which enjoys a canonicity property: a closed term of boolean type is definitionally equal to true or false. Canonicity is a necessary condition for a computational interpretation of type theory as a programming language, and does not hold for existing axiomatic presentations of higher-dimensional type theory. The method of proof is a generalization of the NuPRL semantics, interpreting types as syntactic groupoids rather than equivalence relations.
On the power of coercion abstraction
Authors: Cretin Julien , Rémy Didier
Published: October 2012

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain forms of delayed type instantiation. We generalize F-eta by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the lambda-calculus but keeping track of which parts of terms are coercions. We obtain a language where coercions do not contribute to the reduction but may block it and are thus not erasable. We recover erasable coercions by choosing a weak reduction strategy and restricting coercion abstraction to value-forms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes F-eta, F-sub, and MLF in a unified framework.
Abstractions from tests
Authors: Naik Mayur , Yang Hongseok , Castelnuovo Ghila , Sagiv Mooly
Published: October 2012

We present a framework for leveraging dynamic analysis to find good abstractions for static analysis. A static analysis in our framework is parametrised. Our main insight is to directly and efficiently compute from a concrete trace, a necessary condition on the parameter configurations to prove a given query, and thereby prune the space of parameter configurations that the static analysis must consider. We provide constructive algorithms for two instance analyses in our framework: a flow- and context-sensitive thread-escape analysis and a flow- and context-insensitive points-to analysis. We show the efficacy of these analyses, and our approach, on six Java programs comprising two million bytecodes: the thread-escape analysis resolves 80% of queries on average, disproving 28% and proving 52%; the points-to analysis resolves 99% of queries on average, disproving 29% and proving 70%.
Sound predictive race detection in polynomial time
Authors: Smaragdakis Yannis , Evans Jacob , Sadowski Caitlin , Yi Jaeheon , Flanagan Cormac
Published: October 2012

Data races are among the most reliable indicators of programming errors in concurrent software. For at least two decades, Lamport's happens-before (HB) relation has served as the standard test for detecting races--other techniques, such as lockset-based approaches, fail to be sound, as they may falsely warn of races. This work introduces a new relation, causally-precedes (CP), which generalizes happens-before to observe more races without sacrificing soundness. Intuitively, CP tries to capture the concept of happens-before ordered events that must occur in the observed order for the program to observe the same values. What distinguishes CP from past predictive race detection approaches (which also generalize an observed execution to detect races in other plausible executions) is that CP-based race detection is both sound and of polynomial complexity. We demonstrate that the unique aspects of CP result in practical benefit. Applying CP to real-world programs, we successfully analyze server-level applications (e.g., Apache FtpServer) and show that traces longer than in past predictive race analyses can be analyzed in mere seconds to a few minutes. For these programs, CP race detection uncovers races that are hard to detect by repeated execution and HB race detection: a single run of CP race detection produces several races not discovered by 10 separate rounds of happens-before race detection.
Meta-level features in an industrial-strength theorem prover
Authors: Moore J. Strother
Published: October 2012

The ACL2 theorem prover---the current incarnation of "the" Boyer-Moore theorem prover---is a theorem prover for an extension of a first-order, applicative subset of Common Lisp. The ACL2 system provides a useful specification and modeling language as well as a useful mechanical theorem proving environment. ACL2 is in use at several major microprocessor manufacturers to verify functional correctness of important components of commercial designs. This talk explores the design of ACL2 and the tradeoffs that have turned out to be pivotal to its success.
A unified approach to fully lazy sharing
Authors: Balabonski Thibaut
Published: October 2012

We give an axiomatic presentation of sharing-via-labelling for weak lambda-calculi, that makes it possible to formally compare many different approaches to fully lazy sharing, and obtain two important results. We prove that the known implementations of full laziness are all equivalent in terms of the number of beta-reductions performed, although they behave differently regarding the duplication of terms. We establish a link between the optimality theories of weak lambda-calculi and first-order rewriting systems by expressing fully lazy lambda-lifting in our framework, thus emphasizing the first-order essence of weak reduction.
Edit lenses
Authors: Hofmann Martin , Pierce Benjamin , Wagner Daniel
Published: October 2012

A lens is a bidirectional transformation between a pair of connected data structures, capable of translating an edit on one structure into an appropriate edit on the other. Many varieties of lenses have been studied, but none, to date, has offered a satisfactory treatment of how edits are represented. Many foundational accounts only consider edits of the form "overwrite the whole structure," leading to poor behavior in many situations by failing to track the associations between corresponding parts of the structures when elements are inserted and deleted in ordered lists, for example. Other theories of lenses do maintain these associations, either by annotating the structures themselves with change information or using auxiliary data structures, but every extant theory assumes that the entire original source structure is part of the information passed to the lens.

We offer a general theory of edit lenses, which work with descriptions of changes to structures, rather than with the structures themselves. We identify a simple notion of "editable structure"--a set of states plus a monoid of edits with a partial monoid action on the states--and construct a semantic space of lenses between such structures, with natural laws governing their behavior. We show how a range of constructions from earlier papers on "state-based" lenses can be carried out in this space, including composition, products, sums, list operations, etc. Further, we show how to construct edit lenses for arbitrary containers in the sense of Abbott, Altenkirch, and Ghani. Finally, we show that edit lenses refine a well-known formulation of state-based lenses, in the sense that every state-based lens gives rise to an edit lens over structures with a simple overwrite-only edit language, and conversely every edit lens on such structures gives rise to a state-based lens.
Exact solutions and bounds for general art gallery problems
Authors: Kröller Alexander , Baumgartner Tobias , Fekete Sándor P. , Schmidt Christiane
Published: October 2012

The classical Art Gallery Problem asks for the minimum number of guards that achieve visibility coverage of a given polygon. This problem is known to be NP-hard, even for very restricted and discrete special cases. For the case of vertex guards and simple orthogonal polygons, Cuoto et al. have recently developed an exact method that is based on a set-cover approach. For the general problem (in which both the set of possible guard positions and the point set to be guarded are uncountable), neither constant-factor approximation algorithms nor exact solution methods are known.

We present a primal-dual algorithm based on linear programming that provides lower bounds on the necessary number of guards in every step and—in case of convergence and integrality—ends with an optimal solution. We describe our implementation and give experimental results for an assortment of polygons, including nonorthogonal polygons with holes.
Assignment-minimum clique coverings
Authors: Ennis John M. , Fayle Charles M. , Ennis Daniel M.
Published: October 2012

The search for minimum clique coverings of graphs appears in many practical guises and with several possible minimization goals. One reasonable goal is to minimize the number of overall cliques in a covering, while a second less well-studied but equally reasonable goal is to minimize the number of individual assignments of vertices to cliques. Both goals constitute NP-hard problems and as such require competitive algorithms for practical progress to be made toward their resolutions. In this article, we introduce a technique for accomplishing the latter goal, using a combination of data reduction and a backtracking algorithm. In addition, we demonstrate that it is not always possible to minimize both the number of cliques and the number of individual vertex-clique assignments simultaneously. This demonstration resolves an open question and underscores the need for techniques that specifically minimize the number of assignments of vertices to cliques. We then illustrate our approach in two practical examples. We follow these examples with a simulation-based comparison of our exact approach with a heuristic based on the state-of-the-art algorithm for minimizing the number of cliques in a clique covering. For this comparison, we consider graphs likely to arise in applied statistics, a category of applications for which minimizing individual vertex-clique assignments is of particular interest.
Engineering highway hierarchies
Authors: Sanders Peter , Schultes Dominik
Published: October 2012

Highway hierarchies exploit hierarchical properties inherent in real-world road networks to allow fast and exact point-to-point shortest-path queries. A fast preprocessing routine iteratively performs two steps: First, it removes edges that only appear on shortest paths
close
to source or target; second, it identifies low-degree nodes and bypasses them by introducing shortcut edges. The resulting hierarchy of highway networks is then used in a Dijkstra-like bidirectional query algorithm to considerably reduce the search space size without losing exactness. The crucial fact is that ‘far away’ from source and target it is sufficient to consider only high-level edges.

Experiments with road networks for a continent show that using a preprocessing time of around 15 min, one can achieve a query time of around 1ms on a 2.0GHz AMD Opteron.

Highway hierarchies can be combined with goal-directed search, they can be extended to answer many-to-many queries, and they can be used as a basis for other speed-up techniques (e.g., for transit-node routing and highway-node routing).
An SDP approach to multi-level crossing minimization
Authors: Chimani Markus , Hungerländer Philipp , Jünger Michael , Mutzel Petra
Published: October 2012

We present an approach based on semidefinite programs (SDP) to tackle the multi-level crossing minimization problem. We are given a layered graph (i.e., the graph's vertices are assigned to multiple parallel levels) and are asked for an ordering of the nodes on each level such that, when drawing the graph with straight lines, the resulting number of crossings is minimized. Solving this step is crucial in what is probably the most widely used graph drawing scheme, the Sugiyama framework.

The problem has received a lot of attention in both the fields of heuristics and exact methods. For a long time, integer linear programming (ILP) approaches were the only exact algorithms applicable, at least for small graphs. Recently, SDP formulations for the special case of two levels were proposed and dominated the ILP for dense instances.

In this article, we present a new SDP formulation for the general multi-level version that, for two levels, is even stronger than the aforementioned specialized SDP. As a by-product, we also obtain an SDP-based heuristic, which in practice always gives (near-)optimal solutions.

We conduct a large set of experiments, both on randomized and on real-world instances, and compare our approach to a state-of-the-art ILP-based branch-and-cut implementation. The SDP clearly dominates for denser graphs, while the ILP approach is usually faster for sparse instances. However, even for such sparse graphs, the SDP solves more instances to optimality than the ILP. In fact, there is no single instance that the ILP solved that the SDP did not. Overall, our experiments reveal that, for sparse graphs, one should usually try to find an optimal solution with the ILP first. If this approach does not solve the instance to optimality within reasonable time, the SDP still has a good chance to do so.

Being able to solve larger real-world instances than reported before, we are also able to evaluate heuristics for this problem. In this article, we do so for the traditional barycenter-heuristic (showing that it leaves a large gap to the true optimum) and the state-of-the-art upward-planarization method (showing that it is usually close to the optimum).
Exact pattern matching with feed-forward bloom filters
Authors: Moraru Iulian , Andersen David G.
Published: October 2012

This article presents a new, memory efficient and cache-optimized algorithm for simultaneously searching for a large number of patterns in a very large corpus. This algorithm builds upon the Rabin-Karp string search algorithm and incorporates a new type of Bloom filter that we call a
feed-forward Bloom filter
. While it retains the asymptotic time complexity of previous multiple pattern matching algorithms, we show that this technique, along with a CPU architecture-aware design of the Bloom filter, can provide speed-ups between 2× and 30×, and memory consumption reductions as large as 50× when compared with grep. Our algorithm is also well suited for implementations on GPUs: A modern GPU can search for 3 million patterns at a rate of 580MB/s, and for 100 million patterns (a prohibitive number for traditional algorithms) at a rate of 170MB/s.
ACM journal on experimental algorithmics special issue on multicore algorithms
Authors: Bader David A. , Tsigas Philippas
Published: October 2012

The recent switch to multicore processors brought a dramatic change that affects a large spectrum of systems from embedded and general-purpose to high-end computing systems. Parallelism is forcing major changes in software development. The aim of this issue is to discuss the challenges that parallelism brings to the design and implementation of algorithms and data structures. This special issue arose out of discussions held at the Dagstuhl Seminar 10261, on Algorithm Engineering held June 27--July 2, 2010, in Germany, and organized by Giuseppe F. Italiano (Università di Roma “Tor Vergata,” Italy), David S. Johnson (AT&T Research, Florham Park, NJ), Petra Mutzel (Technical University of Dortmund, Germany), and Peter Sanders (Karlsruhe Institute of Technology, Germany). We conceived a special issue of the ACM Journal on Experimental Algorithmics with a call for original submissions that address implementation and performance issues of multicore algorithms and data structures for any multicore processor, for example, Intel Nehalem, Single-Chip Cloud, NVIDIA and AMD GPUs. An experimental study typically includes an implementation, a series of experiments designed to understand the behavior of the algorithm(s) under study, and a critical discussion of the experiments and their results. We welcomed experimental submissions and encouraged authors to include test data from previously published studies to enable critical comparisons. A total of nine submissions were received, and four were accepted for this special issue. All manuscripts had at least three extensive reviews, and most received five to six reviews. We thank all of the authors for their submissions, and especially the 16 reviewers of these manuscripts.
An experimental evaluation of the scalability of real-time scheduling algorithms on large-scale multicore platforms
Authors: Dellinger Matthew , Lindsay Aaron , Ravindran Binoy
Published: October 2012

We present an experimental analysis of the scalability of 13 multicore real-time scheduling algorithms on a 48-core AMD platform. The algorithms include G-EDF, P-EDF, C-EDF, and G-NP-EDF. Comparisons are made based on schedulability and tardiness. The algorithms are implemented in a real-time Linux kernel we create called ChronOS. ChronOS extends the Linux kernel's PREEMPT_RT patch with a flexible, scalable real-time scheduling framework. Our study shows that it is possible to implement global fixed and dynamic priority real-time scheduling algorithms which will scale to large-scale multicore platforms. Interestingly, and in contrast to the conclusions of prior research, our results reveal that some global scheduling algorithms (e.g., G-NP-EDF) are scalable on 48-core machines. In our implementation, scalability is restricted by lock contention over the global schedule and the cost of interprocessor communication, rather than the global task queue implementation. We show that algorithms implemented with scalability as a first-order goal are able to provide real-time guarantees on our 48-core platform.
Parallel computation of best connections in public transportation networks
Authors: Delling Daniel , Katz Bastian , Pajor Thomas
Published: October 2012

Exploiting parallelism in route planning algorithms is a challenging algorithmic problem with obvious applications in mobile navigation and timetable information systems. In this work, we present a novel algorithm for the one-to-all
profile-search
problem in public transportation networks. It answers the question for all fastest connections between a given station S and any other station at any time of the day in a single query. This algorithm allows for a very natural parallelization, yielding excellent speed-ups on standard multicore servers. Our approach exploits the facts that, first, time-dependent travel-time functions in such networks can be represented as a special class of piecewise linear functions and, second, only few connections from S are useful to travel far away. Introducing the
connection-setting
property, we are able to extend Dijkstra's algorithm in a sound manner. Furthermore, we also accelerate station-to-station queries by preprocessing important connections within the public transportation network. As a result, we are able to compute all relevant connections between two random stations in a complete public transportation network of a big city (New York) on a standard multi-core server in real time.
Grid sifting
Authors: Bachmaier Christian , Brunner Wolfgang , Gleißner Andreas
Published: October 2012

Directed graphs are commonly drawn by the Sugiyama algorithm where first vertices are placed on distinct hierarchical levels, and second vertices on the same level are permuted to reduce the overall number of crossings. Separating these two phases simplifies the algorithms but diminishes the quality of the result.

We introduce a combined leveling and crossing reduction algorithm based on sifting, which prioritizes few crossings over few levels. It avoids type 2 conflicts, which are crossings of edges whose endpoints are dummy vertices. This helps straightening long edges spanning many levels. The obtained running time is roughly quadratic in the size of the input graph and independent of dummy vertices.
Sentiment analysis of speech prosody for dialogue adaptation in a diet suggestion program
Authors: Crouch Scott , Khosla Rajiv
Published: October 2012

In recent years, programs have been developed which allow robots to engage in simple dialogues with hospital and aged-care patients in order to provide information on and give healthrelated advice. To enable the robot to be persuasive and be accepted by the patient, it must not only understand their responses, but also understand their emotional state [1]. This information can then be used to modify the robot's responses. In an example dialogue, the robot asks whether the patient believes they overeat, to which the patient might respond "I don't overeat". If the patient has responded in a negative emotional tone, this may indicate a refusal to acknowledge the problem rather than the absence of it. In addition, the robot needs to learn to avoid responses which may provoke the patient. At that stage the goal of the robot is to convince the patient to acknowledge the problem before developing ways to solve it.

One method of collecting data about patients' emotional state is to analyze prosodic features of their speech. Prosodic features are the patterns of frequency, energy (volume), and rate of speech. Prosodic features have been known for a long time to reflect the speaker's emotional state, as was first documented by Charles Darwin in The Descent of Man [2], which also showed that, even in other animals whose vocalizations contain no linguistic properties, feelings can be expressed.

The main motivation for the development of this software is to improve upon a diet-suggestion dialogue system currently being developed and tested in aged-care homes.1 The elderly subject engages in dialogue with a health care robot, which provides suggestions to that person's diet, whilst also raising their motivation levels, and improve their perception of the robotic agent.
Knowledge discovery system for automated quality abstraction
Authors: Farooq Faisal , Yu Shipeng , Krishnapuram Balaji , Rao Bharat
Published: October 2012

To encourage the delivery of high quality care with an additional emphasis on the transparency of hospital results and reporting, the Centers for Medicare & Medicaid Services (CMS) and the Joint Commission require each hospital to submit certain inpatient core measures every quarter. In this research, we developed a system that can achieve this automatically with high accuracy for any arbitrary clinical question, in a manner that is easily user configurable/teachable.
On the choice of centralized vs decentralized systems for EPR in hospitals
Authors: Cannataro Mario , Guzzi Pietro Hiram , Tradigo Giuseppe , Veltri Pierangelo
Published: October 2012

We consider the problem of information management standardization in health structures and the problem of implementing and using automatic systems for information management. Although national and European directives have been defined, the Health Care system is still mostly focused on the deployment of core services (e.g. medicine, surgery, diagnostics) so other application such as ICT are lacking in many areas of Health Care. The goal of the ongoing study is the analysis of real cases regarding the introduction of ICT solutions for health-care, discussing centralized protocols (i.e. the use of a single information system for all the departments) versus decentralized solutions based on the development of single information systems for each department which is going to be successively integrated through ad-hoc infrastructures [1, 3].
iADRs
Authors: Lin Wen-Yang , Li He-Yi , Du Jhih-Wei , Feng Wen-Yu , Lo Chiao-Feng
Published: October 2012

Adverse Drug Reaction (ADR) is one of the most important issues on drug safety assessment. Many adverse drug reactions cannot be discovered through limited pre-marketing clinical trials; instead, they can only be recognized by a long term of post-marketing surveillance of drug usages. In this paper, we propose an interactive system platform for ADRs detection. By integrating the concept of ADRs data warehouse and innovative data mining techniques, the proposed system can not only support OLAP style of multidimensional analysis of ADRs, but also offer interactive discovery of associations between drugs and symptoms, called drug-ADR association rule, which can be further specialized by other factors interesting to users, such as demographic information. Experiments indicate that interesting and valuable drug-ADR association rules can be efficiently mined.
2011 Workshop on Visual Analytics in Healthcare
Authors: Caban Jesus J , Gotz David
Published: October 2012

This paper presents a review and summary of the 2011 Workshop on Visual Analytics in Healthcare (VAHC 2011). This was the second annual VAHC workshop and it was held in late October in conjunction with the IEEE VisWeek Conference. The primary goal of the VAHC workshop is to bring together researchers and clinicians to discuss the areas in healthcare that can benefit the most from advances in visualization and analytic systems. This review summarizes the event and provides information on how to access the electronic proceedings. In addition, we seek volunteers who are interested in helping to organize future VAHC workshops.
My Compiler Does Not Understand Me
Authors: Kamp Poul-Henning
Published: October 2012

Only lately have a lot of smart people found audiences for making sound points about what and how we code. Various colleagues have been beating drums and heads together for ages trying to make certain that wise insights about programming stick to neurons. Articles on coding style in this and other publications have provided further examples of such advocacy.
Memory Latency Hiding by Load Value Speculation for Reconfigurable Computers
Authors: Thielmann Benjamin , Huthmann Jens , Koch Andreas
Published: October 2012

Load value speculation has long been proposed as a method to hide the latency of memory accesses. It has seen very limited use in actual processors, often due to the high overhead of reexecuting misspeculated computations. We present PreCoRe, a framework capable of generating application-specific microarchitectures supporting load value speculation on reconfigurable computers. The article examines the lightweight speculation and replay mechanisms, the architecture of the actual data value prediction units as well as the impact on the nonspeculative parts of the memory system. In experiments, using PreCoRe has achieved speedups of up to 2.48 times over nonspeculative implementations.
Ecdysone Control of Developmental Transitions: Lessons from Drosophila Research
Authors: Yamanaka Naoki , Rewitz Kim F. , O'Connor Michael B.
Published: October 2012

The steroid hormone ecdysone is the central regulator of insect developmental transitions. Recent new advances in our understanding of ecdysone action have relied heavily on the application of Drosophila melanogaster molecular genetic tools to study insect metamorphosis. In this review, we focus on three major aspects of Drosophila ecdysone biology: (a) factors that regulate the timing of ecdysone release, (b) molecular basis of stage- and tissue-specific responses to ecdysone, and (c) feedback regulation and coordination of ecdysone signaling.
Autophagy as a Stress-Response and Quality-Control Mechanism: Implications for Cell Injury and Human Disease
Authors: Murrow Lyndsay , Debnath Jayanta
Published: October 2012

Autophagy, a vital catabolic process that degrades cytoplasmic components within the lysosome, is an essential cytoprotective response to pathologic stresses that occur during diseases such as cancer, ischemia, and infection. In addition to its role as a stress-response pathway, autophagy plays an essential quality-control function in the cell by promoting basal turnover of long-lived proteins and organelles, as well as by selectively degrading damaged cellular components. This homeostatic function protects against a wide variety of diseases, including neurodegeneration, myopathy, liver disease, and diabetes. This review discusses our current understanding of these two principal functions of autophagy and describes in detail how alterations in autophagy promote human disease.
(Invited) The Human Factor in Mixed-Signal Design and Its Consequences for Design and Automation
Authors: Brederlow Ralf
Published: October 2012

The semiconductor industry historically has made strong statements about analog circuits to diminish in applications. In parallel electronic design automation (EDA) industry has been committed to enable a high level of analog design automation. However, today analog circuit design reality does not look very different to the status 10 years ago – and analog design is still a common discipline in semiconductor manufacturing. This paper will analyze reason why analog design is still important and why analog design automation is not as successful as its digital counterpart. It is shown that analog circuit complexity strongly increases with the trend towards building systems on chip. Therefore solving today’s mixed signal design problems is becoming urgent. Overall here the situation is not very different from the digital verification crisis we have seen some years back in the past.
Beneficial Effect of Very Thin Active Layer on the Performance of Microcrystalline Silicon TFTs
Authors: Samb M. L. , Jacques E. , Kandoussi K. , Belarbi K. , Coulon N. , Mohammed-Brahim T.
Published: October 2012

Very thin active layer with a thickness lower than 100 nm, is shown to be beneficial for the performance of microcrystalline silicon based Thin Film Transistor thanks to the high interaction between the gate and the opposite face of the active layer. The interaction leads to improved TFT swing and high dynamic control of the threshold voltage by a second gate in front of the main one. The efficiency of the interaction is shown to be at least similar to that of fully depleted SOI-MOSFETs. Finally, the well known back channel effect in TFTs is shown to be highly reduced by the use of thin active layer.
Enhanced Terahertz Detection in Resonant Tunnel Diode-Gated HEMTs
Authors: Sensale-Rodríguez B. , Fay P. , Liu L. , Jena D. , Xing H. G.
Published: October 2012

We report our studies on terahertz detection in high electron mobility transistors (HEMTs) with a resonant-tunneling gate structure, which exhibits negative differential conductance (NDC) from gate to channel; namely, resonant-tunnel-diode (RTD) gated HEMTs. The effect of NDC on detector responsivity is theoretically derived based on Dyakonov-Shur electron-plasma wave theory. The positive gate conductance in traditional HEMTs damps the electron plasma waves, therefore reducing responsivity; conversely, in devices employing NDC gates, detector sensitivity can be greatly enhanced. Our analysis also demonstrates that resonant detection, thus high responsivity, can be obtained even near the threshold voltage in RTD-gated HEMTs, while only non-resonant detection is attainable in conventional HEMTs in this bias regime. Numerical exploration of the design space for GaN HEMTs with double-barrier AlGaN/GaN/AlGaN RTD gates is performed, showing that thin barriers with low Al composition may be the most practical structures to demonstrate this enhanced detection mechanism.
UTBOX SOI Devices with High-k Gate Dielectric Under Analog Perfomance
Authors: Galeti M. , Rodrigues M. , Aoulaiche M. , Collaert N. , Simoen E. , Claeys C. , Martino J. A.
Published: October 2012

This work presents an experimental analysis of the analog performance of UTBOX SOI devices with 20 nm silicon film thickness, 10 nm buried oxide thickness and different gate dielectrics. It was observed that a high-k gate dielectric can achieve a larger intrinsic voltage gain and Early voltage. These devices, however, have a larger low frequency noise, reduced linearity and higher GIDL current.
Liquid Helium Temperature Operation of Graded-Channel SOI nMOSFETs
Authors: de Souza M. , Kilchytska V. , Flandre D. , Pavanello M. A.
Published: October 2012

This work reports, for the first time, the operation of Graded-Channel SOI nMOSFETs at liquid helium temperature. As expected, for all measured devices it has been observed that at 4.2K the transconductance increases with respect to room temperature as a consequence of the mobility rise. On the opposite hand, all the studied devices demonstrated a degradation of the output conductance with temperature reduction. However, this degradation is attenuated below 90K. As a consequence, an increase of the Early voltage and of the intrinsic voltage gain were obtained, in contrast to the data reported in the literature, for devices operating down to 100K. It is demonstrated that GC SOI presented larger Early voltage increase at 4.2K than at room temperature. The rise of the voltage gain promoted by GC architecture has shown to be constant with temperature down to 4.2K.
Evaluation of Graphene Oxidation Methods
Authors: Campos C.D. M. , Veríssimo C. , Moshkalev S. A.
Published: October 2012

Graphene oxide is one of the most important graphene derivates. Due to its unique chemical properties, this compound is largely used as starting point for functionalized products. Functional groups present in grapheme oxide surface have large influence in the following steps of these reactions. Here, we make the evaluation of three different routes to obtain graphene oxide, and which functional groups are present in each product. Based on results, it was possible to conclude that different routes may favor the formation of specific functional groups.
Application of Junctionless Nanowire Transistor in the Self-Cascode Configuration to Improve the Analog Performance
Authors: Doria R. T. , Trevisoli R. D. , de Souza M. , Pavanello M. A.
Published: October 2012

The self-cascode (SC) configuration consists in a series association of two transistors with tied gates usually applied to improve the analog performance of MOS devices. This paper compares the analog parameters of single Junctionless transistors with the ones presented by self-cascode associations composed by two Junctionless devices with identical or different fin widths (symmetric and asymmetric, respectively). The transconductance to the drain current ratio, the Early voltage (V

EA
) and the intrinsic voltage gain (A

V
) have been evaluated for both single devices and SC structures. It has been shown that the SC configurations, specially the asymmetric ones, present a strong reduction of the drain conductance (g

D
) with respect to single devices, resulting in an increase of V

EA
and A

V
, which can be higher than 30 dB depending on the bias conditions.
Fabrication of Transparent Conductive Thin Films Based on Multi-Walled Carbon Nanotubes
Authors: Abe I. Y. , Pereyra I.
Published: October 2012

In this work, thin films of multi-walled carbon nanotubes (MWCNT) were deposited on glass substrates utilizing the dip coating method, utilizing a surfactant to dissolute the CNT in water, aiming their application as transparent conductive contacts. Different surface preparation and CNT concentrations were tested. The electrical, optical and morphological properties were characterized. The results indicate the formation of a non uniform film with CNT aggregates distributed on the surface. Residual surfactant remains in the films, decreasing the transparency of the film. The DI water rinse stage after deposition removes not only surfactant, but also small portions of CNT thin layers, affecting the conductivity of the films. Better results were obtained for the intermediate CNT concentration tested, however other surfactant should be tested to improve film uniformity and conductivity.
Analysis of Resistance Change Development Due to Voiding in Copper Interconnects Ended by A Through Silicon Via
Authors: de Orio R. L. , Ceric H. , Selberherr Siegfried
Published: October 2012

The resistance change due to electromigration induced voiding in modern copper interconnects ended by a Through Silicon Via (TSV) is analyzed. It is shown that two different modes of resistance increase exist during the period of void growth under the TSV. Primarily responsible are imperfections at the TSV bottom introduced during the fabrication process. Consequently, the time to failure of such structures under electromigration stress is likely to follow a bimodal distribution. An analytical model is proposed to explain the resistance change development based on published experimental data and also on numerical simulations.
Piecewise-Linear Algorithm Applied to R2 Experimental Plasma Etching Process
Authors: Jimenez-Fernandez V. , Reyes-Betanzo C. , Hernandez-Paxtian Z. J.
Published: October 2012

Sometimes the only information that is available to characterize an experimental process is a collection of input-output data. In those cases, piecewise linear (PWL) interpolation is an optimal strategy to fit the data into a curve. This paper computing plasma parameters of pressure and RF power as input data that corresponds with a specific silicon etch rate as the output datum in a two dimensional experiment whose behavior is described by a R

2
PWL curve. The computation is approached by a numerical algorithm which scans all the discrete input data distributed in a simplicial form.