Open Access. Powered by Scholars. Published by Universities.^{®}
 Keyword

 GRASP (3)
 Applications (2)
 Interactive systems (2)
 General recursion (1)
 Computer vision (1)

 3D graphics (1)
 Loop Mutation (1)
 Convex sets (1)
 Polytopes (1)
 Human body modeling (1)
 Constraint networks (1)
 System FC (1)
 Timevarying images (1)
 Polyhedra (1)
 Type families (1)
 Onebyone (1)
 Mutation Testing (1)
 3D raster graphics (1)
 Combinatorial topology (1)
 Human motion (1)
 Motion (1)
 Termination (1)
 Human figure modeling (1)
 Delaunay triangulations. (1)
 Robotics (1)
 Dependent types; Congruence closure (1)
 Constraint propagation (1)
 Haskell (1)
 Shellings (1)
 Dependent types (1)
Articles 1  30 of 39
FullText Articles in Computer Engineering
Towards OverheadFree Interface Theory For Compositional Hierarchical RealTime Systems, Jin Hyun Kim, Kygong Hoon Kim, Arvind Easwaran, Insup Lee
Towards OverheadFree Interface Theory For Compositional Hierarchical RealTime Systems, Jin Hyun Kim, Kygong Hoon Kim, Arvind Easwaran, Insup Lee
Technical Reports (CIS)
Much recent research has been conducted on compositional realtime scheduling framework as the framework becomes a useful fundamental theory for realtime OSHypervisor. Much recent research has been conducted on compositional realtime scheduling as the framework becomes a useful fundamental theory for realtime OSHypervisor. However, compositional frameworks suffer from abstraction overheads in composing components. In this paper, we classify the composition overheads into i) supply abstraction overhead associated with the supply from a resource provider, and ii) demand abstraction overhead associated with the component workload. Then, we provide sufficient conditions for each abstraction overhead to be eliminated. In addition, this paper ...
Automated Bug Removal For SoftwareDefined Networks, Yang Wu, Andreas Haeberlen, Wenchao Zhou, Boon T. Loo, Ang Chen
Automated Bug Removal For SoftwareDefined Networks, Yang Wu, Andreas Haeberlen, Wenchao Zhou, Boon T. Loo, Ang Chen
Technical Reports (CIS)
When debugging an SDN application, diagnosing the problem is merely the first step: the operator must still find a fix that solves the problem, without causing new problems elsewhere. However, most existing debuggers focus exclusively on diagnosis and offer the network operator little or no help with finding an effective fix. Finding a suitable fix is difficult because the number of candidates can be enormous. In this paper, we propose a step towards automated repair for SDN applications. Our approach consists of two elements. The first is a data structure that we call meta provenance, which can be used to ...
Dstress: Efficient Differentially Private Computations On Distributed Data, Antonis Papadimitriou, Andreas Haeberlen, Arjun Narayan
Dstress: Efficient Differentially Private Computations On Distributed Data, Antonis Papadimitriou, Andreas Haeberlen, Arjun Narayan
Technical Reports (CIS)
In this paper, we present DStress, a system that can efficiently perform computations on graphs that contain confidential data. DStress assumes that the graph is physically distributed across many participants, and that each participant only knows a small subgraph; it protects privacy by enforcing tight, provable limits on how much each participant can learn about the rest of the graph. We also study one concrete instance of this problem: measuring systemic risk in financial networks. Systemic risk is the likelihood of cascading bankruptcies – as, e.g., during the financial crisis of 2008 – and it can be quantified based on the ...
Big Data Analytics Over Encrypted Datasets With Seabed, Antonis Papadimitriou, Ranjita Bhagwan, Nishanth Chandran, Ramachandran Ramjee, Andreas Haberlen, Harmeet Singh, Abhishek Modi, Saikrishna Badrinarayanan
Big Data Analytics Over Encrypted Datasets With Seabed, Antonis Papadimitriou, Ranjita Bhagwan, Nishanth Chandran, Ramachandran Ramjee, Andreas Haberlen, Harmeet Singh, Abhishek Modi, Saikrishna Badrinarayanan
Technical Reports (CIS)
Today, enterprises collect large amounts of data and leverage the cloud to perform analytics over this data. Since the data is often sensitive, enterprises would prefer to keep it confidential and to hide it even from the cloud operator. Systems such as CryptDB and Monomi can accomplish this by operating mostly on encrypted data; however, these systems rely on expensive cryptographic techniques that limit performance in true “big data” scenarios that involve terabytes of data or more. This paper presents Seabed, a system that enables efficient analytics over large encrypted datasets. In contrast to previous systems, which rely on asymmetric ...
Loopy: Programmable And Formally Verified Loop Transformations, Kedar S. Namjoshi, Nimit Singhania
Loopy: Programmable And Formally Verified Loop Transformations, Kedar S. Namjoshi, Nimit Singhania
Technical Reports (CIS)
Abstract. This paper presents a system, Loopy, for programming loop transformations. Manual loop transformation can be tedious and errorprone, while fully automated methods do not guarantee improvements. Loopy takes a middle path: a programmer specifies a loop transformation at a high level, which is then carried out automatically by Loopy, and formally verified to guard against specification and implementation mistakes. Loopy’s notation offers considerable flexibility with assembling transformations, while automation and checking prevent errors. Loopy is implemented for the LLVM framework, building on a polyhedral compilation library. Experiments show substantial improvements over fully automated loop transformations, using simple and ...
Orca: OrderingFree Regions For Consistency And Atomicity, Christian Delozier, Yuanfeng Peng, Ariel Eizenberg, Brandon Lucia, Joe Devietti
Orca: OrderingFree Regions For Consistency And Atomicity, Christian Delozier, Yuanfeng Peng, Ariel Eizenberg, Brandon Lucia, Joe Devietti
Technical Reports (CIS)
Writing correct synchronization is one of the main difficulties of multithreaded programming. Incorrect synchronization causes many subtle concurrency errors such as data races and atomicity violations. Previous work has proposed stronger memory consistency models to rule out certain classes of concurrency bugs. However, these approaches are limited by a program’s original (and possibly incorrect) synchronization. In this work, we provide stronger guarantees than previous memory consistency models by punctuating atomicity only at ordering constructs like barriers, but not at lock operations. We describe the Orderingfree Regions for Consistency and Atomicity (ORCA) system which enforces atomicity at the granularity of ...
An Empirical Study Of OffByOne Loop Mutation, M. S. Raunak, Christian Murphy, Bryan O'Haver
An Empirical Study Of OffByOne Loop Mutation, M. S. Raunak, Christian Murphy, Bryan O'Haver
Technical Reports (CIS)
Context: Developing test cases that are measurably effective in finding faults in programs is a very challenging research problem. Mutation testing, a prominent technique developed to address this challenge, often becomes com putationally too expensive for practical use due to the very large number of mutants that need to be analyzed. Objective: This paper evaluates the impact of Onebyone (OBO) loop mutation in reducing the cost of mutation analysis and investigates this technique's effectiveness in measuring the strength or weakness of test suites. Method: A set of Java and C programs have been used to generate both OBO and ...
Magiccarpet: Verified Detection And Recovery For HardwareBased Exploits, Cynthia Sturton, Matthew Hicks, Samuel T. King, Jonathan M. Smith
Magiccarpet: Verified Detection And Recovery For HardwareBased Exploits, Cynthia Sturton, Matthew Hicks, Samuel T. King, Jonathan M. Smith
Technical Reports (CIS)
Abstract—MAGICCARPET is a new approach to defending systems against exploitable processor bugs. MAGICCARPET uses hardware to detect violations of invariants involving securitycritical processor state and uses firmware to correctly push software’s state past the violations. The invariants are specified at run time. MAGICCARPET focuses on dynamically validating updates to securitycritical processor state. In this work, (1) we generate correctness proofs for both MAGICCARPET hardware and firmware; (2) we prove that processor state and events never violate our security invariants at runtime; and (3) we show that MAGICCARPET copes with hardwarebased exploits discovered postfabrication using a combination of verified ...
Programming Up To Congruence (Extended Version), Vilhelm Sjoberg, Stephanie Weirich
Programming Up To Congruence (Extended Version), Vilhelm Sjoberg, Stephanie Weirich
Technical Reports (CIS)
This paper presents the design of ZOMBIE, a dependentlytyped programming language that uses an adaptation of a congruence closure algorithm for proof and type inference. This algorithm allows the type checker to automatically use equality assumptions from the context when reasoning about equality. Most dependently typed languages automatically use equalities that follow from reduction during type checking; however, such reasoning is incompatible with congruence closure. In contrast, ZOMBIE does not use automatic reduction because types may contain potentially diverging terms. Therefore ZOMBIE provides a unique opportunity to explore an alternative definition of equivalence in dependently typed language design. Our work ...
A Linear/Producer/Consumer Model Of Classical Linear Logic, Jennifer Paykin, Stephan A. Zdancewic
A Linear/Producer/Consumer Model Of Classical Linear Logic, Jennifer Paykin, Stephan A. Zdancewic
Technical Reports (CIS)
This paper defines a new proof and categorytheoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/nonlinear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions that reflect the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into the category theory. The ...
Improving The Estimation Of Word Importance For News MultiDocument Summarization  Extended Technical Report, Kai Hong, Ani Nenkova
Improving The Estimation Of Word Importance For News MultiDocument Summarization  Extended Technical Report, Kai Hong, Ani Nenkova
Technical Reports (CIS)
In this paper, we propose a supervised model for ranking word importance that incorporates a rich set of features. Our model is superior to prior approaches for identifying words used in human summaries. Moreover we show that an extractive summarizer which includes our estimation of word importance results in summaries comparable with the stateoftheart by automatic evaluation.
Maximization Of NonMonotone Submodular Functions, Jennifer Gillenwater
Maximization Of NonMonotone Submodular Functions, Jennifer Gillenwater
Technical Reports (CIS)
A litany of questions from a wide variety of scientific disciplines can be cast as nonmonotone submodular maximization problems. Since this class of problems includes maxcut, it is NPhard. Thus, general purpose algorithms for the class tend to be approximation algorithms. For unconstrained problem instances, one recent innovation in this vein includes an algorithm of Buchbinder et al. (2012) that guarantees a ½  approximation to the maximum. Building on this, for problems subject to cardinality constraints, Buchbinderet al. (2014) o_er guarantees in the range [0:356; ½ + o(1)]. Earlier work has the best approximation factors for more complex constraints ...
Notes On Convex Sets, Polytopes, Polyhedra, Combinatorial Topology, Voronoi Diagrams And Delaunay Triangulations, Jean H. Gallier
Notes On Convex Sets, Polytopes, Polyhedra, Combinatorial Topology, Voronoi Diagrams And Delaunay Triangulations, Jean H. Gallier
Technical Reports (CIS)
Some basic mathematical tools such as convex sets, polytopes and combinatorial topology are used quite heavily in applied fields such as geometric modeling, meshing, computer vision, medical imaging and robotics. This report may be viewed as a tutorial and a set of notes on convex sets, polytopes, polyhedra, combinatorial topology, Voronoi Diagrams and Delaunay Triangulations. It is intended for a broad audience of mathematically inclined readers.
One of my (selfish!) motivations in writing these notes was to understand the concept of shelling and how it is used to prove the famous EulerPoincare formula(Poincare, 1899) and the more recent Upper ...
Closed Type Families With Overlapping Equations (Extended Version), Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich
Closed Type Families With Overlapping Equations (Extended Version), Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich
Technical Reports (CIS)
Open, typelevel functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have nonlinear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.
A Modal Specification Theory For Timing Variability, Andrew King, Oleg Sokolsky, Insup Lee
A Modal Specification Theory For Timing Variability, Andrew King, Oleg Sokolsky, Insup Lee
Technical Reports (CIS)
Modal specifications are classical formalisms that can be used to express the functional variability of systems; it is particularly useful for capturing the stepwise refinement of componentbased design. However, the extension of such formalisms to realtime systems has not received adequate attention. In this paper, we propose a novel notion of timeparametric modal specifications to describe the timing as well as functional variability of realtime systems.We present a specification theory on modal refinement, property preservation and compositional reasoning. We also develop zonegraph based symbolic methods for the reachability analysis and modal refinement checking. We demonstrate the practical application of ...
Clifford Algebras, Clifford Groups, And A Generalization Of The Quaternions: The Pin And Spin Groups, Jean H. Gallier
Clifford Algebras, Clifford Groups, And A Generalization Of The Quaternions: The Pin And Spin Groups, Jean H. Gallier
Technical Reports (CIS)
One of the main goals of these notes is to explain how rotations in Rn are induced by the action of a certain group, Spin(n), on Rn, in a way that generalizes the action of the unit complex numbers, U(1), on R2, and the action of the unit quaternions, SU(2), on R3 (i.e., the action is denied in terms of multiplication in a larger algebra containing both the
group Spin(n) and R(n). The group Spin(n), called a spinor group, is defined as a certain subgroup of units of an algebra, Cln, the Clifford ...
Combining Proofs And Programs In A Dependently Typed Language, Stephanie Weirich, Vilhelm Sjoberg, Chris Casinghino
Combining Proofs And Programs In A Dependently Typed Language, Stephanie Weirich, Vilhelm Sjoberg, Chris Casinghino
Technical Reports (CIS)
Most dependentlytyped programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, mega). Here, we combine these two approaches into a single dependentlytyped core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a callbyvalue programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can ...
Notes On Elementary Spectral Graph Theory Applications To Graph Clustering Using Normalized Cuts, Jean H. Gallier
Notes On Elementary Spectral Graph Theory Applications To Graph Clustering Using Normalized Cuts, Jean H. Gallier
Technical Reports (CIS)
These are notes on the method of normalized graph cuts and its applications to graph clustering. I provide a fairly thorough treatment of this deeply original method due to Shi and Malik, including complete proofs. I include the necessary background on graphs and graph Laplacians. I then explain in detail how the eigenvectors of the graph Laplacian can be used to draw a graph. This is an attractive application of graph Laplacians. The main thrust of this paper is the method of normalized cuts. I give a detailed account for K = 2 clusters, and also for K > 2 clusters, based ...
On The Coordinated Navigation Of Multiple Independent DiskShaped Robots, Cem Serkan Karagöz, H. Isil Bozma, Daniel E. Koditschek
On The Coordinated Navigation Of Multiple Independent DiskShaped Robots, Cem Serkan Karagöz, H. Isil Bozma, Daniel E. Koditschek
Technical Reports (CIS)
This paper addresses the coordinated navigation of multiple independently actuated diskshaped robots  all placed within the same diskshaped workspace. Assuming perfect sensing, shared centralized communications and computation, as well as perfect actuation, we encode complete information about the goal, obstacles and workspace boundary using an artificial potential function over the cross product space of the robots’ simultaneous configurations. The closedloop dynamics governing the motion of each robot take the form of the appropriate projection of the gradient of this function. We show, with some reasonable restrictions on the allowable goal positions, that this function is an essential navigation function  a ...
Bracketing Guidelines For Treebank Ii Style Penn Treebank Project, Ann Bies, Mark Ferguson, Karen Katz, Robert Macintyre
Bracketing Guidelines For Treebank Ii Style Penn Treebank Project, Ann Bies, Mark Ferguson, Karen Katz, Robert Macintyre
Technical Reports (CIS)
No abstract provided.
Modeling And Animating Human Figures In A Cad Environment, Norman I. Badler
Modeling And Animating Human Figures In A Cad Environment, Norman I. Badler
Technical Reports (CIS)
With the widespread acceptance of threedimensional modeling techniques, highspeed hardware, and relatively lowcost computation, modeling and animating one or more human figures for the purposes of design assessment, human factors, task simulation, and human movement understanding has become feasible outside the animation production house environment. This tutorial will address the stateoftheart in human figure geometric modeling, figure positioning, figure animation, and task simulation.
The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom
The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom
Technical Reports (CIS)
We briefly survey the major thrusts of computer graphics activities, examining trends and topics rather than offering a comprehensive survey of all that is happening. The directions of professional activities, hardware, software, and algorithms are outlined. Within hardware we examine workstations, personal graphics systems, high performance systems, and low level VLSI chips; within software, standards and interactive system design; within algorithms, visible surface rendering and shading, threedimensional modeling techniques, and animation.
Note: This paper was presented at Eurographics'84 in Copenhagen, Denmark.
Appendices  Parametric Keyframe Interpolation Incorporating Kinetic Adjustment And Phrasing Control, Scott N. Steketee, Norman I. Badler
Appendices  Parametric Keyframe Interpolation Incorporating Kinetic Adjustment And Phrasing Control, Scott N. Steketee, Norman I. Badler
Technical Reports (CIS)
These are the unpublished appendices for the paper entitled, "Parametric Keyframe Interpolation Incorporating Kinetic Adjustment and Phrasing Control."
Guide: Graphical User Interfaced Development Environment, Tamar E. Granor, Norman I. Badler
Guide: Graphical User Interfaced Development Environment, Tamar E. Granor, Norman I. Badler
Technical Reports (CIS)
GUIDE is an interactive graphical system for designing and generating graphical user interfaces. It provides flexibility to the system designer while minimizing the amount of code which the designer must write. The GUIDE methodology includes the notions of "tool," "task," and "context." GUIDE encourages designers to tailor their systems to individual users by inclusion of "user profiles," allowing different control paths based on the user's characteristics. GUIDE also provides a method for invoking application routines with parameters. Parameters may be based on user inputs and are computed at invocation time. Help messages are created along with the objects to ...
Tempus: A System For The Design And Simulation Of Human Figures In A TaskOriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro Brotman
Tempus: A System For The Design And Simulation Of Human Figures In A TaskOriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro Brotman
Technical Reports (CIS)
A system called TEMPUS is outlined which is being developed to simulate graphically the taskoriented activities of several human agents in a threedimensional environment. TEMPUS is a task simulation facility for the evaluation of complex workstations visavis the normal and emergency procedures they are intended to support and the types and number of individuals who must carry them out. TEMPUS allows a user to interactively:
 Create on or more human figures which are correctly scaled according to a specific population, or which meet certain size constraints.
 View the human figure in any of several graphical modes: stick figure, line or ...
