bluuebunny/crossref_metadata_2025 huggingface dataset:
Caisson
Authors: Li Xun , Tiwari Mohit , Oberg Jason K. , Kashyap Vineeth , Chong Frederic T. , Sherwood Timothy , Hardekopf Ben
Published: October 2012

Information flow is an important security property that must be incorporated from the ground up, including at hardware design time, to provide a formal basis for a system's root of trust. We incorporate insights and techniques from designing information-flow secure programming languages to provide a new perspective on designing secure hardware. We describe a new hardware description language, Caisson, that combines domain-specific abstractions common to hardware design with insights from type-based techniques used in secure programming languages. The proper combination of these elements allows for an expressive, provably-secure HDL that operates at a familiar level of abstraction to the target audience of the language, hardware architects.

We have implemented a compiler for Caisson that translates designs into Verilog and then synthesizes the designs using existing tools. As an example of Caisson's usefulness we have addressed an open problem in secure hardware by creating the first-ever provably information-flow secure processor with micro-architectural features including pipelining and cache. We synthesize the secure processor and empirically compare it in terms of chip area, power consumption, and clock frequency with both a standard (insecure) commercial processor and also a processor augmented at the gate level to dynamically track information flow. Our processor is competitive with the insecure processor and significantly better than dynamic tracking.
Understanding POWER multiprocessors
Authors: Sarkar Susmit , Sewell Peter , Alglave Jade , Maranget Luc , Williams Derek
Published: October 2012

Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors.

In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER multiprocessors.

Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.
Partial-coherence abstractions for relaxed memory models
Authors: Kuperstein Michael , Vechev Martin , Yahav Eran
Published: October 2012

We present an approach for automatic verification and fence inference in concurrent programs running under relaxed memory models. Verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, verifying that the program satisfies the specification under a sufficiently relaxed memory model is undecidable. For stronger models, the problem is decidable but has non-primitive recursive complexity.

In this paper, we focus on models that have store-buffer based semantics, e.g., SPARC TSO and PSO. We use abstract interpretation to provide an effective verification procedure for programs running under this type of models. Our main contribution is a family of novel
partial-coherence
abstractions, specialized for relaxed memory models, which partially preserve information required for memory coherence and consistency. We use our abstractions to automatically verify programs under relaxed memory models. In addition, when a program violates its specification but can be fixed by adding fences, our approach can automatically infer a correct fence placement that is optimal under the abstraction. We implemented our approach in a tool called BLENDER and applied it to verify and infer fences in several concurrent algorithms.
Probabilistic, modular and scalable inference of typestate specifications
Authors: Beckman Nels E. , Nori Aditya V.
Published: October 2012

Static analysis tools aim to find bugs in software that correspond to violations of specifications. Unfortunately, for large and complex software, these specifications are usually either unavailable or sophisticated, and hard to write.

This paper presents ANEK, a tool and accompanying methodology for inferring specifications useful for modular typestate checking of programs. In particular, these specifications consist of pre and postconditions along with aliasing annotations known as access permissions. A novel feature of ANEK is that it can generate program specifications even when the code under analysis gives rise to conflicting constraints, a situation that typically occurs when there are bugs. The design of ANEK also makes it easy to add heuristic constraints that encode intuitions gleaned from several years of experience writing such specifications, and this allows it to infer specifications that are better in a subjective sense. The ANEK algorithm is based on a modular analysis that makes it fast and scalable, while producing reliable specifications. All of these features are enabled by its underlying probabilistic analysis that produces specifications that are very
likely
.

Our implementation of ANEK infers access permissions specifications used by the PLURAL [5] modular typestate checker for Java programs. We have run ANEK on a number of Java benchmark programs, including one large open-source program(approximately 38K lines of code), to infer specifications that were then checked using PLURAL. The results for the large benchmark show that ANEK can quickly infer specifications that are both accurate and qualitatively similar to those written by hand, and at 5% of the time taken to manually discover and hand-code the specifications.
Mostly-automated verification of low-level programs in computational separation logic
Authors: Chlipala Adam
Published: October 2012

Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about
first-class code pointers
, which is critical for tasks like certifying implementations of threads and processes. Conversely, verifications that deal with first-class code pointers have featured long, complex, manual proofs. In this paper, we introduce the Bedrock framework, which supports mostly-automated proofs about programs with the full range of features needed to implement, e.g., language runtime systems.

