- talks - lists.cs.princeton.edu

Colloquium Speaker, Dec. 16, 2009- David Naumann
by Nicole E. Wagenblast 14 Dec '09

14 Dec '09

Smart Assertions for Dumb Provers David Naumann, Stevens Institute of Technology 4:30 PM Small Auditorium CS 105 Assertions are widely used for runtime checking of software correctness, and increasingly used for compile time checking of simple properties like array index bounds. Structural integrity of pointer based data structures and design patterns often involves recursively defined properties which are costly to check at runtime and which appear to be unsuited to static checking using fully automated theorem provers. Remarkably, judicious use of ghost state lets programmers express recursive properties in pure first order logic and successfully use fast provers based on SAT solving. In this talk I will introduce the technique in elementary terms, for programmers, who may find it immediately useful in testing. I will also outline research questions about how to use the technique in frame conditions, in refactoring, in foundational proofs, in refinement types, in terms of aspects, and in checking information flow properties.

1 1

Colloquium Speaker, Dec. 9, 2009- Marc Fiuczynski
by Nicole E. Wagenblast 07 Dec '09

07 Dec '09

PlanetLab: From Testbed to Service Deployment Platform Marc Fiuczynski, Princeton Computer Science 4:30 PM Small Auditorium CS 105 Abstract: PlanetLab was originally designed to be a realistic testbed for networking and distributed systems research. It has served that role quite well. More recently, however, it has also become a practical platform for rapidly deploying (and then effectively managing) network services that have value to a wide-range of user communities (and a diverse set of network environments). This talk describes three such deployments: (1) providing web connectivity to remote villages and schools; (2) capturing gold-standard measurements of broadband connectivity in the US; and (3) supporting high-speed content distribution in a Telco access network.

1 0

Colloquium Speaker, Dec. 9, 2009- Marc Fiuczynski
by Michele J. Brown 03 Dec '09

03 Dec '09

PlanetLab: From Testbed to Service Deployment Platform Marc Fiuczynski, Princeton Computer Science 4:30 PM Small Auditorium CS 105 Abstract: PlanetLab was originally designed to be a realistic testbed for networking and distributed systems research. It has served that role quite well. More recently, however, it has also become a practical platform for rapidly deploying (and then effectively managing) network services that have value to a wide-range of user communities (and a diverse set of network environments). This talk describes three such deployments: (1) providing web connectivity to remote villages and schools; (2) capturing gold-standard measurements of broadband connectivity in the US; and (3) supporting high-speed content distribution in a Telco access network.

1 0

S Nikolova preFPO
by Melissa Lawson 24 Nov '09

24 Nov '09

Sonya Nikolova will present her preFPO on Wednesday December 2 at 10AM in Room 402. The members of her committee are: Perry Cook, advisor; Marilyn Tremaine (Rutgers) and Christiane Fellbaum, readers; Adam Finkelstein and Szymon Rusinkiewicz, nonreaders. Everyone is invited to attend her talk. Her abstract follows below. ***** Title and Abstract: Improving Vocabulary Organization in Assistive Communication Tools: A Mixed-Initiative Approach Navigating a vocabulary consisting of thousands of entries in order to select appropriate words for building communication is challenging for individuals with lexical access disorders like those caused by aphasia, a cognitive disorder. Most existing assistive communication vocabularies have a lexical organization scheme based on a simple list of words. Some word collections are organized in hierarchies which often leads to deep and confusing searches; others are simply a list of arbitrary categories which causes excessive scrolling and a sense of disorganization. Ineffective vocabulary organization and navigation hurt the usability and adoption of assistive communication tools and ultimately fail to help users engage in practical communication. We have developed a multi-modal visual vocabulary that enables improved navigation and effective word finding by modeling a speaker's "mental lexicon", where words are stored and organized in ways that allow efficient access and retrieval. Due to impaired links in their mental lexicon, people with aphasia have persistent difficulties accessing and retrieving words that express intended concepts. The Visual Vocabulary for Aphasia (ViVA) attempts to compensate for some of these missing or impaired semantic connections by organizing words in a dynamic semantic network where links between words reflect semantic association measures based on WordNet, human judgments of semantic similarity, and past vocabulary usage. ViVA is both adaptable, able to be customized by the user, and adaptive, able to dynamically change to better suit users' past actions and future needs. This mixed-initiative approach enables the user to feel in control by making changes and anticipating ones that have been initiated by the system while still allowing adaptive methods to help determine where and when changes are required. ViVA's adaptable component allows the user to add and remove vocabulary items, and group them in personalized categories. The adaptive component updates the semantic network according to vocabulary usage, user preferences, and a number of semantic association measures. Thus, ViVA tailors the vocabulary organization according to both user-specific information and general knowledge of human semantic memory. We report results from two studies evaluating how ViVA compares to a vocabulary access system in which words are organized hierarchically into common categories. Since our target user population is people with cognitive impairments, further work involves studying the effect of adaptation on users' cognitive load and investigating the tradeoff between improved navigation and changing vocabulary structure due to adaptation.

