Faculty Research Publications (Electrical Engineering and Computer Science)This collection includes scholarly articles produced by EECS faculty and students.http://hdl.handle.net/1957/73032014-09-02T21:46:55Z2014-09-02T21:46:55ZCovering Nearly Surface-Embedded Graphs with a Fixed Number of BallsBorradaile, GlencoraChambers, Erin Wolfhttp://hdl.handle.net/1957/517642014-08-29T23:26:00Z2014-06-01T00:00:00ZCovering Nearly Surface-Embedded Graphs with a Fixed Number of Balls
Borradaile, Glencora; Chambers, Erin Wolf
A recent result of Chepoi, Estellon and Vaxes [Disc. Comp. Geom. '07] states that any planar graph
of diameter at most 2R can be covered by a constant number of balls of size R; put another way, there
are a constant-sized subset of vertices within which every other vertex is distance half the diameter.
We generalize this result to graphs embedded on surfaces of fixed genus with a fixed number of apices,
making progress toward the conjecture that graphs excluding a fixed minor can also be covered by a
constant number of balls. To do so, we develop two tools which may be of independent interest. The first
gives a bound on the density of graphs drawn on a surface of genus g having a limit on the number of
pairwise-crossing edges. The second bounds the size of a non-contractible cycle in terms of the Euclidean
norm of the degree sequence of a graph embedded on surface.
This is an author's peer-reviewed final manuscript, as accepted by the publisher. The published article is copyrighted by Springer and can be found at: http://link.springer.com/journal/454.
2014-06-01T00:00:00ZEstablishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, Monitoring and LearningGroce, AlexHavelund, KlausHolzmann, GerardJoshi, RajeevXu, Ru-Ganghttp://hdl.handle.net/1957/514372014-08-14T20:55:32Z2014-04-01T00:00:00ZEstablishing Flight Software Reliability: Testing, Model Checking, Constraint-Solving, Monitoring and Learning
Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang
In this paper we discuss the application of a range of techniques to the
verification of mission-critical flight software at NASA’s Jet Propulsion Laboratory.
For this type of application we want to achieve a higher level of confidence than can
be achieved through standard software testing. Unfortunately, given the current state
of the art, especially when efforts are constrained by the tight deadlines and resource
limitations of a flight project, it is not feasible to produce a rigorous formal proof of
correctness of even a well-specified stand-alone module such as a file system (much less
more tightly coupled or difficult-to-specify modules). This means that we must look for
a practical alternative in the area between traditional testing and proof, as we attempt
to optimize rigor and coverage. The approaches we describe here are based on testing,
model checking, constraint-solving, monitoring, and finite-state machine learning, in
addition to static code analysis. The results we have obtained in the domain of file systems
are encouraging, and suggest that for more complex properties of programs with
complex data structures, it is possibly more beneficial to use constraint solvers to guide
and analyze execution (i.e., as in testing, even if performed by a model checking tool)
than to translate the program and property into a set of constraints, as in abstraction-based
and bounded model checkers. Our experience with non-file-system flight software
modules shows that methods even further removed from traditional static formal methods
can be assisted by formal approaches, yet readily adopted by test engineers and
software developers, even as the key problem shifts from test generation and selection
to test evaluation.
This is an author's peer-reviewed final manuscript, as accepted by the publisher. The published article is copyrighted by Springer and can be found at: http://link.springer.com/journal/10472.
2014-04-01T00:00:00ZSurvey on System I/O Hardware Transactions and Impact on Latency, Throughput, and Other FactorsLarsen, SteenLee, Benhttp://hdl.handle.net/1957/513692014-08-13T00:19:08Z2014-01-01T00:00:00ZSurvey on System I/O Hardware Transactions and Impact on Latency, Throughput, and Other Factors
Larsen, Steen; Lee, Ben
Computer system I/O has evolved with processor and memory technologies in terms of reducing latency, increasing bandwidth and other factors. As requirements increase for I/O, such as networking, storage, and video, descriptor-based DMA transactions have become more important in high performance systems to move data between I/O adapters and system memory buffers. DMA transactions are done with hardware engines below the software protocol abstraction layers in all systems other than rudimentary embedded controllers. CPUs can switch to other tasks by offloading hardware DMA transfers to the I/O adapters. Each I/O interface has one or more separately instantiated descriptor-based DMA engines optimized for a given I/O port. I/O transactions are optimized by accelerator functions to reduce latency, improve throughput and reduce CPU overhead. This chapter surveys the current state of high-performance I/O architecture advances and explores benefits and limitations. With the proliferation of CPU multi-cores within a system, multi-GB/s ports, and on-die integration of system functions, changes beyond the techniques surveyed may be needed for optimal I/O architecture performance.
This is an author's peer-reviewed final manuscript, as accepted by the publisher. The published article/chapter is copyrighted by Elsevier and can be found at: http://www.elsevier.com/books/advances-in-computers/hurson/978-0-12-420232-0.
2014-01-01T00:00:00ZSecure Multiparty Computation between Distrusted Networks TerminalsCheung, S.-C. S.Nguyen, Thinhhttp://hdl.handle.net/1957/511862014-08-07T15:20:27Z2007-12-11T00:00:00ZSecure Multiparty Computation between Distrusted Networks Terminals
Cheung, S.-C. S.; Nguyen, Thinh
One of the most important problems facing any distributed application over a heterogeneous network is the protection of private
sensitive information in local terminals. A subfield of cryptography called secure multiparty computation (SMC) is the study
of such distributed computation protocols that allow distrusted parties to perform joint computation without disclosing private
data. SMC is increasingly used in diverse fields from data mining to computer vision. This paper provides a tutorial on SMC for
nonexperts in cryptography and surveys some of the latest advances in this exciting area including various schemes for reducing
communication and computation complexity of SMC protocols, doubly homomorphic encryption and private information retrieval.
This is the publisher’s final pdf. The published article is copyrighted by the author(s) and published by Springer. The published article can be found at: http://jis.eurasipjournals.com/.
2007-12-11T00:00:00Z