The heart of our approach is in mostly-automated discharge of verification conditions inspired by separation logic. Our take on separation logic is
computational
, in the sense that function specifications are usually written in terms of
reference implementations in a purely functional language
. Logical quantifiers are the most challenging feature for most automated verifiers; by relying on functional programs (written in the expressive language of the Coq proof assistant), we are able to avoid quantifiers almost entirely. This leads to some dramatic improvements compared to both past work in classical verification, which we compare against with implementations of data structures like binary search trees and hash tables; and past work in verified programming with code pointers, which we compare against with examples like function memoization and a cooperative threading library.
LeakChaser
Authors: Xu Guoqing , Bond Michael D. , Qin Feng , Rountev Atanas
Published: October 2012

In large programs written in managed languages such as Java and C#, holding unnecessary references often results in memory leaks and bloat, degrading significantly their run-time performance and scalability. Despite the existence of many leak detectors for such languages, these detectors often target low-level objects; as a result, their reports contain many false warnings and lack sufficient semantic information to help diagnose problems. This paper introduces a specification-based technique called LeakChaser that can not only capture precisely the unnecessary references leading to leaks, but also explain, with high-level semantics, why these references become unnecessary.

At the heart of LeakChaser is a three-tier approach that uses varying levels of abstraction to assist programmers with different skill levels and code familiarity to find leaks. At the highest tier of the approach, the programmer only needs to specify the boundaries of coarse-grained activities, referred to as transactions. The tool automatically infers liveness properties of these transactions, by monitoring the execution, in order to find unnecessary references. Diagnosis at this tier can be performed by any programmer after inspecting the APIs and basic modules of a program, without understanding of the detailed implementation of these APIs. At the middle tier, the programmer can introduce application-specific semantic information by specifying properties for the transactions. At the lowest tier of the approach is a liveness checker that does not rely on higher-level semantic information, but rather allows a programmer to assert lifetime relationships for pairs of objects. This task could only be performed by skillful programmers who have a clear understanding of data structures and algorithms in the program.

We have implemented LeakChaser in Jikes RVM and used it to help us diagnose several real-world leaks. The implementation incurs a reasonable overhead for debugging and tuning. Our case studies indicate that the implementation is powerful in guiding programmers with varying code familiarity to find the root causes of several memory leaks---even someone who had not studied a leaking program can quickly find the cause after using LeakChaser's iterative process that infers and checks properties with different levels of semantic information.
Spreadsheet table transformations from examples
Authors: Harris William R. , Gulwani Sumit
Published: October 2012

Every day, millions of computer end-users need to perform tasks over large, tabular data, yet lack the programming knowledge to do such tasks automatically. In this work, we present an automatic technique that takes from a user an example of how the user needs to transform a table of data, and provides to the user a program that implements the transformation described by the example. In particular, we present a language of programs TableProg that can describe transformations that real users require.We then present an algorithm ProgFromEx that takes an example input and output table, and infers a program in TableProg that implements the transformation described by the example. When the program is applied to the example input, it reproduces the example output. When the program is applied to another, potentially larger, table with a 'similar' layout as the example input table, then the program produces a corresponding table with a layout that is similar to the example output table. A user can apply ProgFromEx interactively, providing multiple small examples to obtain a program that implements the transformation that the user desires. Moreover, ProgFromEx can help identify 'noisy' examples that contain errors.

To evaluate the practicality of TableProg and ProgFromEx, we implemented ProgFromEx as a module for the Microsoft Excel spreadsheet program. We applied the module to automatically implement over 50 table transformations specified by endusers through examples on online Excel help forums. In seconds, ProgFromEx found programs that satisfied the examples and could be applied to larger input tables. This experience demonstrates that TableProg and ProgFromEx can significantly automate the tasks over tabular data that users need to perform.
Cruiser
Authors: Zeng Qiang , Wu Dinghao , Liu Peng
Published: October 2012