1 0

Thursday Lunch Talk: The economics of virtualization [Nov 19]
by jensg＠princeton.edu 18 Nov '09

18 Nov '09

Tomorrow, Paul Laskowski (UC Berkeley) is presenting his work on the economics of network innovation and virtualization. I have attached the announcement below. Please join us for the talk at CITP. If you are interested in meeting with him please let me know your availability. Paul is at CITP from Wednesday - Friday. Jens Grossklags (Postdoctoral Research Associate, CITP) ------------------- Paul Laskowski - The Economics of Virtualization Date: Thursday, November 19, 2009 Time: 12:30 -1:30 pm Location: 306 Sherrerd Hall Food at 12:30 pm. Discussion begins at 12:45 pm. Everyone invited. The difficulty of making changes to the internet architecture has spawned widespread interest in large-scale, “virtualized” testbeds as a place to deploy new services. Despite the excitement, uncertainty surrounds the question of how technologies can bridge the gap from testbed to global availability. It is recognized that no amount of validation will spur today’s ISPs to make architectural changes, so if new services are to reach a widespread audience, the testbed itself must provide that reach. This suggests two questions: First, would today’s network providers (or a new set of providers) ever support a virtualized architecture on a global scale? Second, even if they did, would such a network, spanning a great many domains, support the adoption of new services or upgrades to the infrastructure? In this talk, I will argue that the answers to these questions depend critically on how money flows to network and service providers. A novel economic theory, rooted in the classic model of Cournot competition, allows us to compare market types with regard to service innovation and network upgrade. According to this analysis, there is a danger that a virtualized testbed inherits the market structure prevalent in the internet architecture, causing investment levels to remain poor. On the other hand, alternate market designs can dramatically improve incentives to invest in services, and even in network upgrades, but may encounter resistance from network providers who are likely to see reduced profits. I will discuss how these alternate market types may be implemented.))

1 0

Today's Colloquium Cancelled
by Andrew W. Appel 18 Nov '09

18 Nov '09

Today's colloquium is cancelled. David Naumann cannot speak due to an illness.

1 0

David Naumann--Colloquium Speaker, Wednesday, October 18, 2009
by Michele J. Brown 16 Nov '09

16 Nov '09

Title: Smart Assertions for Dumb Provers David Naumann, Stevens Institute of Technology 4:30PM- Small Auditorium CS105 Host: Andrew Appel Assertions are widely used for runtime checking of software correctness, and increasingly used for compile time checking of simple properties like array index bounds. Structural integrity of pointer based data structures and design patterns often involves recursively defined properties which are costly to check at runtime and which appear to be unsuited to static checking using fully automated theorem provers. Remarkably, judicious use of ghost state lets programmers express recursive properties in pure first order logic and successfully use fast provers based on SAT solving. In this talk I will introduce the technique in elementary terms, for programmers, who may find it immediately useful in testing. I will also outline research questions about how to use the technique in frame conditions, in refactoring, in foundational proofs, in refinement types, in terms of aspects, and in checking information flow properties. Joint work with Anindya Banerjee, Mike Barnett, and Stan Rosenberg

1 0

Colloquium Speaker, Wednesday, November 18, 2009- David Naumann
by Michele J. Brown 13 Nov '09

13 Nov '09

