IA072 Seminar on Concurrency

Programme

  • 21. 9 . 2018 - Arrangements
  • 5. 10. 2018 - cancelled (no speaker)
  • 12. 10. 2018 - moved to Mendel Museum on 10. 10. 2018 at 16:00: Javier Esparza - Black Ninjas in the Dark: Analyzing Population Protocols
  • 19. 10. 2018 - Pavel Čadek - Using Loop Bound Analysis For Invariant Generation (FMCAD presentation rehearsal)
    • Abstract: The problem of loop bound analysis can conceptually be seen as an instance of invariant generation. However, the methods used in loop bound analysis differ considerably from previous invariant generation techniques. Interestingly, there is almost no previous work comparing the two sets of techniques. In our paper, we show that loop bound analysis methods can efficiently produce invariants which are hard to prove for state-of-the-art invariant generation techniques (e.g., polynomial invariants or invariants relating many variables) and thus enrich the tool-set of invariant analysis
  • 26. 10. 2018 - Marek Chalupa - S. Anand, P. Godefroid, and N. Tillmann: Demand-Driven Compositional Symbolic Execution, TACAS 2008.
  • 2. 11. 2018 - Martina Vitovská - J. Li, S. Zhu, Y. Zhang, G. Pu, and M. Y. Vardi: Safety model checking with complementary approximations, ICCAD 2017.
  • 9. 11. 2018 - Katka Sloupová - A. Zeljić, P. Backeman, Ch. M. Wintersteiger, and P. Rümmer: Exploring Approximations for Floating-Point Arithmetic Using UppSAT, IJCAR 2018.
  • 16. 11. 2018 - cancelled (ICFEM 2018,  LPAR 2018)
  • 23. 11. 2018 - cancelled (LPAR 2018)
  • 30. 11. 2018 - Martin Jonáš - Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (Presentation from LPAR 2018)
    • Abstract: In general, deciding satisfiability of quantified bit-vector formulas becomes harder with increasing maximal allowed bit-width of variables and constants. However, this does not have to be the case for formulas that come from practical applications. For example, software bugs often do not depend on the specific bit-width of the program variables and would manifest themselves also with much lower bit-widths. We experimentally evaluate this thesis and show that satisfiability of the vast majority of quantified bit-vector formulas from the SMT-LIB repository remains the same even after reducing bit-widths of variables to a very small number of bits. This observation may serve as a starting-point for development of heuristics or other techniques that can improve performance of SMT solvers for quantified bit-vector formulas.
  • 7. 12. 2018 - Vladimír Štill - D. Schemmel, J. Büning, O. S. Dustmann, T. Noll, and K. Wehrle: Symbolic Liveness Analysis of Real-World Software, CAV 2018.
  • 14. 12. 2018 - cancelled (no speaker)

Papers on omega-automata:

Papers on SAT/SMT solving:

Papers on slicing:

Papers on games and synthesis:

Others papers to present:

 

Předchozí
Následující