Security enforcement inlined into user threads often delays the protected programs; inlined resource reclamation may interrupt program execution and defer resource release. We propose
software cruising
, a novel technique that migrates security enforcement and resource reclamation from user threads to a concurrent monitor thread. The technique leverages the increasingly popular multicore and multiprocessor architectures and uses
lock-free
data structures to achieve
non-blocking
and efficient synchronization between the monitor and user threads. As a case study, software cruising is applied to the heap buffer overflow problem. Previous mitigation and detection techniques for this problem suffer from high performance overhead, legacy code compatibility, semantics loyalty, or tedious manual program transformation. We present a concurrent heap buffer overflow detector, Cruiser, in which a concurrent thread is added to the user program to monitor heap integrity, and custom lock-free data structures and algorithms are designed to achieve high efficiency and scalability. The experiments show that our approach is practical: it imposes an average of 5% performance overhead on SPEC CPU2006, and the throughput slowdown on Apache is negligible on average.
Garbage collection for monitoring parametric properties
Authors: Jin Dongyun , Meredith Patrick O'Neil , Griffith Dennis , Rosu Grigore
Published: October 2012

Parametric properties are behavioral properties over program events that depend on one or more parameters. Parameters are bound to concrete data or objects at runtime, which makes parametric properties particularly suitable for stating multi-object relationships or protocols. Monitoring parametric properties independently of the employed formalism involves
slicing
traces with respect to
parameter instances
and sending these slices to appropriate non-parametric
monitor instances
. The number of such instances is theoretically unbounded and tends to be enormous in practice, to an extent that how to efficiently manage monitor instances has become one of the most challenging problems in runtime verification. The previous formalism-independent approach was only able to do the obvious, namely to garbage collect monitor instances when all bound parameter objects were garbage collected. This led to pathological behaviors where unnecessary monitor instances were kept for the entire length of a program. This paper proposes a new approach to garbage collecting monitor instances. Unnecessary monitor instances are collected lazily to avoid creating undue overhead. This lazy collection, along with some careful engineering, has resulted in RV, the most efficient parametric monitoring system to date. Our evaluation shows that the average overhead of RV in the DaCapo benchmark is 15%, which is two times lower than that of JavaMOP and orders of magnitude lower than that of Tracematches.
kb
-anonymity
Authors: Budi Aditya , Lo David , Jiang Lingxiao , Lucia
Published: October 2012

It is often very expensive and practically infeasible to generate test cases that can exercise all possible program states in a program. This is especially true for a medium or large industrial system. In practice, industrial clients of the system often have a set of input data collected either before the system is built or after the deployment of a previous version of the system. Such data are highly valuable as they represent the operations that matter in a client's daily business and may be used to extensively test the system. However, such data often carries sensitive information and cannot be released to third-party development houses. For example, a healthcare provider may have a set of patient records that are strictly confidential and cannot be used by any third party. Simply masking sensitive values alone may not be sufficient, as the correlation among fields in the data can reveal the masked information. Also, masked data may exhibit different behavior in the system and become less useful than the original data for testing and debugging.

For the purpose of releasing private data for testing and debugging, this paper proposes the
kb
-anonymity model, which combines the
k
-anonymity model commonly used in the data mining and database areas with the concept of program behavior preservation. Like
k
-anonymity,
kb
-anonymity replaces some information in the original data to ensure privacy preservation so that the replaced data can be released to third-party developers. Unlike
k
-anonymity,
kb
-anonymity ensures that the replaced data exhibits the same kind of program behavior exhibited by the original data so that the replaced data may still be useful for the purposes of testing and debugging. We also provide a concrete version of the model under three particular configurations and have successfully applied our prototype implementation to three open source programs, demonstrating the utility and scalability of our prototype.
ALTER
Authors: Udupa Abhishek , Rajan Kaushik , Thies William
Published: October 2012

For decades, compilers have relied on dependence analysis to determine the legality of their transformations. While this conservative approach has enabled many robust optimizations, when it comes to parallelization there are many opportunities that can only be exploited by changing or re-ordering the dependences in the program.

This paper presents Alter: a system for identifying and enforcing parallelism that violates certain dependences while preserving overall program functionality. Based on programmer annotations, Alter exploits new parallelism in loops by reordering iterations or allowing stale reads. Alter can also infer which annotations are likely to benefit the program by using a test-driven framework.

Our evaluation of Alter demonstrates that it uncovers parallelism that is beyond the reach of existing static and dynamic tools. Across a selection of 12 performance-intensive loops, 9 of which have loop-carried dependences, Alter obtains an average speedup of 2.0x on 4 cores.
Path-based inductive synthesis for program inversion
Authors: Srivastava Saurabh , Gulwani Sumit , Chaudhuri Swarat , Foster Jeffrey S.
Published: October 2012

