Talks & Seminars
Reachability Expressions: Metaprograms for Guiding Symbolic Reachability .
Prof. Supratik Chakraborty, IIT Bombay
Date & Time: September 5, 2007 11:00
Venue: F.C.Kohli Audi.
Symbolic reachability analysis is a technique for determining whether a set of nodes in a graph is reachable from another set of nodes, without actually representing the nodes and edges of the graph explicitly in memory. Symbolic reachability has recently found widespread use in applications spanning analysis, optimization and verification of software and hardware systems, where extremely large state spaces have to be searched. We discuss a framework for uniformly specifying a wide range of strategies for exact and approximate symbolic reachability analysis. The framework, called reachability expressions, allows specifying search strategies using a decomposition of the set of transitions in a state transition system, and also permits decomposing the overall state space into clusters/projections of states, on which different search strategies may be applied. Each reachability expression has an operational semantics that translates to a search strategy. Several optimizations at the level of expressions then translate to improved heuristics for searching, as has been demonstrated in experiments. Given a class of reachability expressions, we also have a simple way of determining whether the set of states obtained using one expression is equal to or over/under approximates that obtained using another expression. This gives rise to a provable meta-programming approach for guiding the search in very large state spaces
Speaker Profile:
List of Talks


Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback