bluuebunny/crossref_metadata_2025 huggingface dataset:
Syntactic control of interference for separation logic
Authors: Reddy Uday S. , Reynolds John C.
Published: October 2012

Separation Logic has witnessed tremendous success in recent years in reasoning about programs that deal with heap storage. Its success owes to the fundamental principle that one should keep separate areas of the heap storage separate in program reasoning. However, the way Separation Logic deals with program variables continues to be based on traditional Hoare Logic without taking any benefit of the separation principle. This has led to unwieldy proof rules suffering from lack of clarity as well as questions surrounding their soundness. In this paper, we extend the separation idea to the treatment of variables in Separation Logic, especially Concurrent Separation Logic, using the system of Syntactic Control of Interference proposed by Reynolds in 1978. We extend the original system with permission algebras, making it more powerful and able to deal with the issues of concurrent programs. The result is a streamined presentation of Concurrent Separation Logic, whose rules are memorable and soundness obvious. We also include a discussion of how the new rules impact the semantics and devise static analysis techniques to infer the required permissions automatically.
Algebraic foundations for effect-dependent optimisations
Authors: Kammar Ohad , Plotkin Gordon D.
Published: October 2012

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi's monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols. We develop an annotated version of Levy's Call-by-Push-Value language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).
Towards nominal computation
Authors: Bojanczyk Mikolaj , Braud Laurent , Klin Bartek , Lasota Slawomir
Published: October 2012

Nominal sets are a different kind of set theory, with a more relaxed notion of finiteness. They offer an elegant formalism for describing lambda-terms modulo alpha-conversion, or automata on data words. This paper is an attempt at defining computation in nominal sets. We present a rudimentary programming language, called Nlambda. The key idea is that it includes a native type for finite sets in the nominal sense. To illustrate the power of our language, we write short programs that process automata on data words.
Formalizing the LLVM intermediate representation for verified program transformations
Authors: Zhao Jianzhou , Nagarakatte Santosh , Martin Milo M.K. , Zdancewic Steve
Published: October 2012

This paper presents Vellvm (verified LLVM), a framework for reasoning about programs expressed in LLVM's intermediate representation and transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM's intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate different reasoning styles and proof techniques.

To validate Vellvm's design, we extract an interpreter from the Coq formal semantics that can execute programs from LLVM test suite and thus be compared against LLVM reference implementations. To demonstrate Vellvm's practicality, we formalize and verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm's tools allow us to extract a new, verified implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance is competitive with the non-verified, ad-hoc original.
A rely-guarantee-based simulation for verifying concurrent program transformations
Authors: Liang Hongjin , Feng Xinyu , Fu Ming
Published: October 2012

Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be preserved in general with the presence of parallel compositions, due to instruction reordering and the different granularities of atomic operations at the source and the target. On the other hand, the refinement relation defined based on fully abstract semantics of concurrent programs assumes arbitrary parallel environments, which is too strong and cannot be satisfied by many well-known transformations. In this paper, we propose a Rely-Guarantee-based Simulation (RGSim) to verify concurrent program transformations. The relation is parametrized with constraints of the environments that the source and the target programs may compose with. It considers the interference between threads and their environments, thus is less permissive than relations over sequential programs. It is compositional w.r.t. parallel compositions as long as the constraints are satisfied. Also, RGSim does not require semantics preservation under all environments, and can incorporate the assumptions about environments made by specific program transformations in the form of rely/guarantee conditions. We use RGSim to reason about optimizations and prove atomicity of concurrent objects. We also propose a general garbage collector verification framework based on RGSim, and verify the Boehm et al. concurrent mark-sweep GC.
The ins and outs of gradual type inference
Authors: Rastogi Aseem , Chaudhuri Avik , Hosmer Basil
Published: October 2012

Gradual typing lets programmers evolve their dynamically typed programs by gradually adding explicit type annotations, which confer benefits like improved performance and fewer run-time failures.

However, we argue that such evolution often requires a giant leap, and that type inference can offer a crucial missing step. If omitted type annotations are interpreted as unknown types, rather than the dynamic type, then static types can often be inferred, thereby removing unnecessary assumptions of the dynamic type. The remaining assumptions of the dynamic type may then be removed by either reasoning outside the static type system, or restructuring the code.

We present a type inference algorithm that can improve the performance of existing gradually typed programs without introducing any new run-time failures. To account for dynamic typing, types that flow in to an unknown type are treated in a fundamentally different manner than types that flow out. Furthermore, in the interests of backward-compatibility, an escape analysis is conducted to decide which types are safe to infer. We have implemented our algorithm for ActionScript, and evaluated it on the SunSpider and V8 benchmark suites. We demonstrate that our algorithm can improve the performance of unannotated programs as well as recover most of the type annotations in annotated programs.
An executable formal semantics of C with applications
Authors: Ellison Chucky , Rosu Grigore
Published: October 2012