In this paper, we investigate the problem of semi-automated inversion of imperative programs, which has the potential to make it much easier and less error prone to write programs that naturally pair as inverses, such as insert/delete operations, compressors/decompressors, and so on. Viewing inversion as a subproblem of program synthesis, we propose a novel synthesis technique called Path-based inductive synthesis (PINS) and apply it to inversion. PINS starts from a program
P
and a template
T
for its inverse. PINS then iteratively refines the space of template instantiations by exploring paths in the composition of
P
and
T
with symbolic execution. PINS uses an SMT solver to intelligently guide the refinement process, based on the paths explored so far. The key idea motivating this approach is the
small path-bound hypothesis
: that the behavior of a program can be summarized with a small, carefully chosen set of its program paths.

We evaluated PINS by using it to invert 14 programs such as compressors (e.g., Lempel-Ziv-Welch), encoders (e.g., UUEncode), and arithmetic operations (e.g., vector rotation). Most of these examples are difficult or impossible to invert using prior techniques, but PINS was able to invert all of them. We also found that a semi-automated technique we developed to
mine
a template from the program to be inverted worked well. In our experiments, PINS takes between one second to thirty minutes to synthesize inverses. We believe this proof-of-concept implementation demonstrates the viability of the PINS approach to program synthesis.
Directed incremental symbolic execution
Authors: Person Suzette , Yang Guowei , Rungta Neha , Khurshid Sarfraz
Published: October 2012

The last few years have seen a resurgence of interest in the use of symbolic execution -- a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution and other path-sensitive analysis techniques to large systems remains challenging despite recent algorithmic and technological advances. An alternative to solving the problem of scalability is to
reduce
the scope of the analysis. One approach that is widely studied in the context of regression analysis is to analyze the
differences
between two related program versions. While such an approach is intuitive in theory, finding efficient and precise ways to identify program differences, and characterize their effects on how the program executes has proved challenging in practice.

In this paper, we present
Directed Incremental Symbolic Execution
(DiSE), a novel technique for detecting and characterizing the effects of program changes. The novelty of DiSE is to combine the
efficiencies
of static analysis techniques to compute program difference information with the
precision
of symbolic execution to explore program execution paths and generate path conditions affected by the differences. DiSE is a complementary technique to other reduction or bounding techniques developed to improve symbolic execution. Furthermore, DiSE does not require analysis results to be carried forward as the software evolves -- only the source code for two related program versions is required. A case-study of our implementation of DiSE illustrates its effectiveness at detecting and characterizing the effects of program changes.
Mining hot calling contexts in small space
Authors: D'Elia Daniele Cono , Demetrescu Camil , Finocchi Irene
Published: October 2012

Calling context trees (CCTs) associate performance metrics with paths through a program's call graph, providing valuable information for program understanding and performance analysis. Although CCTs are typically much smaller than call trees, in real applications they might easily consist of tens of millions of distinct calling contexts: this sheer size makes them difficult to analyze and might hurt execution times due to poor access locality. For performance analysis, accurately collecting information about hot calling contexts may be more useful than constructing an entire CCT that includes millions of uninteresting paths. As we show for a variety of prominent Linux applications, the distribution of calling context frequencies is typically very skewed. In this paper we show how to exploit this property to reduce the CCT size considerably.

We introduce a novel run-time data structure, called
Hot Calling Context Tree (HCCT)
, that offers an additional intermediate point in the spectrum of data structures for representing interprocedural control flow. The HCCT is a subtree of the CCT that includes only hot nodes and their ancestors. We show how to compute the HCCT without storing the exact frequency of all calling contexts, by using fast and space-efficient algorithms for mining frequent items in data streams. With this approach, we can distinguish between hot and cold contexts on the fly, while obtaining very accurate frequency counts. We show both theoretically and experimentally that the HCCT achieves a similar precision as the CCT in a much smaller space, roughly proportional to the number of distinct hot contexts: this is typically several orders of magnitude smaller than the total number of calling contexts encountered during a program's execution. Our space-efficient approach can be effectively combined with previous context-sensitive profiling techniques, such as sampling and bursting.
Separation logic + superposition calculus = heap theorem prover
Authors: Navarro Pérez Juan Antonio , Rybalchenko Andrey
Published: October 2012

