SRM seminar

Abstracts 2016

Speaker: Katia Santaca
Title: A Topological Categorization of Agents for the Definition of Attack States in Multi-Agent Systems
Abstract: In this work, I propose a topological categorization of agents that makes use of the multiple-channel logic (MCL) framework, a recently developed model of reasoning about agents. I introduce a complete formalization of prejudices on agents’ attitudes and propose an extension of the rules of the MCL framework. I then use RCC-5 (the Region Connection Calculus) to categorize different agents in Multi-Agent Systems (MAS) based on the collaboration, competence, and honesty of agents. I discuss the possibility of using RCC-3 and RCC-8 and generalize my results to define an upper-bound in the number of different types of agents in MAS. Finally, I apply my topological categorization to a specific MAS that describes a Cyber-Physical System, for which I define, categorize and discuss the resulting attack states.

Speaker: Chiu Kai Wu
Title: Summary on the work on boolean network and controllability
Abstract: A non-standard variant of pertubation strategy is applied on Boolean Network (both synchronous and asynchronous mode). The corresponding results may help one to understand more features about attractors on Boolean Network, especially the asynchronous one. Finally, some work on controllability on boolean network will be discussed.

Speaker: Yu Li
Title: Mathematical Modeling of Network Traffic
Abstract: Increasing access to the Internet is producing profound influence around the World. More and more people are taking advantage of the Internet to obtain information, communicate with each other far away and enjoy various recreations. This largely increased demand for the Internet requires better and more effective models. During the 1990s, a number of studies show that due to a different nature from telephonic traffic, in particular a bursty nature, traditional queuing models are not applicable in modeling of modern traffic. This work presents some alternative rigorous models that can be used in studying the behavior of the Internet traffic.

Speaker: Mathias Humbert
Title: New Challenges in Health Data Privacy: The Case of MicroRNA Expressions
Abstract: The rapidly decreasing cost of molecular profiling tests, such as DNA sequencing, and the consequent increasing availability of biological data are revolutionizing medicine, but at the same time create novel privacy risks. The research community has already proposed a plethora of methods for protecting genomic data against these risks. However, the privacy risks stemming from epigenetics, which bridges the gap between the genome and our health characteristics, have been largely overlooked so far, even though epigenetic data is no less privacy sensitive. In this talk, I will first provide some background on health data. I will then show how personal microRNA expression profiles, despite their variability, can be successfully tracked over time. I will also present two mechanisms for mitigating the linkability threat: (i) hiding a subset of disease-irrelevant miRNA expressions, and (ii) probabilistically sanitizing the miRNA expression profiles. Furthermore, I will show how, by knowing the actual microRNA expressions of a victim, one can infer that she is a member of a given microRNA dataset by only relying on aggregate statistics about this dataset. I will also propose countermeasures to mitigate this threat, similarly as for the linkability attack. I will conclude by presenting some open challenges in health data privacy.

Speaker: Steve Kremer
Title: Can Charlie distinguish Alice and Bob? (Automated verification of equivalence properties.)
Abstract: Formal, symbolic techniques for modelling and automatically analyzing security protocols are extremely successful and were able to discover many security flaws. Initially, these techniques were mainly developed to analyze authentication and confidentiality properties. Both these properties are trace properties and efficient tools for their verification exist. In more recent years anonymity-like properties have received increasing interest. Many flavors of anonymity properties are naturally expressed in terms of indistinguishability and modeled as an observational equivalence in process calculi. We will present recent advances in the verification of such indistinguishability properties.

Speaker: Dan Bogdanov
Title: Deploying secure computing for real-world applications
Abstract: Secure computation (SC) stands for a group of technologies for computing on encrypted inputs without decrypting them. In this talk, I will introduce Sharemind, a secure application server that uses secure computation for building privacy-preserving applications. Sharemind supports multiple secure computing technologies, with more mature ones supporting secure operations on encrypted integers, fixed-point and floating point numbers, strings and bits. We have built Sharemind-powered systems for analyzing confidential government tax and education databases, detect large-scale fraud from transactions and to build more secure cloud services. The talk will focus on scaling secure computing applications from efficient primitives to applications processing up to a hundred million records.