Local Matching Of Surfaces Using Critical Points, Gerald Radack, Norman I. Badler
Local Matching Of Surfaces Using Critical Points, Gerald Radack, Norman I. Badler
Technical Reports (CIS)
The local matching problem on surfaces is: Given a pair of oriented surfaces in 3space, find subsurfaces that are identical or complementary in shape. A heuristic method is presented for local matching that is intended for use on complex curved surfaces (rather than such surfaces as as cubes and cylinders).
The method proceeds as follows: (1) Find a small set of pointscalled "critical points" on the two surfaces with the property that if p is a critical point and p matches q, then q is also a critical point. The critical points are taken to be local extrema of either ...
Generating Shadows With An Umbra And Penumbra, Lynne Shapiro, Norman I. Badler
Generating Shadows With An Umbra And Penumbra, Lynne Shapiro, Norman I. Badler
Technical Reports (CIS)
An algorithm for generating shadows with an umbra and penumbra due to distributed light sources is presented. The method used is based on the inclusion of the shadow volumes in the object data processed by a depthbuffer visible surface computation. The standard depthbuffer data structure is modified to allow the handling of shadows with a depthbuffer hidden surface algorithm. The algorithm involves breaking the light source up into a set of point sources and superimposing the shadows generated by each point source to obtain the final shadow.
The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom
The Computer Graphics Scene In The United States, Norman I. Badler, Ingrid Carlbom
Technical Reports (CIS)
We briefly survey the major thrusts of computer graphics activities, examining trends and topics rather than offering a comprehensive survey of all that is happening. The directions of professional activities, hardware, software, and algorithms are outlined. Within hardware we examine workstations, personal graphics systems, high performance systems, and low level VLSI chips; within software, standards and interactive system design; within algorithms, visible surface rendering and shading, threedimensional modeling techniques, and animation.
Outline Of A Calculus Of Type Subsumption, Hassan AïtKaci
Outline Of A Calculus Of Type Subsumption, Hassan AïtKaci
Technical Reports (CIS)
This paper is a brief analysis of the notion of syntactic representation of types followed by a proposal of a formal calculus of type subsumption. The idea which is developed centers on the concept of indexed term, an extension of the definition of algebraic terms relaxing the fixed arity and fixed indexing constraints, and which allows term symbols to have some preorder structure. It is shown that the structure on the set of symbols can be "homomorphically" extended to indexed terms to what is defined to be a subsumption ordering. Furthermore, when symbols have a lattice structure, this structure extends ...
Tempus: A System For The Design And Simulation Of Human Figures In A TaskOriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro, Carolyn Brown
Tempus: A System For The Design And Simulation Of Human Figures In A TaskOriented Environment, Norman I. Badler, Jonathan Korein, James U. Korein, Gerald M. Radack, Lynne Shapiro, Carolyn Brown
Technical Reports (CIS)
A system called TEMPUS is outlined which is being developed to simulate graphically the taskoriented activities of several human agents in a threedimensional environment. TEMPUS is a task simulation facility for the evaluation of complex workstations visavis the normal and emergency procedures they are intended to support and the types and number of individuals who must carry them out. TEMPUS allows a user to interactively:
* Create one or more human figures which are correctly scaled according to a specific population, or which meet certain size constraints.
* View the human figure in any of several graphical modes: stick figure, line or ...