Program analysis and verification tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising foundation for dealing with heap manipulating programs, while the development of practical automated deduction/satisfiability checking tools for separation logic is a challenging problem. In this paper, we present an efficient, sound and complete automated theorem prover for checking validity of entailments between separation logic formulas with list segment predicates. Our theorem prover integrates separation logic inference rules that deal with list segments and a superposition calculus to deal with equality/aliasing between memory locations. The integration follows a modular combination approach that allows one to directly incorporate existing advanced techniques for first-order reasoning with equality, as well as account for additional theories, e.g., linear arithmetic, using extensions of superposition. An experimental evaluation of our entailment prover indicates speedups of several orders of magnitude with respect to the available state-of-the-art tools.
Precise and compact modular procedure summaries for heap manipulating programs
Authors: Dillig Isil , Dillig Thomas , Aiken Alex , Sagiv Mooly
Published: October 2012

We present a strictly bottom-up, summary-based, and precise heap analysis targeted for program verification that performs strong updates to heap locations at call sites. We first present a theory of heap decompositions that forms the basis of our approach; we then describe a full analysis algorithm that is fully symbolic and efficient. We demonstrate the precision and scalability of our approach for verification of real C and C++ programs.
Scaling abstraction refinement via pruning
Authors: Liang Percy , Naik Mayur
Published: October 2012

Many static analyses do not scale as they are made more precise. For example, increasing the amount of context sensitivity in a
k
-limited pointer analysis causes the number of contexts to grow exponentially with
k
. Iterative refinement techniques can mitigate this growth by starting with a coarse abstraction and only refining parts of the abstraction that are deemed relevant with respect to a given client.

In this paper, we introduce a new technique called
pruning
that uses client feedback in a different way. The basic idea is to use coarse abstractions to prune away parts of the program analysis deemed irrelevant for proving a client query, and then using finer abstractions on the sliced program analysis. For a
k
-limited pointer analysis, this approach amounts to adaptively refining and pruning a set of prefix patterns representing the contexts relevant for the client. By pruning, we are able to scale up to much more expensive abstractions than before. We also prove that the pruned analysis is both sound and complete, that is, it yields the same results as an analysis that uses a more expensive abstraction directly without pruning.
Taming wildcards in Java's type system
Authors: Tate Ross , Leung Alan , Lerner Sorin
Published: October 2012

Wildcards have become an important part of Java's type system since their introduction 7 years ago. Yet there are still many open problems with Java's wildcards. For example, there are no known sound and complete algorithms for subtyping (and consequently type checking) Java wildcards, and in fact subtyping is suspected to be undecidable because wildcards are a form of bounded existential types. Furthermore, some Java types with wildcards have no joins, making inference of type arguments for generic methods particularly difficult. Although there has been progress on these fronts, we have identified significant shortcomings of the current state of the art, along with new problems that have not been addressed.

In this paper, we illustrate how these shortcomings reflect the subtle complexity of the problem domain, and then present major improvements to the current algorithms for wildcards by making slight restrictions on the usage of wildcards. Our survey of existing Java programs suggests that realistic code should already satisfy our restrictions without any modifications. We present a simple algorithm for subtyping which is both sound and complete with our restrictions, an algorithm for lazily joining types with wildcards which addresses some of the shortcomings of prior work, and techniques for improving the Java type system as a whole. Lastly, we describe various extensions to wildcards that would be compatible with our algorithms.
Composable asynchronous events
Authors: Ziarek Lukasz , Sivaramakrishnan KC , Jagannathan Suresh
Published: October 2012

Although asynchronous communication is an important feature of many concurrent systems, building
composable
abstractions that leverage asynchrony is challenging. This is because an asynchronous operation necessarily involves two distinct threads of control -- the thread that initiates the operation, and the thread that discharges it. Existing attempts to marry composability with asynchrony either entail sacrificing performance (by limiting the degree of asynchrony permitted), or modularity (by forcing natural abstraction boundaries to be broken).

In this paper, we present the design and rationale for
asynchronous events
, an abstraction that enables composable construction of complex asynchronous protocols without sacrificing the benefits of abstraction or performance. Asynchronous events are realized in the context of Concurrent ML's first-class event abstraction. We discuss the definition of a number of useful asynchronous abstractions that can be built on top of asynchronous events (e.g., composable callbacks) and provide a detailed case study of how asynchronous events can be used to substantially improve the modularity and performance of an I/O-intensive highly concurrent server application.
Reflections on LEEF 2011
Authors: Olbrish Koreen
Published: October 2012