Speaker: Soumya Paul
Title: Approximate Probabilistic Verification of Hybrid Systems
Abstract:
Hybrid systems whose mode dynamics are governed by non-linear ordinary differential equations (ODEs) are often a natural model for biological processes. However such models are difficult to analyze. To address this, we develop a probabilistic analysis method by approximating the mode transitions as stochastic events. We assume that the probability of making a mode transition is proportional to the measure of the set of pairs of time points and value states at which the mode transition is enabled. To ensure a sound mathematical basis, we impose a natural continuity property on the non-linear ODEs. We also assume that the states of the system are observed at discrete time points but that the mode transitions may take place at any time between two successive discrete time points. This leads to a discrete time Markov chain as a probabilistic approximation of the hybrid system. We then show that for BLTL (bounded linear time temporal logic) specifications the hybrid system meets a specification if and only if its Markov chain approximation meets the same specification with probability 1. However, the construction of the Markov chain is infeasible. To get around this, we formulate a sequential hypothesis testing procedure for verifying approximately that the Markov chain meets a BLTL specification with high probability. Our case studies on cardiac cell dynamics and the circadian rhythm indicate that our scheme can be applied in a number of realistic settings.

(This is joint work with P.S. Thiagarajan, Benjamin Gyori, Liu Bing and R. Ramanathan.)

Speaker: Catalin Dragan
Title: Machine-checked proofs of privacy for electronic voting
Abstract: We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme.

Speaker: Juan Luis Jimenez Laredo
Title: Lessons Learned on Global Optimization: An Evolutionary Computation Approach
Abstract: Since the early days of computation, the complexity and size of problems to be solved by computational methods has continuously increased. Nowadays we are tackling problems in engineering, physics or biology that were out of imagination just few years ago. However, truly complex and high dimensional problems still pose a challenge to our ability for meeting reasonable solutions in a reasonable time. This talk aims at presenting some general lessons that I have learned when facing some of these challenges during the course of my research in global optimization. While there are no magical recipes for designing an optimizer (there is no free lunch), there are certain general questions that can be posed for efficiently tackling an optimization problem considering some of its features. This presentation will focus on posing and answering such questions from the perspective of evolutionary computation.

Speaker: Louis Fippo Fitime
Title: Efficient Static Analysis of Dynamical Properties of Automata Networks
Abstract:
Biological Regulatory Networks (BRNs) are usually used in systems biology for modelling, understanding and controlling the dynamics of different biological functions (differentiation, proliferation, proteins synthesis, apoptose) inside cells. Those networks are enhanced with experimental data that are nowadays more available which give an idea on the dynamics of BRNs components. Formal analysis of such models fails in front of the combinatorial explosion of generated behaviours despite the fact that BRNs provide abstract representation of biological systems.

This work handles hybrid modelling, the formal verification and control of Large Biological Regulatory Networks. This modelling is done thanks to stochastic automata networks by integrating time-series data.

Firstly, this work proposes a refining of the dynamics by estimation of stochastic and temporal (delay) parameters from time-series data and integration of those parameters in automata networks models. This integration allows the parametrisation of the transitions between the states of the system.

Secondly, this work develops static analysis by abstract interpretation in the stochastic automata networks allowing efficient under- and over-approximation of quantitative (probability and delay) reachability properties. This analysis enables to highlight the critical components to satisfy these properties.

Finally, taking advantage from the previous developed static analyses for the reachability properties in the qualitative point of view, and from the power of logic programming (Answer Set Programming), this work addresses the domain of control of system by proposing the identification of bifurcation transitions. Bifurcations are transitions after which the system can no longer reach a state that was previously reachable.

Speaker: Chiu Kai Wu
Title: Graph-theoretic Approach to Structural Controllability of Linear System and Some NP-Hard Results
Abstract:
Given a linear system, it is enough to consider a finite time in order to understand the entire behavior of the system. Structural controllability, in which one further neglects the exact dynamics, studies whether one is able to drive a state of the given system to arbitrary state. In 2011 and 2014, Barabasi's group proposed two algorithms concerning controllability and considered their applications towards several real-life networks.

The mathematical formulation and the corresponding graph theoretical approach (based on the work of Lin (1970), Murota and Poljak (1990)) for linear system will be stated. An abstract formulation of Barabasi's works will then be given and their NP-hardness of some variants will be stated.

Speaker: Alessandro Bruni
Title: Selene in Celf: Formalising Voting Protocols in Linear Logic
Abstract: Designing security protocols is a task notoriously known to be prone to mistakes. Voting protocols in particular have subtle and often contrasting properties like vote verifiability, receipt-freeness and coercion resistance, hence their precise characterisation is often complex to understand. In this talk, we aim to show how the foundational framework of linear logic can help to produce clear specifications of complex protocols, using the Selene internet voting protocol as a case in point. The notions of coherence and concurrency built into the linear logical framework Celf provide an initial check on the protocol well-formedness, and more advanced security properties can be expressed using dependent types and the higher-order syntactic approach of Celf.