This paper describes an executable formal semantics of C. Being executable, the semantics has been thoroughly tested against the GCC torture test suite and successfully passes 99.2% of 776 test programs. It is the most complete and thoroughly tested formal definition of C to date. The semantics yields an interpreter, debugger, state space search tool, and model checker "for free". The semantics is shown capable of automatically finding program errors, both statically and at runtime. It is also used to enumerate nondeterministic behavior.
A type theory for probability density functions
Authors: Bhat Sooraj , Agarwal Ashish , Vuduc Richard , Gray Alexander
Published: October 2012

There has been great interest in creating probabilistic programming languages to simplify the coding of statistical tasks; however, there still does not exist a formal language that simultaneously provides (1) continuous probability distributions, (2) the ability to naturally express custom probabilistic models, and (3) probability density functions (PDFs). This collection of features is necessary for mechanizing fundamental statistical techniques. We formalize the first probabilistic language that exhibits these features, and it serves as a foundational framework for extending the ideas to more general languages. Particularly novel are our type system for absolutely continuous (AC) distributions (those which permit PDFs) and our PDF calculation procedure, which calculates PDF s for a large class of AC distributions. Our formalization paves the way toward the rigorous encoding of powerful statistical reformulations.
A type system for borrowing permissions
Authors: Naden Karl , Bocchino Robert , Aldrich Jonathan , Bierhoff Kevin
Published: October 2012

In object-oriented programming, unique permissions to object references are useful for checking correctness properties such as consistency of typestate and noninterference of concurrency. To be usable, unique permissions must be
borrowed
--- for example, one must be able to read a unique reference out of a field, use it for something, and put it back. While one can null out the field and later reassign it, this paradigm is ungainly and requires unnecessary writes, potentially hurting cache performance. Therefore, in practice borrowing must occur in the type system, without requiring memory updates. Previous systems support borrowing with external alias analysis and/or explicit programmer management of
fractional permissions
. While these approaches are powerful, they are also awkward and difficult for programmers to understand. We present an integrated language and type system with unique, immutable, and shared permissions, together with new
local permissions
that say that a reference may not be stored to the heap. Our system also includes
change permissions
such as unique>>unique and unique>>none that describe how permissions flow in and out of method formal parameters. Together, these features support common patterns of borrowing, including borrowing multiple local permissions from a unique reference and recovering the unique reference when the local permissions go out of scope, without any explicit management of fractions in the source language. All accounting of fractional permissions is done by the type system "under the hood." We present the syntax and static and dynamic semantics of a formal core language and state soundness results. We also illustrate the utility and practicality of our design by using it to express several realistic examples.
Fast local search for the steiner problem in graphs
Authors: Uchoa Eduardo , Werneck Renato F.
Published: October 2012

We present efficient algorithms that implement four local searches for the Steiner problem in graphs: vertex insertion, vertex elimination, key-path exchange, and key-vertex elimination. In each case, we show how to find an improving solution (or prove that none exists in the neighborhood) in O(m log n) time on graphs with n vertices and m edges. Many of the techniques and data structures we use are relevant in the study of dynamic graphs in general, beyond Steiner trees. Besides the theoretical interest, our results have practical impact: These local searches have been shown to find good-quality solutions in practice, but high running times limited their applicability.
StreamKM++
Authors: Ackermann Marcel R. , Märtens Marcus , Raupach Christoph , Swierkot Kamil , Lammersen Christiane , Sohler Christian
Published: October 2012