Presented is a recap of LEEF 2011, themed Change the Game: How games, simulations, and virtual worlds change the nature of learning and work. The conference is centered on how learning and entertainment technologies redefine the learning experience.
An alternative visual analysis of the build heap algorithm
Authors: Thompson Hussein , Chadhuri Pranay
Published: October 2012

This article presents an alternative visual analysis of the BUILDHEAP algorithm provided by Goodrich and Tamassia [4]. The analysis is based only on elementary properties of complete binary trees and a simple comparison of the areas of rectangles. As such, it should be accessible to a wide cross-section of students taking a typical algorithm design and analysis course.
Promoting online learning through learners' vision
Authors: Al-Khanjari Z. A. , Kutti N. S. , Dorvlo A. S.S.
Published: October 2012

Rapidly improving services over the internet and increasing availability of web-based education (WBED) products and services encourages the management of the education institutions to decide for any tangible transformation in the existing education paradigm. As learners represent the customers of any education paradigm, it becomes an important issue to understand their vision over the infl uence of technology on the current education environment. Without this knowledge any transformation of the current education paradigm may seem to be possible, but may lead to some unforeseen results. It is foreseen that introduction of a course management tool at Sultan Qaboos University (SQU) would initiate an effective transformation of currently practiced education scheme. This has also created an unavoidable hesitation to carry out a full-scale implementation of e-learning. In order to resolve this problem, we (the researchers at SQU) are encouraged to carry out a full-scale experimental study to identify the visions of learners with respect to the increasing influence of Technology on the current education. This paper presents the results of a survey conducted on the learner community in the Faculty of Science along with a useful discussion and conclusion.
Girls get it
Authors: Mason Raina , Cooper Graham , Comber Tim
Published: October 2012

In this article, we describe high school promotional visits and campus workshops developed to encourage female junior high school students to consider a career in information technology. The students were exposed to programming concepts and activities in a manner that made such content enjoyable and relatively easy to understand and were given pre and post workshop questionnaires. Students perceived programming as simpler and themselves as being more capable after attending these workshops. The article demonstrates the potential for such workshops to address aspects of perceived difficulty and of self-perceptions in ability to master such content.
Gamification: Using Game Mechanics to Enhance eLearning
Authors: Raymer Rick
Published: October 2012

Is gamification just another empty buzzword, or can the principles that game designers employ to engage players really be applied to the design of eLearning software? What exactly is gamification? And, can the theories of gamification be applied to a variety of projects regardless of scope and budget? This article will address specific ways that game mechanics can be applied to your eLearning projects.
Learnstreaming
Authors: Callahan Dennis
Published: October 2012

The Internet has moved from one-way, static pages to two way, real-time streams. One of the easiest ways to evolve with this digital shift is to have a mental model or metaphor that helps you make better sense of this new online world. Learnstreaming is framework for helping you and others make better sense of today's online world.
Computing
Authors: Frailey Dennis J.
Published: October 2012

In recent months, there has been considerable discussion about the value of computing as an academic discipline and the value of computing studies in furthering one's career. Kevin Carey (2010) recently wrote an article showing how a student who took only a few computing courses and then changed majors was able to exploit the knowledge and discipline he learned to solve some serious problems in other domains. Carey's paper focused on the knowledge gained from learning how to program, but what about the other knowledge that is fundamental to our field? Should people outside of computing learn about computing fundamentals because they are as important as, say, basic science or math? This prompted me to examine the role of computing in my own career, and to make some observations on computing jobs in industry and how we might better appreciate and promulgate what we know.
Visual help to learn programming
Authors: Mascarell Jordi Bataller
Published: October 2012

In this article, we describe several types of figures and diagrams to help explaining many fundamental programming concepts to beginners. These concepts include functions, classes, encapsulation public and private access, inheritance, pass by value or by reference, algorithms and method interactions. During our teaching experience since 1995, we have observed recurring problems on understanding the mentioned concepts. Additionally, we have been able to help students to overcome them by following the recipe of "one concept, one drawing".
Reducing the dropout rate in an introductory programming course
Authors: Yadin Aharon
Published: October 2012

