Pizza, Puzzle and Presentation Lunch (P-cubed L)
(former Brown Bag Lecture Series)
For more information on P-cubed L Series, please, contact Nadya Kuzmina.
Fall 2006
|
Thursday, September 14, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Joe Pohl
|
|
"Constructive Membership Predicates as Index Types"
|
|
Summary:
In the constructive setting, membership predicates over recursive types
are inhabited by terms indexing the elements that satisfy the criteria for
membership. In this paper, we motivate and explore this idea in the
concrete setting of lists and trees. We show that the inhabitants of
membership predicates are precisely the inhabitants of a generic shape
type. We show that membership of $x$ (of type $T$) in structure $S$,
$(x\in_T{}S)$ can not, in general, index all parts of a structure $S$ and
we generalize to a form $\rho\in{}S$ where $\rho$ is a predicate over $S$.
Under this scheme, $(\lambda{}x.True)\in{}S$ is the set of all indexes
into $S$, but we show that not all subsets of indexes are expressible by
strictly local predicates. Accordingly, we extend our membership
predicates to predicates that retain state ``from above'' as well as allow
``looking below''. Predicates of this form are complete in the sense that
they can express every subset of indexes in $S$. These ideas are
motivated by experience programming in Nuprl's constructive type theory
and the theorems for lists and trees have been formalized and mechanically
checked.
|
|
Download:
|
TUESDAY, September 26, 12:20 - 1:15 pm
(please, note the change of day to TUESDAY for just this week)
|
|
|
EN, 4066
|
|
Paul Maxim
|
|
"Where are You?"
|
|
Summary:
The ability of robots to quickly and accurately localize
their neighbors is extremely important in swarm robotics. Prior
approaches generally rely either on global information provided by
GPS, beacons, and landmarks, or complex local information provided by
vision systems. In this paper we provide a new technique, based on
trilateration. This system is fully distributed, inexpensive,
scalable, and robust. In addition, the system provides a unified
framework that merges localization with information exchange between
robots. The usefulness of this framework is illustrated on a number of
applications.
|
|
Download:
|
|
Thursday, October 12, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
To be Added.
|
|
To be Added.
|
|
Summary:
|
|
Download:
|
|
Thursday, October 26, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Miranda Bryant
|
|
To be Added.
|
|
Summary:
|
|
Download:
|
|
Thursday, November 9, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
To be Added.
|
|
To be Added.
|
|
Summary:
|
|
Download:
|
|
Thursday, November 23, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
To be Added.
|
|
To be Added.
|
|
Summary:
|
|
Download:
|
|
Thursday, December 7, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
To be Added.
|
|
To be Added.
|
|
Summary:
|
|
Download:
|
Spring 2006
|
Thursday, March 30, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Ryan Harkins
|
|
"Resource-Bounded Measure in Double Exponential Time"
|
|
Summary:
Since the inception of resource-bounded measure for computational complexity by Lutz in 1990,
research has investigated the measure of classes within E, EXP, ESPACE, EXPSPACE, and even
within P and PSPACE. But very little has been examined at the double-exponential time setting
or any other higher class. We build upon the tools for resource-bounded measure to explore
measure in classes of higher time complexity. We extend previous results for martingales into
this higher setting and observe several conclusions. The first is that measure separation
propagates upwards, in that if the measure of NP is not 0, then the measure of NE is not 0,
whereas class inequality was known to propagate downwards. We also strengthen some recent
results and prove measure equivalence of some randomized classes.
|
|
Download: PDF
|
|
Thursday, April 13, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Christer Karlsson
|
|
Network Intrusion Detection: an Attempt to Use Multiple Anomaly Detectors to Classify Cyber-attacks.
|
|
Summary:
Network Intrusion Detection Systems (NIDS) is an area of research that
has been active for some time with well-developed technologies. The
intrusion detection techniques can be classified into two approaches:
misuse detection and anomaly detection. The misuse detection systems
rely upon signatures of known attacks or pre-defined rules to match
and identify known attacks. The anomaly detection system usually
establishes the normal usage profile of a system that is a model of
the expected observable behavior and any large deviation will be
identified as a possible attack. We present a novel approach that
tries to bridge the gap between the two systems. The creation of an
ensemble of classifiers reveals more information about the class of an
attack thus it far surpasses the ability of any single classifier.
|
|
Thursday, April 27, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Lucas Shaw
|
|
Vaccination Strategies for Virus Spread via Air Travel.
|
|
Flu vaccine shortage worries and fear of a global flu pandemic have
been common stories in the mass media. Effective use of existing
vaccine supplies is important for preventing an epidemic of a virus.
Work on modeling the spread of a virus via air travel between the 12
cities with the busiest airports is examined. Differential equations
are used to model the spread of the virus within each city while a
Markov chain models approximately 2,000 daily airplane flights between
the cities, whose total population is approximately 55,000,000 people.
Given various supplies of vaccine, an Evolutionary Algorithm (EA)
develops optimal vaccination allocation policies. These policies are
significantly more effective than benchmark vaccine policies. Analysis
of the differential equations and Markov chain reveals important
elements of the EA's policies, yielding an explanation of the EA's
policies in simple terms. From this analysis we extract more
meaningful vaccination policies. There is some evidence that, with
parameters roughly describing the flu virus, the model is predictive
in comparing the results with the spread of flu at the end of 2005.
The framework used is fully generalizable to modeling the spread of
many harmful substances in a loosely connected set of populations,
including the spread of computer viruses and animal pathogens.
|
Fall 2005
|
Thursday, October 6, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Joe Pohl
|
|
"I don't think I will ever see a program as lovely as a tree: Formalizing
trees and recursive types. "
|
|
Summary:
By introducing some of the basic constructs of type theory, we
formalize some basic notions of tree as types. We will then use these
trees to show how formal methods and mathematics can play a role in
development of specifications for correct by construction software and in
algorithms. We finish with some constructions dealing with the equality of
tree types and describe decidable types and what can still be obtained if
our underlying type is not necessarily decidable.
|
|
Thursday, October 20, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Nadya Kuzmina
|
|
Recovering specifications from programs: a dynamic approach.
|
|
Summary:
A constraint is a restriction on one or more values of (part of) an object-oriented model or system. Constraints on visual models provide for better documentation, improved precision and communication without misunderstanding. Constraints inserted into program code are helpful in understanding the underlying program logic. Constraints must be preserved when code is modified, thus aiding in program evolution and revealing hidden erroneous behaviour. However, more often than not developers are in too much of a hurry to write constraints. Invariant detection offers a solution to this problem by recovering constraints at certain program points. Daikon is a fully automated implementation of a dynamic invariant detector, which is capable of inferring many kinds of invariants. I am looking into inferring object-oriented OCL constraints for Java programs dynamically to help developers annotate their visual models and code with (editable) constraints.
|
|
Download: Open Office Presentation | PDF
|
|
Thursday, November 3, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
John Paul
|
|
A Formal Approach for Debugging and Vulnerability Analysis in
Web Applications.
|
Summary: A web application is a suite of software programs that run on a web
server and interact across a network with a remote user's web browser
to provide services to the user. A typical service provided by many
web applications is remote user access to information stored in an
organization's databases. Web applications are complex and error-prone
to develop and to maintain, and because of their high visibility it is
especially important to discover early any programming bugs.
This lecture introduces a research project that seeks to apply formal
methods to the task of automatically checking source code
representations of web applications for programming bugs. The talk
will explain a general formalism for modeling a web application as a
finite transition system and the applicability of model checking to
the debugging task.
|
|
Download: PDF
|
|
Thursday, November 17, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Suranga Hettiarachchi
|
|
Swarm Formations for Obstacle Avoidance.
|
|
Summary: This lecture presents a novel extension to our artificial physics
framework, with the use of a generalized Lennard-Jones force law. We
utilized evolutionary algorithms to optimize the parameters of the force
laws. These force laws were tested within the context of moving robotic
swarm formations through obstacle fields to a goal.
In addition, we present novel metrics of performance, namely, the number
of robots that collide with obstacles, their connectivity, the number of
robots that reach the goal, and the time to the goal.
We conclude with comparative results of our force laws using the
performance criteria.
|
|
Thursday, December 1, 12:20 - 1:15 pm
|
|
|
EN, 4066
|
|
Jinwook Shin
|
|
The Basic Building Blocks of Attacks.
|
|
Summary: This lecture introduces a basic building block discovery algorithm in
computer security attacks. By "basic building blocks" we mean the
essential elements common to all attack programs in a certain class.
To identify the basic building blocks, we first formalize and build
attack models from a variety of attack programs. These models take
form of finite-state transducers (FSTs). Then, we do induction over
the models to extract the basic building blocks of attacks.
|
