IA072 Seminar on Concurrency

Programme

  • 19. 9. 2014 - dean's time off
  • 26. 9. 2014 - Arrangements
  • 3. 10. 2014 - Martin Jonáš - Efficiently solving quantified bit-vector formulas, FMSD 2013 (by C. M. Wintersteiger, Y. Hamadi, and L. de Moura).
  • 10. 10. 2014 - Petr Bauch - LTL Model Checking via Non-termination Analysis

Abstract: Unrolling the transition relation of programs leads to state space explosion unmanageable by state-of-the-art verifiers. Fortunately, for certain classes of programs and certain properties, the correctness can be checked without unrolling. In this talk we first describe the known approaches of employing termination analysis to decide validity of LTL properties. Given that termination analysis is incomplete, such approaches cannot prove property violation. Thus we further describe two novel approaches of lifting the non-termination analysis to full LTL model checking: first, via MaxSAT-directed generation of invariants and second, via PDR-like approximation of recurrent sets.

Complementation of Büchi automata is in general non-trivial task. Similarly to finite automata over finite words, when the given BA is deterministic and total, we can get an automaton for the complement easily - by dualizing the accepting condition. In such a case we get a co-Büchi automaton. When the BA is not deterministic, situation gets much more complicated. Complementation by determinization involves huge blow-up in state space and one usually gets Street accepting condition, which is more complex to check and work with. Some other complementations were designed, the best known involves at most (0.96n)^n blow-up in states. In automata-based approach to terminal analysis BA of a special shape appear. They are almost deterministic and have only one Büchi accepting state. We show an alternative complementation procedure that is sufficient for this kind of automata.

  • 5. 12. 2014 - Martin Kučera - Abstract satisfaction, POPL 2014 (by V. D'Silva, L. Haller, and D. Kroening).
  • 12. 12. 2014 - Petr Bauch - Inductive data flow graphs, POPL 2013 (by A. Kincaid, Z. Farzan, and A. Podelski).
  • (15. 12. 2014, FMDSA seminar, 14:00 in C417 - Marek Trtík - Combined Numerical Analysis of C Programs)
  • 19. 12. 2014 - cancelled (no speaker)

Papers to present:

 

Předchozí
Následující