Speaker: Alexandr Lenin
Title: Infeasibility Certificates for Attack Trees
Abstract: The talk will give an overview of various algebraic as well as empirical ways to certify infeasibility in attack trees. Infeasibility certificates are compact proofs that the considered task is unsolvable. In this talk we will focus on proofs allowing to certify infeasibility of the weighted monotone satisfiability (WMSAT) problem with application to attack trees. Corresponding computational methods to generate and validate such infeasibility proofs will be introduced.

Speaker: Cas Cremers
Title: On Post-Compromise Security (and messaging protocols you actually use)
Abstract:
We study communication with a party whose secrets have already been compromised. At first sight, it may seem impossible to provide any type of security in this scenario. However, under some conditions, practically relevant guarantees can still be achieved. We call such guarantees “post-compromise security”; they represent a natural continuation of the trend towards increased security against mass surveillance. We provide the first informal and formal definitions for post-compromise security, and show that it can be achieved in several scenarios.

At a technical level, we instantiate our informal definitions in the setting of authenticated key exchange (AKE) protocols, and develop two new strong security models for two different threat models. We show that both of these security models can be satisfied, by proposing two concrete protocol constructions and proving they are secure in the models. Our work leads to crucial insights on how post-compromise security can (and cannot) be achieved, paving the way for applications in other domains.

We show how our work relates to recent messaging protocol libraries, as used by WhatsApp, Facebook Messenger, and Google Allo.

Speaker: Karim Lounis
Title: A Stochastic Framework for Quantitative Analysis of Attack-Defense Trees
Abstract: Cyber attacks are becoming increasingly complex, practically sophisticated and organized. Losses due to such attacks are important, varying from the loss of money to business reputation spoilage. Therefore, there is a great need for potential victims of cyber attacks to deploy security solutions that allow the identification and/or prediction of potential cyber attacks, and deploy defenses to face them. In this paper, we propose a framework that incorporates Attack-Defense trees (ADTrees) and Continuous Time Markov Chains (CTMCs) to systematically represent attacks, defenses, and their interaction. This solution allows to perform quantitative security assessment, with an aim to predict and/or identify attacks and find the best and appropriate defenses to reduce the impact of attacks.

Speaker: Tim Muller
Title: How to Use Information Theory to Mitigate Unfair Rating Attacks
Abstract: In the recent past, we have used information theory to measure the damage of unfair rating attacks on the quality of a rating. Conversely stated: how much information is guaranteed to be transmitted by a rating, despite it possibly being an unfair rating inserted by an attacker? In our most recent paper, we try to use the techniques that we developed to improve the design of trust systems. Some factors are outside our control, such as who the attackers are and how they behave, as well as the level of subjectivity of the honest advisors. We can, however, control whom to ask which ratings. We prove 6 guidelines that improve the robustness of a rating system, by asking for the right ratings from the right people. The proofs are based on our information theoretic work.

Speaker: Cheng-Te Li
Title: Mining Big Social and Diffusion Data with Its Applications
Abstract: The structures of online social networks, such as Facebook and Twitter, are the essential social playgrounds where user interactions lead to the generation and diffusion of information. Social interactions and the dissemination of various information contents (e.g. news, opinions, and images) provide an unprecedented amount of data for researchers to investigate humanity and invent novel applications. In this talk, I will present our recent advances on mining, predicting, and applying social interactions and information diffusion. Specifically, the talk will deliver answers to deal with the following questions. (1) Which individuals in social networks are more influential to spread the information without prior knowledge? (2) Given a complex heterogeneous information network, how to extract compact but important knowledge for user profiling and detecting terrorists? (3) Assume Starbucks are seeking for new places to expand business, can we recommend Starbucks some candidate locations that can attract more customers? If time permits, I will briefly introduce more of our research outcomes on social and urban computing.