This article describes an action research for reducing the high students' dropout rate after an introductory programming course. As part of the action research, that was performed during four semesters several course structures and learning tactics were examined. The success was attributed to three main factors. (1) using Python as the first introductory programming language, which freed the students from detailed language syntax and allowed them to concentrate on algorithms and problem solving; (2) using a visualization environment (Micro-world) for the whole duration of the course, which helped in understanding the more complex and abstract issues; and (3) using individual assignments that enforced better learning habits. The article describes the various attempts, as well as the final structure that reduced the failing students by over 77%.
25 Free Resources for Learning a Language Online
Authors: Hart Jane
Published: October 2012

In Jane Hart's monthly column for eLearn she shares some "gems"—useful or valuable tools, resources, and products she has unearthed for learning and performance improvement/support. In this month's column she focuses on free resources for learning how to speak a foreign language.
Status update
Authors: Snyder Lawrence
Published: October 2012

Many countries are engaged in efforts to revamp their high school computer science curricula. This paper touches briefly on the state of affairs with high school CS in Canada, Israel, India, and New Zealand. Each country has different issues to address in implementing a concepts-rich high school computer science curriculum. The paper then reviews the recent report from the United Kingdom,
Shut Down or Restart? The Way Forward for Computing in the UK Schools
.
SIGCSE spotlight
Authors: White Curt M.
Published: October 2012

Hello, and welcome to
SIGCSE Spotlight
, an ongoing column that highlights and reflects on the current trends within computing education and the SIGCSE community. In this quarter's issue we are going to go behind the scenes at the premier SIGCSE conference -- the SIGCSE Technical Symposium. The Technical Symposium was held from February 29th to March 3rd in Raleigh, North Carolina. While it was reported that 1286 members were in attendance, few, if any, comprehend the amount of work that takes place behind the scenes. To gain a better appreciation, let's take a look at "A Week in the Life of the SIGSCE Technical Symposium".
Book Review: 'Digital Teaching Platforms: Customizing Classroom Learning For Each Student' edited by Chris Dede and John Richards
Authors: Layton-James Laura
Published: October 2012

Chris Dede and John Richards have amassed 20 years of research and development in using digital learning environment, which is shared in their latest book, Digital Teaching Platforms: Customizing Classroom Learning For Each Student. The material is presented in four parts, providing an overview of digital platforms and how they can be used to support individual student learning.
A novel 3D video transcoding scheme for adaptive 3D video transmission to heterogeneous terminals
Authors: Liu Shujie , Chen Chang Wen
Published: October 2012

Three-dimensional video (3DV) is attracting many interests with its enhanced viewing experience and more user driven features. 3DV has several unique characteristics different from 2D video: (1) It has a much larger amount of data captured and compressed, and corresponding video compression techniques can be much more complicated in order to explore data redundancy. This will lead to more constraints on users' network access and computational capability, (2) Most users only need part of the 3DV data at any given time, while the users' requirements exhibit large diversity, (3) Only a limited number of views are captured and transmitted for 3DV. View rendering is thus necessary to generate virtual views based on the received 3DV data. However, many terminal devices do not have the functionality to generate virtual views. To enable 3DV experience for the majority of users with limited capabilities, adaptive 3DV transmission is necessary to extract/generate the required data content and represent it with supported formats and bitrates for heterogeneous terminal devices. 3DV transcoding is an emerging and effective technique to achieve desired adaptive 3DV transmission. In this article, we propose the first efficient 3DV transcoding scheme that can obtain any desired view, either an encoded one or a virtual one, and compress it with more universal H.264/AVC. The key idea of the proposed scheme is to appropriately utilize motion information contained in the bitstream to generate candidate motion information. Original information of both the desired view and reference views are used to obtain this candidate information and a proper motion refinement process is carried out for certain blocks. Simulation results show that, compared to the straightforward cascade algorithm, the proposed scheme is able to output compressed bitstream of the required view with significantly reduced complexity while incurring negligible performance loss. Such a 3DV transcoding can be applied to most gateways that usually have constraints on computational complexity and time delay.
A new methodology to derive objective quality assessment metrics for scalable multiview 3D video coding
Authors: Roodaki Hoda , Hashemi Mahmoud Reza , Shirmohammadi Shervin
Published: October 2012