Title: Smart Assertions for Dumb Provers David Naumann, Stevens Institute of Technology 4:30PM- Small Auditorium CS105 Host: Andrew Appel Assertions are widely used for runtime checking of software correctness, and increasingly used for compile time checking of simple properties like array index bounds. For pointer based data structures and design patterns, structural integrity conditions often involve recursively defined properties which are costly to check at runtime and which appear to be unsuited to static checking using fully automated theorem provers. Remarkably, judicious use of ghost state lets programmers express recursive properties in pure first order logic, thereby enabling the use of fast provers based on SAT solving. In this talk I will introduce the technique and pose research questions about how to use the technique in frame conditions, in foundational proofs, in refinement types for higher order programs, in terms of aspects, and in checking information flow properties. Joint work with Anindya Banerjee, Mike Barnett, and Stan Rosenberg

1 0

Fwd: [ens] talk about blackhole identification by Italo Cunha, Nov 11 11am, CS 302
by Yaping Zhu 09 Nov '09

09 Nov '09

Begin forwarded message: > From: Yaping Zhu <yapingz(a)CS.Princeton.EDU> > Date: October 7, 2009 6:55:55 PM PDT > To: ens(a)lists.cs.princeton.edu > Subject: [ens] talk about blackhole identification by Italo Cunha, > Nov 11 11am, CS 302 > > hi all, > Italo Cunha from UPMC Paris Universitas is visiting Princeton on Nov > 11. He will be giving a talk at 11am in CS 302 (title and abstract > below). please let me know if you'd like to meet with him in person. > > thanks, > Yaping > > Title: Measurement Methods for Fast and Accurate Blackhole > Identification with Binary Tomography > > Abstract: Binary tomography--the process of identifying faulty network > links through coordinated end-to-end probes--is a promising method for > detecting failures that the network does not automatically mask (e.g., > network "blackholes"). Because tomography is sensitive to the > quality of > the input, however, naive end-to-end measurements can introduce > inaccuracies. This paper develops two methods for generating inputs to > binary tomography algorithms that improve their inference speed and > accuracy. Failure confirmation is a per-path probing technique to > distinguish packet losses caused by congestion from persistent link or > node failures. Aggregation strategies combine path measurements from > unsynchronized monitors into a set of consistent observations. When > used > in conjunction with existing binary tomography algorithms, our methods > identify all failures that are longer than two measurement cycles, > while > inducing relatively few false alarms. In two wide-area networks, our > techniques decrease the number of alarms by as much as two orders of > magnitude. Compared to the state of the art in binary tomography, our > techniques increase the identification rate and avoid hundreds of > false > alarms. > > Bio: Ítalo Cunha received the B.Sc. degree in computer science and the > M.Sc. degree in computer science from Universidade Federal de Minas > Gerais, Brazil, in 2004 and 2007, respectively. He is currently a > second > year Ph.D. candidate in UPMC Paris Universitas, doing his research > with > Thomson, Paris, France. His research interests are in network > measurement, troubleshooting, and management. > _______________________________________________ > ens mailing list > ens(a)lists.cs.princeton.edu > https://lists.cs.princeton.edu/mailman/listinfo/ens

1 0

Colloquium Speaker, Wed. Nov. 11, 2009- Andrew Bavier
by Michele J. Brown 09 Nov '09

09 Nov '09

Title: Establishing Resource Allocation Policies in the PlanetLab Federation Andrew Bavier, Princeton University, Computer Science Department Wednesday, Nov 11, 2009 4:30PM Small Auditorium, CS 105 Over time PlanetLab has evolved from a centrally-administered testbed to a federation of regional testbeds that are operated independently. The PlanetLab software is also freely available, which has allowed many organizations to bring up their own "private" PlanetLabs. For most private PlanetLabs, a barrier to entering the federation is the inability to express access and allocation policies for their own resources, and the lack of tools to communicate, analyze, and enforce those policies. In the first part of my talk, I will present an overview of the PlanetLab federation. Next I will focus on VINI, a private PlanetLab we have deployed in Internet2 and NLR, and which is intended for evaluating new network architectures. Finally, I will describe a tool ("sfatables") we have built for expressing and enforcing resource allocation policies. Our approach was designed to enable VINI to federate with PlanetLab, but it is general enough to accommodate a diverse collection of computing facilities. This talk describes joint work with Larry Peterson, Sapan Bhatia, Jennifer Rexford, and Nick Feamster.

1 0