Speaker: Qixia Yuan
Title: Fast Simulation of Probabilistic Boolean Networks
Abstract: Probabilistic Boolean networks (PBNs) is an important mathematical framework widely used for modelling and analysing biological systems. PBNs are suited for modelling large biological systems, which more and more often arise in systems biology. However, the large system size poses a~significant challenge to the analysis of PBNs, in particular, to the crucial analysis of their steady-state behaviour. Numerical methods for performing steady-state analyses suffer from the state-space explosion problem, which makes the utilisation of statistical methods the only viable approach. However, such methods require long simulations of PBNs, rendering the simulation speed a crucial efficiency factor. For large PBNs and high estimation precision requirements, a slow simulation speed becomes an obstacle. In this paper, we propose a structure-based method for fast simulation of PBNs. This method first performs a network reduction operation and then divides nodes into groups for parallel simulation. Experimental results show that our method can lead to an approximately 10 times speedup for computing steady-state probabilities of a real-life biological network.

Speaker: Diego Agustin Ambrossio and Marcos Cramer
Title: A Non-Monotonic Logic for Distributed Access Control
Abstract: We define Distributed Access Control Logic (D-ACL), whose main difference from state-of-the-art says-based access control logics is that it is non-monotonic, thus allowing access denials to be modelled straightforwardly in the formalism. Additionally D-ACL allows for access rights and other properties relevant to access control to be defined inductively, which increases its expressive power compared to other first-order access control logics. The semantics of D-ACL is based on the well-founded semantics for autoepistemic logic. We define a query-driven decision procedure for the propositional fragment of D-ACL, which is designed in such a way that it allows to determine access rights while minimizing the information flow between principals in order to enhance security and reduce privacy concerns.

Speaker: Sasa Radomirovic
Title: Human Errors in Security Protocols
Abstract:
Many security protocols involve humans, not machines, as endpoints. The differences are critical: humans are not only computationally weaker than machines, they are naive, careless, and gullible.

We propose the first formal theory accounting for human errors in security protocols. We tackle the major problem that security protocols are designed and proven to be correct without taking the human users into account. Our theory allows to model more realistic humans that can be untrained or trained. Untrained humans have no knowledge about the protocol and may deviate arbitrarily from its specification. Trained humans generally follow rules or follow the protocol, but may make mistakes such as omitting a critical security check. The model allows to derive what general rules have to be known by a human such that desired security properties are provided by a protocol. We validate the utility of our model by analyzing and comparing several authentication protocols.

Joint work with David Basin and Lara Schmid.

Speaker: Yang Zhang
Title: Quantifying Location Sociality
Abstract: The emergence of location-based social networks provides an unprecedented chance to study the interaction between human mobility and social relations. In this work, we focus on quantifying whether a location is suitable for conducting social activities, and the notion is named location sociality. Being able to quantify location sociality creates practical opportunities such as urban planning and location recommendation. To quantify a location's sociality, we propose a mixture model of HITS and PageRank on a heterogeneous network linking users and locations. By exploiting millions of check-in data generated by Instagram users in New York and Los Angeles, we investigate the relation between location sociality and several location properties, such as location categories, rating and popularity. We further perform two case studies, i.e., friendship prediction and location recommendation, experimental results demonstrate the usefulness of our quantification.

Speaker: Boris Skoric
Title: Physical Unclonable Functions, optical and otherwise
Abstract: PUFs have become a mainstream research topic, and the first commercial applications have slowly found their way into the security market. In this talk I give an overview of PUF technologies and how they can be used for various purposes such as key storage, authentication, anti-counterfeiting, software to hardware binding, and tamper evidence. The focus will be on optical PUFs.

Speaker: Mahsa Taziki
Title: D2P: Distance-based Differential Privacy in Recommenders
Abstract: The upsurge in the number of web users over the last two decades has resulted in a significant growth of online information. This information growth calls for recommenders that personalize the information proposed to each individual user. Nevertheless, personalisation also opens major privacy concerns. This talk presents D2P, a novel protocol that ensures a strong form of differential privacy published in VLDB2015, which we call distance-based differential privacy, and which is particularly well suited to recommenders.

Speaker: Marc Beunardeau
Title: On the fly authentication and slow-motion zero-knowledge
Abstract: This is a two-part talk.
In the first part, we discuss on the fly authentication. Message authentication code (MAC) are tags at the end of a message that are a function of the message and a share secret between the sender and the receiver. This tag is computed by the sender, sent along with the message, and computed by the receiver. If the message is modified, it is impossible for the attacker to compute the corresponding new tag. Therefore any modification is detected.

