This is a seminar on formal methods in computer science and engineering
organized by the Laboratory for Theoretical Computer Science at HUT.
We meet usually on Fridays at 2 p.m. in room B353 in the Computer Science
building.
- 16.1.2003 Victor Khomenko ( University of Newcastle upon Tyne,
School of Computing Science):
Detecting State Coding Conflicts in STGs Using SAT
Note: The talk is held on THURSDAY Jan 16 at 10.15 in the TML seminar
room TA346.
Abstract:
The behaviour of asynchronous circuits is often described
by Signal Transition Graphs (STGs), which are Petri nets whose
transitions are interpreted as rising and falling edges of
signals. One of the crucial problems in the synthesis of such
circuits is that of identifying whether an STG satisfies the
Complete State Coding (CSC) requirement, e.g. by using model
checking based on the reachability graph of an STG.
In this paper, we avoid constructing the reachability graph of an
STG, which can lead to state space explosion, and instead use only
the information about causality and structural conflicts between
the events involved in a finite and complete prefix of its
unfolding. The model checking algorithm is derived by adopting the
Boolean Satisfiability (SAT) approach. This technique leads not
only to huge memory savings when compared to methods based on
reachability graphs, but also to significant speedups.
- 14.2.2003 Sakari Seitz:
An Efficient Local Search Algorithm for Random 3-SAT
Abstract:
A stochastic local search algorithm based on the
record-to-record travel (RRT) is applied to the random 3-satisfiability
problem. Experiments on instances with up to one million variables
indicate its time complexity to be almost always linear below the
SAT/UNSAT transition (just like the recent SP algorithm by Zecchina et
al.). How near the transition RRT still finds a satisfying truth
assignment efficiently is dependent on the deviation parameter: to get
closer to the transition point, the deviation must be increased, thereby
slowing down the algorithm. The coefficient of linearity in time
complexity tends to infinity, when approaching the transition.
Other similar (toy) problems are also considered in order to help in
understanding the behaviour of the algorithm.
- 7.3.2003 Petteri Kaski:
Classifying 1-factorizations
Abstract:
A 1-factorization of a graph is a decomposition its edge set into
1-regular spanning subgraphs (1-factors). For example, a 1-factorization
of the complete graph on 2n vertices can be seen as a tournament schedule
for 2n teams, where each team plays exactly once against every other team
during 2n-1 rounds consisting of n games each. Two 1-factorizations are
considered isomorphic if one can be obtained from the other by relabelling
the vertices.
We report work in progress on the problem of generating the nonisomorphic
1-factorizations of a graph. Our approach is to formulate the generation
of 1-factorizations as an exact cover problem, which is then solved using
methods similar to those used in the recent successful classification of
the nonisomorphic Steiner triple systems of order 19.
This is joint work with Patric Östergård.
- 7.3.2003 Harri Haanpää:
Computing Sum Covers and Packings of Small Abelian Groups
Abstract:
A subset S of an Abelian group G is a sum cover, if any element of the group
may be expressed as a sum of two elements of S, and a sum packing, if no
element of the group may be expressed as a sum of two elements of S in more
than one way. Methods for determining a minimum sum cover and a maximum sum
packing of an Abelian group are presented, and distributing the computation
over a network of workstations is discussed.
- 10.3.2003 Satu Virtanen:
Properties of Nonuniform Network Models
Abstract:
Nonuniform random network models aim to capture properties of
natural networks, that is networks constructed from application data. It
is evident that the traditional random graph models do not produce graphs
that resemble application data; a fact already brought up by Erdös and
Renyí in 1960. Recently, two main approaches have been suggested to model
natural networks more accurately: small-world networks that capture the
small average distance and high clustering of e.g. social networks, and
scale-free networks that aim to match the observed degree distribution of
communication networks. In this talk we review the modelling efforts on
natural networks, discussing application examples and properties of some
of the suggested models. In conclusion we summarize our on-going work on
the algoritmic implications of network structure, such as locating
clusters in large graphs.
- 21.3.2003 Markku-Juhani O. Saarinen:
IBM SC, Factoring, and my Experiences with Supercomputing
Abstract:
In this short informal talk, I will discuss the supercomputing
resources which are available to us (after simple application
procedure) from CSC Oy, especially their latest addition, the 512-CPU IBM
eServer Cluster 1600. Writing programs which efficiently utilize these
parallel architectures is not as simple as it sounds, and I'll try to
describe the skills that you must teach yourself to be able to do that.
My implementations of various factoring algorithms (ECM and MPQS) are used
as examples.
In the second part of the talk I will discuss the various uses for
supercomputing in cryptology, especially how it often makes sense to
estimate the security of a cryptographic algorithm in terms
of cost of breaking it, i.e. in "dollars" rather than "bits".
- 28.3.2003 Henrik Petander:
Go-core - Mobility Management in the Next Generation
Internet
Abstract:
GO-Core is a research project at TCS laboratory. It focuses on the
research of mobility of single hosts and entire networks in the IPv6
Internet. The mobile networks can be connected to a mobile
router moving between access points in an infrastructure network or they
can use ad hoc networking for Internet access. The project will produce
a number of mobility management software prototypes based on the MIPL
Mobile IPv6 implementation for Linux. These prototypes will be used for
demonstrating the research results of the project on mobility management
in heterogenous wireless networks.
- 4.4.2003 Janne Lundberg:
Brocom/Multicast - Future Multicast Technology
Abstract: Brocom/Multicast is a research project at the TCS laboratory.
The project is developing new ways of distributing multicast data to
mobile clients that are connected to the Internet using wireless
technologies. The project is designing and implementing a prototype of a
multicast system that can utilize any current or future wireless
technology that can transmit IP packets. The focus of the project is on
developing multicast caching and on the efficient use of the air
interface.
- 9.5.2003 Satu Virtanen:
Online Methods for Clustering the Web Graph
Abstract:
We examine clustering of massive graphs based on local information and
stochastic search. Clustering is the process of identifying semantic
entities from large data sets. In the Web graph, a cluster can be
characterized as a subgraph of webpages or websites that are highly
interconnected and hence are likely to be semantically related in their
content. Traditional clustering methods for graphs require as input the
full adjacency relation and produce a clustering for all vertices of the
graph simultaneously. For many applications, it would suffice to locate
the cluster of a given vertex. Hence local search methods are of interest.
We define a cluster fitness measure for optimization with a local search
method, such as simulated annealing. This measure favors clusters that
have several edges between the included vertices and only a few edges
pointing outside the cluster. We have conducted experiments on several
offline datasets and are currently testing a Web crawler to identify
clusters from the World Wide Web. Determining properties of the clusters
in a graph may help to characterize natural graphs and to evaluate how
well existing generation models match the properties of e.g. the Web
graph.
- 27.5.2003 Peeter Laud (University of Tartu):
Confidentiality Analysis Correct wrt. Computational Semantics.
(Slides [PDF])
NOTE: The talk is held at 14.15-16.00 in room A328.
Abstract:
Suppose that the inputs and outputs of a program are divided to different
security classes. In this case we want to be sure that the public outputs of
the program contain no information about its private inputs --- we want the
program to have secure information flow. We have to analyse the program text
to determine whether the program has such property; secure information flow
is in general not testable. There exist wholly automatic program analyses
for secure information flow. These analyses are allowed to "err to the safe
side" --- they are allowed to tag some secure programs as insecure. However,
if the analysis finds a program to be secure then it really must be secure.
The analyses must be allowed to err sometimes, because secure information
flow is undecidable.
Usual definitions of secure information flow have information-theoretic
nature. An analysis correct with
respect to such definition may only deem such programs secure, whose public
outputs and private inputs are statistically independent. The inputs and
outputs of a cryptographic primitive (for example, symmetric encryption) are
not statistically independent. However, we still consider them secure and
according to certain definitions, they indeed are. To handle symmetric
encryption in analyses for secure information flow, we first propose a new
definition for it, requiring only computational independence of the
program's private inputs and public outputs. We then give a program analysis
correct with respect to this definition and capturing the intuitive meaning
of security of symmetric encryption.
Similar question arises when a cryptographic protocol is employed to
transfer some secret data from one party to another. We would like to make
sure that no attacker can learn anything about the secret message. There
exist analyses for this task. These analyses are correct with respect to the
semantics of protocols and security definition based on term algebras ---
they are correct in the so-called Dolev-Yao model. Unfortunately, this model
is not a faithful abstraction of reality and we cannot deduce the security
of the real protocol from the absence of attacks in the Dolev-Yao model.
We propose a confidentiality definition similar to the definition of
computationally secure information flow. We state that a message is secret
if it is computationally independent from the attackers "experience" while
running in parallel with the protocol. We then present a simple analysis for
analysing protocols correct with respect to that security definition.
- 13.6.2003 Tuomo Pyhälä:
Specification Coverage Aided Test Selection
Abstract:
In this paper test selection strategies in formal
conformance testing are considered. As the testing
conformance relation we use the ioco relation,
and extend the previously presented on-the-fly test
generation algorithms for ioco to include test selection
heuristic based on a specification coverage metric.
The proposed method combines a greedy test selection
with randomization to guarantee completeness.
As a novel implementation technique we employ bounded
model checking for lookahead in greedy test selection.
- 27.6.2003 Toni Jussila:
BMC via On-the-Fly Determinization
Abstract: The paper develops novel bounded model checking techniques for
labelled transition systems. The aim is to increase the efficiency of
BMC by exploiting the inherent concurrency in the product of LTSs in
order to cover more executions of the product within a given bound. This
is done by considering a non-standard execution model, step executions,
where multiple actions can take place simultaneously and where component
LTSs are determinized on-the-fly, i.e., a component may be in a set of
states in a step instead of in just one as in standard interleaving
executions. Step executions can be further restricted to a subclass
called process executions without loosing reachable states. For bounded
model checking of reachability properties of the product of LTSs the
paper presents translation schemes from LTSs to a constrained Boolean
circuit such that satisfying valuations of the circuit correspond to
step (process) executions of the product. The translation schemes have
been implemented and some experimental comparisons performed. The
results show that the bound needed for step and process executions is in
most cases lower than in interleaving executions and that the running
time of the model checker using process executions is smaller than using
steps. Moreover, the performance compares favorably to a
state-of-the-art interleaving BMC implementation in the NuSMV system.
