## Formal Methods Forum## Spring 2003This 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. For further information, please contact Ilkka Niemelä.
## Program- 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.
[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links] Latest update: 09 January 2005. Ilkka Niemelä |