We study the possibility to spread this tag in a message, so that a modification is detected before the whole message is received. We consider a setting in which the attacker has access to a side channel telling him when the receiver stops reading the message, allowing him to get information on which part of the tag was false. We try to add uncertainty to the stopping time, and to add nonce and duplicate detection to the protocol, as countermeasures to the attack.

In the second part, we discuss slow motion zero-knowledge. Discrete-logarithm authentication protocols are known to present two interesting features: The first is that the prover’s commitment, x = g^r , claims most of the prover’s computational effort. The second is that x does not depend on the challenge and can hence be computed in advance. Provers exploit this feature by pre-loading (or pre-computing) ready to use commitment pairs r_i, x_i. The r_i can be derived from a common seed but storing each x_i still requires 160 to 256 bits when implementing DSA or Schnorr. This paper proposes a new concept called slow motion zero-knowledge (SM-ZK). SM-ZK allows the prover to slash commitment size (by a factor of 4 to 6) by combining classical zero-knowledge and a timing side-channel. We pay the conceptual price of requiring the ability to measure time but, in exchange, obtain communication-efficient protocols.

Speaker: Katsiaryna Labunets
Title: Security Risk Assessment Methods: An Evaluation Framework and Theoretical Model of the Criteria Behind Methods' Success
Abstract: Over the past decades a significant number of methods to identify and mitigate security risks have been proposed, but there are few empirical evaluations that show whether these methods are actually effective. So how can practitioners decide which method is the best for security risk assessment of their projects? To this end, we propose an evaluation framework to compare security risk assessment methods that evaluates the quality of results of methods application with help of external industrial experts and can identify aspects having an effect on the successful application of these methods. The results of the framework application helped us to build the model of key aspects that impact the success of a security risk assessment. Among these aspects are i) the use of catalogues of threats and security controls which can impact methods' actual effectiveness and perceived usefulness and ii) the use of visual representation of risk models that can positively impact methods' perceived ease of use, but negatively affect methods' perceived usefulness if the visual representation is not comprehensible due to scalability issues. To further investigate these findings, we conducted additional empirical investigations: i) how different features of the catalogues of threats and security controls contribute into an effective risk assessment process for novices and experts in either domain or security knowledge, and ii) how comprehensible are different representation approaches for risk models (e.g. tabular and graphical). This presentation will focus on the results of empirical studies on comprehensibility of different representation approaches for risk models.

Speaker: Hongyang Qu
Title: Performance Study of Game-Theoretic Learning Algorithms
Abstract: A stochastic model checker is presented for analysing the performance of game-theoretic learning algorithms. The method enables the comparison of short-term behaviour of learning algorithms intended for use. The procedure of comparison is automated and it can be tuned for accuracy and speed. Users can choose from among various learning algorithms to select a suitable one for a given practical problem. The powerful performance of the method is enabled by a novel behaviour-similarity-relation, which compacts large state spaces into small ones. The stochastic model checking tool is tested on a set of examples classified into four categories to demonstrate the effectiveness of selecting suitable algorithms for distributed decision making.

Speaker: Pei Wang
Title: Translingual Obfuscation
Abstract: Program obfuscation is an important software protection technique that prevents attackers from revealing the programming logic and design of the software. We introduce translingual obfuscation, a new software obfuscation scheme which makes programs obscure by "misusing" the unique features of certain programming languages. Translingual obfuscation translates part of a program from its original language to another language which has a different programming paradigm and execution model, thus increasing program complexity and impeding reverse engineering. In this paper, we investigate the feasibility and effectiveness of translingual obfuscation with Prolog, a logic programming language. We implement translingual obfuscation in a tool called BABEL, which can selectively translate C functions into Prolog predicates. By leveraging two important features of the Prolog language, i.e., unification and backtracking, BABEL obfuscates both the data layout and control flow of C programs, making them much more difficult to reverse engineer. Our experiments show that BABEL provides effective and stealthy software obfuscation, while the cost is only modest compared to one of the most popular commercial obfuscators on the market. With BABEL, we verified the feasibility of translingual obfuscation, which we consider to be a promising new direction for software obfuscation.