We develop a new k-means clustering algorithm for data streams of points from a Euclidean space. We call this algorithm StreamKM++. Our algorithm computes a small weighted sample of the data stream and solves the problem on the sample using the k-means++ algorithm of Arthur and Vassilvitskii (SODA '07). To compute the small sample, we propose two new techniques. First, we use an adaptive, nonuniform sampling approach similar to the k-means++ seeding procedure to obtain small coresets from the data stream. This construction is rather easy to implement and, unlike other coreset constructions, its running time has only a small dependency on the dimensionality of the data. Second, we propose a new data structure, which we call coreset tree. The use of these coreset trees significantly speeds up the time necessary for the adaptive, nonuniform sampling during our coreset construction.

We compare our algorithm experimentally with two well-known streaming implementations: BIRCH [Zhang et al. 1997] and StreamLS [Guha et al. 2003]. In terms of quality (sum of squared errors), our algorithm is comparable with StreamLS and significantly better than BIRCH (up to a factor of 2). Besides, BIRCH requires significant effort to tune its parameters. In terms of running time, our algorithm is slower than BIRCH. Comparing the running time with StreamLS, it turns out that our algorithm scalesmuch better with increasing number of centers. We conclude that, if the first priority is the quality of the clustering, then our algorithm provides a good alternative to BIRCH and StreamLS, in particular, if the number of cluster centers is large. We also give a theoretical justification of our approach by proving that our sample set is a small coreset in low-dimensional spaces.
Efficient relaxed search in hierarchically clustered sequence datasets
Authors: Bader Kai C. , Atallah Mikhail J. , Grothoff Christian
Published: October 2012

This article presents a new algorithm for finding oligonucleotide signatures that are specific and sensitive for organisms or groups of organisms in large-scale sequence datasets. We assume that the organisms have been organized in a hierarchy, for example, a phylogenetic tree. The resulting signatures, binding sites for primers and probes, match the maximum possible number of organisms in the target group while having at most
k
matches outside of the target group.

The key step in the algorithm is the use of the lowest common ancestor (LCA) to search the organism hierarchy; this allows the combinatorial problem in almost linear time (empirically observed) to be solved. The presented algorithm improves performance by several orders of magnitude in terms of both memory consumption and runtime when compared to the best-known previous algorithms while giving identical, exact solutions.

This article gives a formal description of the algorithm, discusses details of our concrete, publicly available implementation, and presents the results from our performance evaluation.
A topological sorting algorithm for large graphs
Authors: Ajwani Deepak , Cosgaya-Lozano Adan , Zeh Norbert
Published: October 2012

We present an I/O-efficient algorithm for topologically sorting directed acyclic graphs, called IterTS. In the worst case, our algorithm is extremely inefficient and performs O(
n
ċ sort(
m
)) I/Os. However, our experiments show that IterTS achieves good performance in practice. To evaluate IterTS, we compared its running time to those of three competitors: PeelTS, an I/O-efficient implementation of the standard strategy of iteratively removing sources and sinks; ReachTS, an I/O-efficient implementation of a recent parallel divide-and-conquer algorithm based on reachability queries; and SeTS, a standard DFS-based topological sorting built on top of a semiexternal DFS algorithm. In our evaluation on various types of input graphs, IterTS consistently outperformed PeelTS and ReachTS by at least an order of magnitude in most cases. SeTS outperformed IterTS on most graphs whose vertex sets fit in memory. However, IterTS often came close to the running time of SeTS on these inputs and, more importantly, SeTS was not able to process graphs whose vertex sets were beyond the size of main memory, while IterTS was able to process such inputs efficiently.
Fast k-selection algorithms for graphics processing units
Authors: Alabi Tolu , Blanchard Jeffrey D. , Gordon Bradley , Steinbach Russel
Published: October 2012

Finding the kth-largest value in a list of n values is a well-studied problem for which many algorithms have been proposed. A naïve approach is to sort the list and then simply select the kth term in the sorted list. However, when the sorted list is not needed, this method does quite a bit of unnecessary work. Although sorting can be accomplished efficiently when working with a graphics processing unit (GPU), this article proposes two GPU algorithms, radixSelect and bucketSelect, which are several times faster than sorting the vector. As the problem size grows so does the time savings of these algorithms with a sixfold speed-up over GPU sorting for float vectors larger than 2
24
and for double vectors larger than 2
20
, ultimately reaching a 19.1 times speed-up for double vectors of length 2
28
.
Situation role-based privacy control using dynamic credentials for emergency health services
Authors: Chun Soon Ae , Kwon Joon Hee , Lee Haesung
Published: October 2012

Emerging Health Information Technologies (HIT) such as Electronic Health Record (EHR) and PHR systems and Heath Information Exchanges (HIEs) facilitate access to and sharing of patients' medical data distributed in different HIT systems. One of the many major challenges to overcome for EHRs to be successful and for sharing of patient information across different EHR systems in the HIE environment is patient privacy. Typically a patient has medical records in various providers' EHR systems. In this diversely distributed system, it is difficult to ensure the consistent privacy control of distributed health information of the patient. Currently, a patient in the initial visit to a doctor's office fills out a paper-based questionnaire regarding health information privacy and release permissions and how his or her own heath information may be shared. It is difficult to ensure that privacy is controlled in the manner a patient specifies or to ensure that healthcare providers honor the privacy specifications by the patient about sharing and using his or her own health data. The patient simply relies on the organization's policy in good faith, but has no control over who can access what and how her own data can be shared and used.
An agenda for ultra-large-scale system research for global health informatics
Authors: Facelli Julio C.
Published: October 2012

This extended abstract describes the characteristics of Ultra- Large-Scale Systems (ULSS) and the gaps in our understanding of these systems. We compare the characteristics of ULSS with the desired characteristics for national and global health information systems. Using the methodology proposed for the US Department of Defense and representative global health scenarios, we identify a strategy to develop a research agenda in Ultra-Large-Scale-Systems for Global Health Informatics.
A new paradigm for the development of future medical software systems
Authors: Meixner Gerrit , Zuehlke Detlef
Published: October 2012

In many areas of human life, computer-based Information Technology (IT) has prevailed and become essential for the coordinated and efficient organization of workflows. Especially in the field of health care, interaction between human beings and IT is a sensitive subject. Inevitably, people working in the field of health care will have to make use of the potentials of IT in order to meet the enormous demands on e.g. patient management. When we look at the situation of current medical software systems, we can find major advances in the performance capacities of modern software systems, but must also note their rapid penetration into almost every facet of the daily hospital routine. Today medical software systems can be characterized as a vast number of (networked) software which each fulfills specific functions (e.g., hospital information system, Picture Archiving and Communication System) and which is used by different user groups (e.g., physicians, nurses, medical secretaries) with diverse user tasks [4]. Yet, for almost two decades, graphical user interfaces have dominated the interaction of medical software systems in most cases. In the future, a broader range of paradigms will emerge, allowing for multi-modal interaction. But also the growing number of heterogeneous platforms (operating systems, graphical libraries) and devices utilized complementarily (e.g., PC, Toughbook, Smartphone, PDA) demand for the development of congeneric user interfaces for a plethora of target platforms. Especially "mobile healthcare computing devices (MHCDs) are rapidly becoming an integral part of hospital information systems. Deployment of these devices is becoming an important IT strategy designed to assist in improving quality of care, enhancing patient services, increasing productivity, lowering costs, improving cash flow, as well as facilitating other critical delivery processes" [3]. For MHCDs aspects like getting the right information at the right time in the right place (context sensitivity) is important.

To be able to cope with requirements like interoperability, context-sensitivity and device-independent usage a model-based approach for the development of user interfaces (MBUID) appears to be favourable [2].
Connection between traditional medicine and disease
Authors: Katayama Kotoe , Yamaguchi Rui , Imoto Seiya , Matsuura Keiko , Watanabe Kenji , Imoto Seiya
Published: October 2012

In Japanese traditional medicine, "Monshin" plays an important role. "Monshin" is a questionnaire that asked the patient's lifestyle and subjective symptoms. Specialists decide traditional herbal medicine by using of "Monshin". In this research, we connect "Monshin" to disease through building the Network.
Addressing extensibility requirements for health informatics data
Authors: Shankar Mallikarjun , Tomkins-Tinch Christopher
Published: October 2012

The electronic health record (EHR) is a key artifact that threads the workflow from medical encounters to resolution (treatments and claims disposition) - it aims to provide a longitudinal view into a patient's interaction with care providers within an institution to enable better and streamlined care. The EHR must front a variety of information sources which can vary and evolve over time, creating natural challenges for data representation, storage, retrieval, and information mutation. We argue that underlying data systems must store information in a flexible manner to allow EHR and other systems to insert and extract data without rigid constraints and strict or
a priori
defined schemas.
Organizing RadLex lexicon for efficient retrieval of radiology documents
Authors: Ramakrishnan I. V. , Tithi J. J. , Bagate A. , Khot V. , Ahmed F. , Harrington D. , Talati R.
Published: October 2012

As more and more medical reports go online there is a move in the medical community to standardize the terminology used in these reports. The expectation is that uniformity of vocabulary can reduce variations and hence significantly aid the organization and retrieval of medical documents with modern search engines. Even medical specialties are beginning to realize the potential benefits and are getting together to develop standards for the individual specialties. In the specialty of Radiology, RadLex is the standardized lexicon developed by the Radiological Society of North America. A standardized term in RadLex is assigned one unique category from among: preferred name, synonym and abbreviation. The size of RadLex (over 12,000 terms) makes it difficult to recall a term and all its synonyms and abbreviations. From a usability perspective it is highly desirable to search with a single RadLex term and let the search engine transparently retrieve not only all the documents in which the term appears but also all the other documents created with related terms (synonyms and abbreviations) Towards that we propose an automata-based organization of RadLex lexicon to facilitate efficient retrieval of radiology documents with RadLex search terms. The automaton is used at index creation time to identify RadLex terms in a document and augment its indexes with additional terms related to those identified by the automaton. A distinguishing aspect of the approach is its computational efficiency and its broad applicability to medical Information Retrieval (IR) applications.
Modeling People and Places with Internet Photo Collections
Authors: Crandall David , Snavely Noah
Published: October 2012

This article describes our work in using online photo collections to reconstruct information about the world and its inhabitants at both global and local scales. This work has been driven by the dramatic growth of social content-sharing Web sites, which have created immense online collections of user-generated visual data. Flickr.com alone currently hosts more than 6 billion images taken by more than 40 million unique users, while Facebook.com has said it grows by nearly 250 million photos every day.
Thelytokous Parthenogenesis in Eusocial Hymenoptera
Authors: Rabeling Christian , Kronauer Daniel J.C.
Published: October 2012

Female parthenogenesis, or thelytoky, is particularly common in solitary Hymenoptera. Only more recently has it become clear that many eusocial species also regularly reproduce thelytokously, and here we provide a comprehensive overview. Especially in ants, thelytoky underlies a variety of idiosyncratic life histories with unique evolutionary and ecological consequences. In all eusocial species studied, thelytoky probably has a nuclear genetic basis and the underlying cytological mechanism retains high levels of heterozygosity. This is in striking contrast to many solitary wasps, in which thelytoky is often induced by cytoplasmic bacteria and results in an immediate loss of heterozygosity. These differences are likely related to differences in haplodiploid sex determination mechanisms, which in eusocial species usually require heterozygosity for female development. At the same time, haplodiploidy might account for important preadaptations that can help explain the apparent ease with which Hymenoptera transition between sexual and asexual reproduction.
Pathogenesis of Immunoglobulin A Nephropathy: Recent Insight from Genetic Studies
Authors: Kiryluk Krzysztof , Novak Jan , Gharavi Ali G.
Published: October 2012

Recent genome-wide association studies (GWAS) have identified multiple susceptibility loci for immunoglobulin A nephropathy (IgAN), the most common form of glomerulonephritis, implicating independent defects in adaptive immunity (three loci on chromosome 6p21 in the MHC region), innate immunity (8p23 DEFA locus, 17p23 TNFSF13 locus, 22q12 HORMAD2 locus), and the alternative complement pathway (1q32 CFH/CFHR locus). In geospatial analysis of 85 populations, a genetic risk score based on the replicated GWAS loci is highest in Asians, intermediate in Europeans, and lowest in Africans, capturing the known difference in prevalence among world populations. The genetic risk score also uncovered a previously unsuspected increased prevalence of IgAN-attributable kidney failure in Northern Europe. The IgAN risk alleles have opposing effects on many immune-mediated diseases, suggesting that selection has contributed to variation in risk allele frequencies among different populations. Incorporating genetic, immunologic, and biochemical data, we present a multistep pathogenesis model that provides testable hypotheses for dissecting the mechanisms of disease.
(Keynote) History and Future Directions in SiGe HBT BiCMOS Technology and Its Applications
Authors: Harame D. , Joseph A. , Cheng P. , Jain V. , Camillo-Castillo R.
Published: October 2012

The development of SiGe BiCMOS has mirrored silicon semiconductor development as the technology transitioned from Ge transistors, to silicon transistors, to ion-implanted base, to polysilicon emitter transistors, and finally to SiGe HBTs and SiGe BiCMOS. While the physics of the graded base SiGe HBT transistor was established early on in 1954 by Herb Kroemer it was not until the 1980s that SiGe HBTs were first realized. At the core of the SiGe Heterojunction Bipolar transistor development is the SiGe Epitaxy. In fact the SiGe HBT drove the development of the SiGe:B S/D processes now used for stressors in advanced CMOS since it was the first commercial technology with SiGe layers. SiGe HBT BiCMOS continues to find large volume production opportunities in applications that require mostly RF/Analog and less digital content (Big-A/little-D). Scaling has driven the speed performance (
f

MAX
) towards terahertz levels to open up yet more applications. Many challenges still exist in the technology.
(Invited) SOI Technologies from Microelectronics to Microsystems - Meeting the
More than Moore
Roadmap Requirements
Authors: Raskin Jean-Pierre
Published: October 2012

This last decade Silicon-on-Insulator (SOI) MOSFET technology has demonstrated its potentialities for high frequency (reaching cut-off frequencies close to 500 GHz for nMOSFETs) and for harsh environments (high temperature, radiation) commercial applications. SOI also presents high resistivity substrate capabilities, leading to substantially reduced substrate losses. More recently, SOI technology has been emerging as a major contender for heterogeneous microsystems applications. In this work, we demonstrate the advantages of SOI technology for RF CMOS integration as well as for building thin film sensors on thin dielectric membrane and three-dimensional micro-electromechanical (MEMS) sensors and actuators co-integrated with their associated SOI CMOS circuitry.
(Invited) Overview of Fully Depleted SOI Technology and Circuit Benefits
Authors: Mazure Carlos , Nguyen Bich-Yen
Published: October 2012

FDSOI is a technology platform which is particularly suited for mobile IC applications targeting high speed at low-voltage operation. This review focuses on the properties and benefits of a fully depleted architecture and advantages at the IC level.
On the Variability of the Low-Frequency Noise in UTBOX SOI nMOSFETs
Authors: Simoen E. , Andrade G.M. C. , Mendes Almeida L. , Aoulaiche M. , Caillat C. , Jurczak M. , Claeys C.
Published: October 2012

The variability of the low-frequency (LF) noise in n-channel MOSFETs fabricated on an Ultra Thin Buried Oxide (UTBOX) Silicon-on-Insulator (SOI) substrate has been studied and compared with the variability in the threshold voltage and low-field mobility of the same devices. No correlation has been found between the noise magnitude and the DC parameters, suggesting that the traps responsible for the current fluctuations do not affect the latter. A possible explanation is that the LF noise is dominated by Generation-Recombination (GR) centers in the silicon film, which have less impact on the drain current.
Analysis of Total Ionizing Dose Effects on a Pseudo-Static Random Access Memory (PSRAM)
Authors: Both T. H. , Wirth Gilson I. , Pereira Junior E. C. F. , Gonçalez O. L. , Vaz R. G. , Pereira M. A. , Milagres D. C.
Published: October 2012

The purpose of this work is to describe the total ionizing dose effects on a commercial ISSI 4Mb pseudo-static random access memory (PSRAM). Experimental results from an irradiation test performed at the Ionizing Radiation Laboratory at Instituto de Estudos Avançados (LRI/IEAv) using a Co-60 gamma-radiation source were analyzed and compared to simulation results of typical memory circuits and typical memory architecture, in order to identify error patterns and failure mechanisms.
Comparative Study of Biaxial and Uniaxial Mechanical Stress Influence on the Low Frequency Noise of Fully Depleted SOI nMOSFETs Operating in Triode and Saturation Regime
Authors: de Souza M.A. S. , Doria R. T. , de Souza M. , Martino J. A. , Pavanello M. A.
Published: October 2012

This paper presents an experimental comparative study of uniaxial and biaxial strain techniques influence on the low frequency noise of planar fully depleted SOI nMOSFETs operating in linear and saturation regimes. The comparison between devices from the same technology with these two strained techniques demonstrated a reduction of low frequency noise for devices with both strain technologies in linear regime for shorter devices (below 410 nm). In saturation regime the reduction of low frequency noise for uniaxial and biaxial strain also occurs, but does not depend on the channel length, and the reduction of low frequency noise in favor of both strain technologies is more pronounced for channel length of 160 nm.
Phenomenological Modeling of Charge Injection - Beyond the Schottky Barrier Paradigm
Authors: Blawid S. , Claus M. , Schröter M.
Published: October 2012

We (re-)investigate the charge injection across a heterojunction of one-dimensional semiconductors by analytical means and by solving self-consistently the effective-mass Schrödinger and the Poisson equation. The charge injection is generally determined by the value of the Schottky barrier. However, we find that a potential step and an effective mass discontinuity across the junction have considerable impact on the charge injection and thus the junction transparency. The impact of the junction transparency on the DC characteristics of a fully gated 50nm carbon nanotube field-effect transistor is demonstrated and device optimization criteria are briefly discussed.
Current Degradation in GaN HEMTs: Is Self-Heating Responsible
Authors: Padmanabhan Balaji , Vasileska Dragica , Goodnick Stephen M.
Published: October 2012

Electrical reliability of GaN HEMT system in both the on state and the off state regime is still a fundamental problem to be solved. To get an insight for the occurrence of the current collapse phenomena in GaN HEMTs, an electro-thermal particle based device simulator consisting of a Monte Carlo-Poisson solver, self consistently coupled with an energy balance solver for both acoustic and optical phonons, was developed. We observe that the incorporation of self-heating effects leads to an increase in the vertical electric field in the gate to drain extension region which can lead to large charge trapping on the surface and also the possibility of forming cracks or pits.
A New Analytic Model for Double Gate FinFETs Parasitic Resistance
Authors: Pereira A.S. N. , Giacomini R.
Published: October 2012

A new analytic model for Parasitic Resistance of Double Gate FinFETs is proposed in this work. The model was developed considering the current distribution observed in three-dimensional simulations. The contact resistance was modeled using a variable impedance transmission line model, to approximate source and drain geometries to the real shapes of these regions. The model has a closed expression, without adjustment parameters and is very accurate when compared to simulation results and published experimental data.
Stress Conditions to Study the Reliability Characteristics of High-k Nanolaminates
Authors: Quinteros C. P. , Palumbo F. , Campabadal F. , Miranda E.
Published: October 2012

Constant voltage stressing is a standard technique to test the reliability characteristics of dielectrics used as gate insulator in MOS structures. In this work, the importance of choosing the appropriate voltage to perform stress measurements is assessed. Based on the particular dielectric permittivities and thicknesses, different operating regions in Al2O3, HfO2 and nanolaminates of both materials in terms of their breakdown voltages were established. Preliminary results seem to indicate that there is a strongly relationship between the Weibull breakdown statistics and the applied stress voltage.
Experimental Validation of the Drain Current Analytical Model of the Fully Depleted Diamond SOI nMOSFETs by Using Paired T-test Statistical Evaluation
Authors: Peruzzi V. V. , Renaux C. , Flandre D. , Gimenez S. P.
Published: October 2012

The focus of this work is to validate the drain current analytical model of the Fully Depleted Diamond SOI nMOSFETs, by applying the paired t-test statistical evaluation with experimental data of the six different samples of integrated circuits containing different Diamond SOI MOSFETs and Conventional ones counterparts. Two parameters are considered in this work: maximum transconductance and saturation drain current. We observe that, for the most cases (worst case is around 85% of the repeatability for the saturation drain current), the Diamond drain current analytical model is capable to reproduce a similar statistical behavior than the one observed for the conventional SOI nMOSFET counterpart, considering the same bias conditions and SOI CMOS manufacturing process of the integrated circuits.
Simulation of a Miller OpAmp with FinFETs at High Temperatures
Authors: Contreras E. , Cerdeira A. , Pavanello M. A.
Published: October 2012

For practical applications temperature can play an important role in the performance of a circuit. This paper describes the performance of a Miller Operational Amplifier with FinFET transistors operating in a wide temperature range by circuit simulation. FinFETs were modeled using the Symmetric Doped Double-Gate Model introduced in SmartSPICE circuit simulator calibrated with measured data. Amplifier simulation, performed at 27ºC, 100ºC and 200ºC, reproduced the amplifier behavior and the variation of gain and cutoff frequency.
Micro-Reactors for Testing Sensor Devices Based on Suspended Carbon Nanotubes
Authors: Savu R. , Silveira J. V. , Flacker A. , Vaz A. R. , Joanni E. , Gobbi A. L. , Rotondaro A.L. P. , Moshkalev S. A.
Published: October 2012

In this work, we report the fabrication of micro-reactors for the characterization of nano-sensors based on suspended nanoparticle-decorated carbon nanotubes (CNTs/NPs). The capsules were fabricated from a single Kovar® piece, having a small volume chamber (100µl). Gold thin films were sputtered onto Si/SiO2 substrates and the electrodes were patterned using electrochemical deposition, photolithography and wet chemical corrosion. In order to obtain devices based on suspended nanotubes, prior to CNTs deposition, a 1µm wide and 5µm deep gap was milled in the substrate by focused ion beam (FIB). The dielectrophoresis (DEP) technique was used for the deposition of the suspended CNTs over the as obtained patterned electrodes. The sensors were tested using oxygen and nitrogen atmospheres, in the pressure range between 10-5 and 10-1mbar. The small chamber volume allowed the measurement of fast sensor characteristic times, with the sensors showing good sensitivity towards gas and pressure as well as high reproducibility.
TiO2 Nanotubes Production and Characterization
Authors: Fraga T. M. , Albertin K. F. , Pereyra I.
Published: October 2012

TiO2 nanotubes arrays were obtained by Ti foil and Ti thin films on glass substrate, deposited by RF magnetron sputtering, anodization in a NH4F organic solution with different anodization voltages and times. Annealing treatment to promote nanotubes crystallization in anatase phase was done. Different photolithography pattern techniques were utilized to define nanotubes lines from 10 to 90µm wide. The obtained samples were characterized by Raman spectroscopy and Scanning Electron Microscopy (SEM).
Accounting for Short Channel Effects in the Drain Current Modeling of Junctionless Nanowire Transistors
Authors: Trevisoli R. D. , Doria R. T. , de Souza M. , Pavanello M. A.
Published: October 2012

Junctionless nanowire transistors have a constant doping profile from source to drain, providing a great scalability without the need of rigorously controlled doping gradients and activation techniques. Therefore, these devices are considered as promising for decananometer era. This work proposes an analytical model for the drain current in junctionless nanowire transistor (JNT) accounting for short channel effects and temperature dependence. Tridimensional numerical simulations of p-type devices have been performed to validate the model. Experimental data of n-type devices have also been used.
Impact of the Extension Region Concentration on the UTBOX 1T-FBRAM
Authors: Sasaki K. R. A. , Almeida L. M. , Martino J. A.
Published: October 2012

The goal of this work is to analyze the impact of different extension region concentrations on the programming window and retention time of an UTBOX 1T-DRAM performance through 2D numerical simulations. It is also included some analysis of an extension-less UTBOX device, which presented three order of magnitude higher retention time for the extension-less device, even using a higher drain bias to read. It was observed that each structure showed different optimum biases conditions.
Simulation of PECVD SiO2 Deposition Using a Cellular Automata Approach
Authors: Colombo F. B. , Carreño M.N. P.
Published: October 2012

A cellular model to simulate PECVD SiO2 deposition is described. The automaton is based on a cellular approach described by Strasser and Selberherr. The automaton parameters effects on the resulting films are analyzed. The results generated by the simulator are also compared to experimental results of the fabrication of a pedestal ARROW.
Influence of Silicon Binding Energy on Photoluminescence of Si-Implanted Silicon Dioxide
Authors: González-Fernández A. A. , Juvert J. , Aceves-Mijares M. , Llobera A. , Domínguez C,
Published: October 2012

Studies of photo-luminescence (PL) and X-ray Photoelectron Spectroscopy (XPS) were performed to silicon-rich silicon dioxide films (SRO) fabricated by implantation of Si ions on SiO2 deposited by plasma enhanced chemical vapor deposition (PECVD). Samples presented PL spectra formed by the contribution of two bands, respectively related to defects and quantum confinement (QC). The XPS results for the different samples presented significant differences in the density and types of Si-Si and Si-O bonds. A relation was observed between the types of Si bonds and the PL characteristics presented by the material, obtaining a modulation of the emission spectra trough the change of the implantation dose.
Porous Silicon Photonic Crystals: Influence of Electrolyte Composition on the Nanostructure and the Optical Response
Authors: Huanca Danilo Roque , Elias Vinícius Freire , Salcedo Walter Jaimes
Published: October 2012

Porous silicon photonic crystal devices with and without microcavity were fabricated anodizing p+-silicon into electrolyte with different chemical composition. They were made in order to study the effect of the electrolyte composition upon their structural properties and on their optical response. It was found that low HFelectrolytes yield structures with high porosity, weak mechanical stability and low effective refractive index. However, the addition of water into this electrolyte leads to the formation of layers with high refractive index and strong mechanical stability. In addition, the interface roughnesses of them are also dependent on the electrolyte features and influence the reflectance quality of these devices. This quality can be improvement after thermal oxidation or may worsen, depending on the features of the porous structure and on the effect of the oxidation upon the interface roughness. Long oxidation times yield smoother interfaces.
Microlens Array Fabricated by Gray-Scale Lithography Maskless System
Authors: Cirino G. A. , Lopera S. A. , Montagnoli A. N. , Mansano R. D. , Neto L. G.
Published: October 2012

This work presents the fabrication of a high fill factor Fresnel microlens array (MLA) by employing a low-cost home-built maskless exposure lithographic system. A phase relief structure was generated on a photoresist-coated silicon wafer, replicated in Polydimethylsiloxane (PDMS) and electrostatically bonded to a glass substrate. Optical characterization was based on the evaluation of the maximum intensity of each spot generated at the MLA focal plane as well as its full width at half maximum (FWHM) intensity values. The resulting FWHM and maximum intensity spot mean values were 50 ± 8%μm and 0.71 ± 7% a.u , respectively. Such a MLA can be applied as Shack-Hartmann wavefront sensors, in optical interconnects and to enhance the efficiency of detector arrays.
Influence of the Transparent Conductive Oxides on the P-OLEDs Behavior
Authors: Santos E. R. , Correia F. C. , Junior E.C. B. , Onmori R. K. , Fonseca F. J. , de Andrade A. M. , Wang S. H.
Published: October 2012

Multilayer polymer-organic light emitting diodes (P-OLEDs) were assembled with different transparent conductive oxide (TCO) and aluminum as the anode and cathode, respectively. Two types of TCOs, ITO (indium tin oxide) or FTO (fluorine tin oxide), with different sheet resistances, from 10 to 61 Ω/□, were used. A blend of poly[(1,4-phenylene)-alt-2,7(9,9 dioctylfluorene)] and an europium complex (20 %) was used as the polymeric photoactive layer of the devices. The performance of P-OLEDs showed that those having the FTO film with the lowest sheet resistance presented the lowest threshold voltage, while those having the ITO with the lowest sheet resistance presented the highest luminance among all types of devices obtained.
Junctionless Fabrication on SOI Wafers Using Focused Ion Beam Milling and Al Diffusion
Authors: Lima L.P. B. , dos Santos M.V. P. , Cioldin F. H. , Diniz J. A. , Doi I. , Fo J. Godoy
Published: October 2012

pMOS Junctionless (JL) devices were fabricated on Silicon On Insulator (SOI) substrates using gallium (Ga+) Focused Ion Beam (FIB) milling and Al diffusion, to get Si nanowire with p+ doping, respectively. Furthermore, SiO2 and Pt layers were used as gate dielectric and electrodes (gate, drain and source) of Junctionless transistors, respectively, and also were deposited using Ga+ FIB. Width, length and height dimensions of Si nanowire were about 100~300 nm, 4 μm and 200 nm, respectively. Energy Dispersive X-Ray Spectroscopy (EDS) measurements were carried out to confirm the surface composition of Si nanowire, dielectric and electrodes. In addition, from EDS results, Ga incorporation on Si nanowire surface occurred. This incorporation was from Ga+ FIB with no significant damage on Si nanowire. Drain-source current (Id) x drain source voltage (Vds) measurements of JL transistors were carried out, and indicate that the devices are working, like a gated resistor or JL device, with high Pt source and drain contact resistances, which lead to the distortions of Id x Vds curves. However, these distortions can be reduced using a longer time of contact sintering process and a Si nanowire height lower than 50 nm. Finally, our fabrication method using FIB process steps (Si milling, SiO2 and Pt depositions) and Al diffusion can be used to obtain Junctionless devices.
Amorphous Silicon Carbide Thin Films Deposited by Magnetron Co-Sputtering: Effect of Applied Power and Deposition Pressure on Film Characteristics
Authors: Medeiros H. S. , Pessoa R. S. , Maciel H. S. , Massi M. , Tezani L. L. , Leal G. , Galvão N. K. A. M. , da Silva Sobrinho A. S.
Published: October 2012

In this work, the effect of deposition pressure and total power applied to Si and C targets on the a-SiC film characteristics was investigated by profilometry, X-ray diffraction (XRD), Raman spectroscopy, and Rutherford-Backscattering Spectrometry (RBS). Profilometry results indicate an increase in the film thickness by increasing both the deposition pressure and total power. Both Crich and Si-rich a-SiC films were grown only by varying the deposition pressure or total power. Raman spectra suggest that the films contain amorphous phases because a-SiC clusters together with a-Si and a-C clusters were observed. The XRD analysis confirmed the amorphous structure of these films.