RESOURCES

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision | Last revision Both sides next revision | ||

seminars:2008 [2009/06/29 08:40] vkuncak |
seminars:2008 [2009/06/29 08:43] vkuncak |
||
---|---|---|---|

Line 4: | Line 4: | ||

\\ | \\ | ||

- | ====== 2008 (inverse chronological order) ====== | + | ====== 2008 ====== |

- | ===== Faster Symmetry Discovery using Sparsity of Symmetries ===== | + | //In inverse chronological order// |

- | | + | |

- | * 2009-06-26 - 14:15, **BC01** [[http://www.eecs.umich.edu/~karem/|Karem A. Sakallah]] (Scheduled as Part of Summer Research Institute) | + | |

- | | + | |

- | Many computational tools have recently begun to benefit from the use of the symmetry inherent in the tasks they solve, and use general-purpose graph symmetry tools to uncover this symmetry. However, existing tools suffer quadratic runtime in the number of symmetries explicitly returned and are of limited use on very large, sparse, symmetric graphs. This paper introduces a new symmetry-discovery algorithm which exploits the sparsity present not only in the input but also the output, i.e., the symmetries themselves. By avoiding quadratic runtime on large graphs, it improves state-of the-art runtimes from several days to less than a second. | + | |

- | | + | |

- | ==== Sliding Window Abstraction for Infinite Markov Chains ==== | + | |

- | | + | |

- | * 2009-06-25 - 09:30 to 10:00 Maria Mateescu | + | |

- | | + | |

- | We present an on-the-ﬂy abstraction technique for inﬁnite-state con- | + | |

- | tinuous-time Markov chains. We consider Markov chains that are specified by a | + | |

- | ﬁnite set of transition classes. Such models naturally represent biochemical reac- | + | |

- | tions and therefore play an important role in the stochastic modeling of biological | + | |

- | systems. We approximate the transient probability distributions at various time in- | + | |

- | stances by solving a sequence of dynamically constructed abstract models, each | + | |

- | depending on the previous one. Each abstract model is a ﬁnite Markov chain that | + | |

- | represents the behavior of the original, inﬁnite chain during a specfic time inter- | + | |

- | val. Our approach provides complete information about probability distributions, | + | |

- | not just about individual parameters like the mean. The error of each abstrac- | + | |

- | tion can be computed, and the precision of the abstraction reﬁned when desired. | + | |

- | We implemented the algorithm and demonstrate its usefulness and efficiency on | + | |

- | several case studies from systems biology. | + | |

- | | + | |

- | * 2009-06-25 - 10:00 to 12:00 Damien Zufferey's and Thibaud Hottelier's Master Thesis Defense | + | |

- | | + | |

- | ===== Invariants for Arrays and Matrices (Thibaud Hottelier)===== | + | |

- | | + | |

- | We present a loop property generation method for loops iterating over multi-dimensional | + | |

- | arrays. When used on matrices, our method is able to infer their shapes (also | + | |

- | called types), such as upper-triangular, diagonal, etc. To generate loop properties, we | + | |

- | first transform a nested loop iterating over a multi-dimensional array into an equivalent | + | |

- | sequence of unnested loops. Then, we infer quantified loop invariants for each unnested | + | |

- | loop using a generalization of a recurrence-based invariant generation technique. These | + | |

- | loop invariants give us conditions on matrices from which we can derive matrix types | + | |

- | using a first-order theorem prover. Invariant generation is implemented in the software | + | |

- | package Aligator and the type derivation is performed by the theorem prover Vampire. | + | |

- | When run on the Java matrix package JAMA, our tool based on this method was able to | + | |

- | infer automatically matrix all types describing the matrix shapes guaranteed by JAMA’s | + | |

- | API. | + | |

- | | + | |

- | We have also applied our method to a large number of loops over one-dimensional | + | |

- | arrays, extracted from C programs. Non-trivial invariants can be inferred in many | + | |

- | cases. The experimental evaluations provides practical justifications for the scalability | + | |

- | and time-efficiency of our approach. | + | |

- | | + | |

- | ===== Verification of Concurrent Asynchronous Message-passing Programs (Damien Zufferey)===== | + | |

- | | + | |

- | Writing concurrent programs is a very delicate task. The nondeterminism | + | |

- | introduced by the scheduler makes bugs in concurrent programs hardly | + | |

- | reproducible.Formal verification can help the programmer to find such | + | |

- | bugs. In this thesis we focus on actor programs. Actors provide a model | + | |

- | for concurrent programs based on asynchronous message passing. The | + | |

- | contribution of this report is twofold. First we detail our | + | |

- | investigation of static systems of actors, i.e. actors programs where | + | |

- | the number of created actors is finite and known at compile time. We | + | |

- | develop a technique for proving deadlock freedom of such systems. We | + | |

- | achieve a good level of scalability through a heuristic that detects | + | |

- | potential deadlocks. Finally we explore the possibility of extending the | + | |

- | static model with dynamic actor creation. Due to the undecidability of | + | |

- | all verification related problems for the general class of system with | + | |

- | actor creation, we restrict ourself to certain systems which we call | + | |

- | star topologies. In star topologies, only a finite set of actors can | + | |

- | create other actors and the topology is restricted to a star shape, | + | |

- | where dynamically created actors cannot communicate with each other. In | + | |

- | practice, programs following a client-sever kind of communication fall | + | |

- | into this category of star topologies. | + | |

- | | + | |

- | \\ | + | |

- | * 2009-06-25 - 14:30 to 15:00 Rohit Singh, "Quantitative Synthesis"\\ | + | |

- | | + | |

- | * 2009-06-25 - 15:00 to 15:30 Ritesh Gupta, "Hybrid approach to analyze Markov chains"\\ | + | |

- | \\ | + | |

- | \\ | + | |

- | | + | |

- | | + | |

- | ===== Program Verification and Synthesis over Predicate Abstraction ===== | + | |

- | | + | |

- | * 2009-06-25 - 16:15 [[http://www.cs.umd.edu/~saurabhs/|Saurabh Srivastava]] | + | |

- | | + | |

- | | + | |

- | Static determination of program correctness (verification) and automatic program construction (synthesis) are two important challenges in programming languages research. Due to the undecidable nature of both problems no easy solutions are feasible. In this talk we present our work on program verification and synthesis, presenting techniques for both using Satisfiability Modulo Theory (SMT) solvers. Very efficient SMT solvers are now available and we use them to construct powerful verification techniques. Verification can be accomplished by discovering appropriate invariants--facts that hold in every execution of the program. | + | |

- | | + | |

- | We present three novel algorithms that discover sophisticated invariants using SMT solvers. Two of these algorithms use an iterative approach, one computing the weakest invariants and the other the strongest invariants, while the third employs a constraint-based approach to encode the invariant as a SAT instance. | + | |

- | | + | |

- | We have implemented the techniques developed under the umbrella project, Verification and Synthesis using SMT Solvers (VS3), in a tool by the same name. Preliminary experiments using VS3 show promising results. In particular, we discuss its power in verifying full correctness for all major sorting algorithms, which are considered some of the most difficult benchmarks for verification. Verifying full correctness for sorting algorithms requires inferring \forall\exists invariants for permutation properties and \forall invariants for sortedness properties. | + | |

- | | + | |

- | Time permitting, we will briefly discuss a new principled approach to program synthesis that builds on program verification. We demonstrate encouraging preliminary results for program synthesis. | + | |

- | | + | |

- | Project Webpage: http://www.cs.umd.edu/~saurabhs/pacs | + | |

- | | + | |

- | | + | |

- | \\ | + | |

- | * 2009-06-26 - 13:30, BC 355 Philippe Rannou, "Quantitative Languages" | + | |

- | \\ | + | |

===== Computing Convex Hulls by Automata Iteration ===== | ===== Computing Convex Hulls by Automata Iteration ===== |