Speaker: Yang Zhang
Title: An Empirical Study on User Access Control in Online Social Networks
Abstract: In recent years, access control in online social networks has attracted academia a considerable amount of attention. Previously, researchers mainly studied this topic from a formal perspective. On the other hand, how users actually use access control in their daily social network life is left largely unexplored. This work presents the first large-scale empirical study on users' access control usage on Twitter and Instagram. Based on the data of 150k users on Twitter and 280k users on Instagram collected consecutively during three months in New York, we have conducted both static and dynamic analysis on users' access control usage. Our findings include: female users and young users are more concerned about their privacy; users who enable their access control setting are less active and have smaller online social circles; global events and important festivals can influence users to change their access control settings. Furthermore, we exploit machine learning classifiers to perform an access control setting prediction. Through experiments, the predictor achieves a fair performance with the AUC equals to 0.70, indicating whether a user enables his access control setting or not can be predicted to a certain extent.

Speaker: Richard Clayton
Title: No room at the Inn? Analysing Hotel Room Poaching
Abstract: The organisers of many conferences arrange for blocks of rooms at appropriate hotels to be reserved for conference attendees, and they may contract to provide given levels of occupancy. Room poaching occurs when third parties approach attendees and persuade them to book through them. This activity is fraudulent when the third party misrepresents their relationship with the conference or fails to honour their obligations and leaves attendees with nowhere to stay. This paper presents a first-hand account of a room poaching incident at ESORICS 2015 and sets this in the context of the wider room poaching issue. Academic conference organisers can take some simple countermeasures to reduce the incidence of the problem.

Speaker: Florian Göpfert
Title: On the Hardness of LWE with Binary Error: Revisiting the Hybrid Lattice-Reduction and Meet-in-the-Middle Attack
Abstract: The security of many cryptographic schemes has been based on special instances of the Learning with Errors (LWE) problem, e.g., Ring-LWE, LWE with binary secret, or LWE with ternary error. However, recent results show that some subclasses are weaker than expected. In this work we show that LWE with binary error, introduced by Micciancio and Peikert, is one such subclass. We achieve this by applying the Howgrave-Graham attack on NTRU, which is a combination of lattice techniques and a Meet-in-the-Middle approach, to this setting. We show that the attack outperforms all other currently existing algorithms for several natural parameter sets. For instance, for the parameter set n = 256, m = 512, q = 256, this attack on LWE with binary error only requires 2⁸⁵ operations, while the previously best attack requires 2¹¹⁷ operations. We additionally present a complete and improved analysis of the attack, using analytic techniques. Finally, based on the attack, we give concrete hardness estimations that can be used to select secure parameters for schemes based on LWE with binary error.

Speaker: Yunior Ramirez-Cruz
Title: Adding redundancy to graph resolvability parameters
Abstract: In a large number of real life situations, it is necessary to uniquely identify the vertices of a graph. Metric generators achieve this by using the distances between vertices. In a graph G, a metric generator is a subset S of V(G) such that for every pair of vertices x,y of V(G) there exists a vertex z in S such that d_G(x,z) ≠ d_G(y,z). Several variations on the notion of metric generators have been proposed, which either modify the criteria determining which pairs of vertices need to be distinguished or the manner in which they are distinguished. In this talk we will cover extensions on the notion of metric generators, or some variations thereof, to handle practical problems arising from the fact that the real-life structure represented by the graph may vary over time, or information regarding some distance values may become unavailable. We will treat k-generators and simultaneous generators. A k-metric generator is a subset S of V(G) such that every pair of vertices x,y in V(G) is distinguished by at least k vertices of S. Simultaneous generators handle the case where we have a family {G1,G2,…,Gt} of graphs defined on a common vertex set V. A simultaneous metric generator for the family is a subset S of V that is a metric generator for every Gi. The talk will cover these extended notions of resolvability, including general characterizations and some interesting examples where these parameters are easy to determine, while noting the fact that extra complexity is added to the original problems in all cases. Considering that in some contexts the ability to uniquely identify vertices in graphs may be an undesired situation, e.g. users in social media data, we expect that this talk may lead to some discussion on how to possibly prevent this in the scenario of the new notions of resolvability.

Speaker: Yongjian Li
Title: paraVerifier: An Automatic Framework for Proving Parameterized Cache Coherence Protocols
Abstract: Parameterized verification of cache coherence protocols is an impottant but challenging research problem. We present in this paper our automatic framework paraVerifier to handle this problem: (1) it first discovers auxiliary invariants and the corresponding causal relations between invariants and protocol rules from a small reference instance of the verified protocol; (2) the discovered invariants and causal relations can then be generalized into their parameterized form to automatically construct a formal proof to establish the correctness of the protocol. paraVerifier has been successfully applied to a number of benchmarks.

Back to SRM presenations.

Contact

For questions and comments contact Jun or Peter .