• 22. 9. 2017 - cancelled
• 29. 9. 2017 - cancelled
• 6. 10. 2017 - Arrangements + Martina Vitovská - K. R. M. Leino and V. Wüstholz: Fine-Grained Caching of Verification Results, CAV 2015.
• 13. 10. 2017 Marek Chalupa - L. Alt, S. Asadi, H. Chockler, K. Even Mendoza, G. Fedyukovich, A. Hyvärinen, and N. Sharygina: HiFrog: SMT-based Function Summarization for Software Verification, TACAS 2017; A. Hyvärinen, S. Asadi, K. Even-Mendoza, G. Fedyukovich, H. Chockler and N. Sharygina: Theory Refinement for Program Verification, SAT 2017.
• 20. 10. 2017 - cancelled
• 27. 10. 2017 - Martin Jonáš - M. Heizmann, Ch. Schilling, and Daniel Tischner: Minimization of Visibly Pushdown Automata Using Partial Max-SAT, TACAS 2017.
• 3. 11. 2017 - Vláďa Štill - K. Dudka, P. Peringer, T. Vojnar: Byte-Precise Verification of Low-Level List Manipulation, SAS 2013.
• 10. 11. 2017 - Juraj Hromkovič - Teaching mathematics and computer science as research instruments (MU Seminar Series, 9:00 at Mendel Museum)
• 24. 11. 2017 - Fanda Blahoudek - S. Sickert, J. Esparza, S. Jaax, J. Křetínský: Limit-Deterministic Büchi Automata for Linear Temporal Logic, CAV 2016.
• 1. 12 2017 - Katka Sloupová - M. Heule, O. Kullmann, S. Wieringa, A. Biere: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads, Haifa Verification Conference 2011. (CANCELLED)
• 8. 12. 2017 - Honza Tušil -D. Lucanu, V. Rusu, A. Arusoaie: A generic framework for symbolic execution: A coinductive approach, Journal of Symbolic Computation 80 (2017).
• 15. 12. 2017 - Viki Vozárová - T. Fiedor, L. Holík, P. Janků, O. Lengál, and T. Vojnar: Lazy Automata Techniques for WS1S, TACAS 2017.

Papers on omega-automata:

• D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata, GandALF 2017.
• Y. Li, Y.-F. Chen, L. Zhang, and D. Liu: A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees, TACAS 2017.
• J. Esparza, J. Křetínský, J.-F. Raskin, and S. Sickert: From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata, TACAS 2017.
• J. Křetínský, T. Meggendorfer, C. Waldmann, and M. Weininger: Index Appearance Record for Transforming Rabin Automata into Parity Automata, TACAS 2017.

Papers on SAT/SMT solving:

• M. Heule, O. Kullmann, S. Wieringa, A. Biere: Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads, Haifa Verification Conference 2011.
• J. P. Inala, R. Singh, A. Solar-Lezama: Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers, SAT 2016.
• A. Fröhlich, A. Biere, C. M. Wintersteiger, Y. Hamadi: Stochastic Local Search for Satisfiability Modulo Theories, AAAI 2015.
• Selected chapters from the Handbook of Satisfiability

Papers on slicing:

• S. Horwitz and T. W. Reps: The Use of Program Dependence Graphs in Software Engineering, ICSE 1992.
• D. W. Binkley and K. B. Gallagher: Program Slicing, Advances in Computers 43, 1996.
• S. Staiger-Stoehr: Practical integrated analysis of pointers, dataflow and control flow, ACM Trans. Program. Lang. Syst. 35(1), 2013.
• M. Aung, S. Horwitz, R. Joiner, and T. W. Reps: Specialization Slicing, ACM Trans. Program. Lang. Syst. 36(2), 2014.
• J. Silva: A Vocabulary of Program Slicing-Based Techniques, ACM Comput. Surv. 44(3), 2012.

Papers on games and synthesis:

• K. Chatterjee, M. Henzinger, and V. Loitzenbauer: Improved Algorithms for One-Pair and k-Pair Streett Objectives, LICS 2015
• R. Bodik and B. Jobstmann: Algorithmic program synthesis: introduction, STTT 15(5-6), 2013.

Others papers to present:

• K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop: Edit Distance for Pushdown Automata, ICALP 2015.
• A. Das, S. K. Lahiri, A. Lal, and Y. Li: Angelic Verification: Precise Verification Modulo Unknowns, CAV 2015.
• Y. Demyanova, T. Pani, H. Veith, and F. Zuleger: Empirical Software Metrics for Benchmarking of Verification Tools, CAV 2015.
• R. Singh and S. Gulwani: Predicting a Correct Program in Programming by Example, CAV 2015.
• A. Farzan, Z. Kincaid, and A. Podelski: Proofs that count, POPL 2014.
• B. Jeannet, P. Schrammel, and S. Sankaranarayanan: Abstract acceleration of general linear loops, POPL 2014.
• D. Kroening, M. Lewis, and G. Weissenbacher: Under-Approximating Loops in C Programs for Fast Counterexample Detection, CAV 2013.
• D. Vanoverberghe, N. Tillmann, and F. Piessens: Test Input Generation for Programs with Pointers, TACAS 2000.
• X. Deng, J. Lee, and Robby: Efficient and formal generalized symbolic execution, Autom. Soft. Eng. 2011.
• S. Khurshid, C. S. Pasareanu, and W. Visser: Generalized Symbolic Execution for Model Checking and Testing, TACAS 2003.
• A. Colin and G. Bernat: Scope-Tree: A Program Representation for Symbolic Worst-Case Execution Time Analysis, ECRTS 2002.
• S. Gulwani, S. Jain, and E. Koskinen: Control-flow refinement and progress invariants for bound analysis, PLDI 2009.
• P. Godefroid and D. Luchaup: Automatic Partial Loop Summarization in Dynamic Test Generation, ISSTA 2011.
• C. Calcagno and D. Distefano: Infer: an Automatic Program Verifier for Memory Safety of C Programs, NFM 2011.
• The Calculus of Computation
• Counterexample-Guided Abstraction Refinement
• The SLAM Project: Debugging System Software via Static Analysis
• SLAM2: Static Driver Verification with Under 4% False Alarms