With the growing demand for 3D video, efforts are underway to incorporate it in the next generation of broadcast and streaming applications and standards. 3D video is currently available in games, entertainment, education, security, and surveillance applications. A typical scenario for multiview 3D consists of several 3D video sequences captured simultaneously from the same scene with the help of multiple cameras from different positions and through different angles. Multiview video coding provides a compact representation of these multiple views by exploiting the large amount of inter-view statistical dependencies. One of the major challenges in this field is how to transmit the large amount of data of a multiview sequence over error prone channels to heterogeneous mobile devices with different bandwidth, resolution, and processing/battery power, while maintaining a high visual quality. Scalable Multiview 3D Video Coding (SMVC) is one of the methods to address this challenge; however, the evaluation of the overall visual quality of the resulting scaled-down video requires a new objective perceptual quality measure specifically designed for scalable multiview 3D video. Although several subjective and objective quality assessment methods have been proposed for multiview 3D sequences, no comparable attempt has been made for quality assessment of scalable multiview 3D video. In this article, we propose a new methodology to build suitable objective quality assessment metrics for different scalable modalities in multiview 3D video. Our proposed methodology considers the importance of each layer and its content as a quality of experience factor in the overall quality. Furthermore, in addition to the quality of each layer, the concept of disparity between layers (inter-layer disparity) and disparity between the units of each layer (intra-layer disparity) is considered as an effective feature to evaluate overall perceived quality more accurately. Simulation results indicate that by using this methodology, more efficient objective quality assessment metrics can be introduced for each multiview 3D video scalable modalities.
Efficient matchings and mobile augmented reality
Authors: Guan Wei , You Suya , Newmann Ulrich
Published: October 2012

With the fast-growing popularity of smart phones in recent years, augmented reality (AR) on mobile devices is gaining more attention and becomes more demanding than ever before. However, the limited processors in mobile devices are not quite promising for AR applications that require real-time processing speed. The challenge exists due to the fact that, while fast features are usually not robust enough in matchings, robust features like SIFT or SURF are not computationally efficient. There is always a tradeoff between robustness and efficiency and it seems that we have to sacrifice one for the other. While this is true for most existing features, researchers have been working on designing new features with both robustness and efficiency. In this article, we are not trying to present a completely new feature. Instead, we propose an efficient matching method for robust features. An adaptive scoring scheme and a more distinctive descriptor are also proposed for performance improvements. Besides, we have developed an outdoor augmented reality system that is based on our proposed methods. The system demonstrates that not only it can achieve robust matchings efficiently, it is also capable to handle large occlusions such as passengers and moving vehicles, which is another challenge for many AR applications.
MOOCs R Us
Authors: Butin Dan W.
Published: October 2012

While MOOCs have much to offer to higher education, Dan W. Butin argues that they can only take us so far. Ultimately, MOOCs provide an apprenticeship into Wikipedia; faculty provide an apprenticeship into democracy.
Product line variability support by FORM and Mecano model integration
Authors: García Francisco José , Barras Juan-Antonio , Laguna Miguel Ángel , Marqués Jos´e Manuel
Published: October 2012

A product line definition must cover several systems, for this reason additional requirements are included as product line assets during domain engineering. Generic assets are presented to cover all components the product line instances are built from, and their corresponding composition rules. These generic assets embrace common and variable product aspects supporting the variability in product line definition and instantiation.This paper is devoted to present the problem of handling product line variability in every life-cycle stage by the integration of the ideas of the domain engineering method FORM (Feature-Oriented Reuse Method) and the Mecano Model, which defines a coarse-grained reusable element structure.
On the use of connector libraries in distributed software architectures
Authors: Kumar M Bharath , Srikant Y. N. , R Lakshminarayanan
Published: October 2012

Recent developments in the field of software architecture have emphasized the concept of first class connectors, which capture the interaction between components. The concept of first class connectors aids the development of distributed software architectures since it can be used to separate concerns of remote interaction between components. A library of prewritten connectors would help prototype, develop, maintain and reconfigure distributed software architectures. Completely automating the usage of connector libraries in distributed software architectures is not trivial since code fragments implementing the connectors have to be partitioned, deployed and instantiated in different machines. In this paper we discuss these issues in connector refinement and instantiation imposed by distributed software architectures and present the construction of a tool that works alongside a connector library to automatically partition, deploy and instantiate architectural entities in various machines. Scalability of the tool to allow for new connector types has been an important issue in its design and function. We also demonstrate the high flexibility and reconfigurability achieved on an interesting application by using a connector library along with our tool.