• 20.  9.  2013 - Arrangements
• 27.  9.  2013 - Martin Kučera - K. L. McMillan: Interpolation and SAT-Based Model Checking, CAV 2003. +  A. R. Bradley: SAT-Based Model Checking without Unrolling, VMCAI 2011.
•   4. 10. 2013 - Marek Trtík - Symbolic memory with pointers (original work).
• 11. 10. 2013 - cancelled (speaker not ready)
• 18. 10. 2013 - cancelled (ATVA 2013)
• 25. 10. 2013 - Petr Bauch - D. Beyer, T. A. Henzinger, M. E. Keremoglu, P. Wendler: Conditional model checking: a technique to pass information between verifiers, SIGSOFT FSE 2012.
•   1. 11. 2013 - cancelled (speaker not ready)
•   8. 11. 2013 - Karolína Malá - O. Kupferman: Recent Challenges and Ideas in Temporal Synthesis, SOFSEM 2012. [slides]
• 15. 11. 2013 - Honza Dupal - K. J. Ottenstein and L. M. Ottenstein: The Program Dependence Graph in a Software Development Environment, ACM SIGPLAN Notices, 1984.
• 22. 11. 2013 - Tomáš Brukner - D. Distefano: Attacking Large Industrial Code with Bi-Abductive Inference, FMICS 2009.
• 29. 11. 2013 - Fanda Blahoudek - Safra's construction.
•   6. 12. 2013 - Viktor Toman - S. C. Krishnan, A. Puri, R. K. Brayton: Deterministic w Automata vis-a-vis Deterministic Buchi Automata, ISAAC 1994.
• 13. 12. 2013 - Pavel Čadek - S. Gulwani and F. Zuleger: The Reachability-Bound Problem, PLDI 2010.
• 20. 12. 2013 -

Papers to present:

• B. Elkarablieh, P. Godefroid, and M. Y. Levin: Precise pointer reasoning for dynamic test generation, ISSTA 2009.

• P. Madhusudan, G. Parlato, and X. Qiu: Decidable logics combining heap structures and data, POPL 2011.

• D. Vanoverberghe, N. Tillmann, and F. Piessens: Test Input Generation for Programs with Pointers, TACAS 2000.

• S. Gulwani, K. K. Mehra, and T. Chilimbi: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity, POPL 2009.

• 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.

• K. Dudka, P. Peringer, and T. Vojnar: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, CAV 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