• 20. 9 . 2019 - Arrangement
• 27. 9. 2019 - Marek Chalupa - Checking Safety Properties Using Induction and a SAT-Solver
•  4. 10. 2019 - cancelled (no speaker)
  
• 8. 10. 2019 - Donald Knuth
  
• 9. 10. 2019 - Dana Scott
  
• 11. 10. 2019 - cancelled (no speaker)
• 18. 10. 2019 - Adam Fiedler - 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.
• 25. 10. 2019 - cancelled (no speaker)
• 1. 11. 2019 - cancelled (ATVA 2019)
  
• 8. 11. 2019 - Tomáš Jašek - S. Kumar, A. Sanyal, V. R, and P. Shah: Property Checking Array Programs Using Loop Shrinking, TACAS 2018. [slides][proof of Theorem 1 (in Slovak)]
  
• 15. 11. 2019 - Juraj Major - J. Křetínský, T. Meggendorfer, C. Waldmann, and M. Weininger: Index Appearance Record for Transforming Rabin Automata into Parity Automata, TACAS 2017.
• 22. 11. 2019 - cancelled (no speaker)
• 29. 11. 2019 - cancelled (no speaker)
• 6. 12. 2019 - Vladimír Štill - Local Nontermination Detection for Parallel C++ Programs (joint work with J. Barnat)
  
• 13. 12. 2019 - Marek Jankola - J. Esparza, J. Křetínský, S. Sickert: One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata, LICS 2018.
• 20. 12. 2019 - cancelled (Xmas)
  

Papers on automata (mostly omega-automata):

• Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi: Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications.
• Yu-Fang Chen, Yong Li, Xuechao Sun, Andrea Turrini, Junnan Xu: ROLL 1.0: 𝜔-Regular Language Learning Library, TACAS 2019.
• Loris D'Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva: Symbolic Register Automata, CAV 2019.
  
• George Argyros and Loris D'Antoni: The Learnability of Symbolic Automata, CAV 2018.
• Vrunda Dave, Paul Gastin and Krishna S.: Regular Transducer Expressions for Regular Transformations over infinite words, LICS 2018.
  
• 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.

Papers on slicing:

• 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 program analysis and verification:

• Philipp Dominik Schubert, Ben Hermann, Eric Bodden: PhASAR: An Inter-Procedural Static Analysis Framework for C/C++, TACAS 2019.
• Dejan Janovic, Bruno Duterte: Property-Directed k-Induction, FMCAD 2016
• Arie Gurfinkel, Alexander Ivrii: K-Induction without Unrolling, FMCAD 2017
  
• Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta: Quantified Invariants via Syntax-Guided Synthesis, CAV 2019.
• Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel: Interpolating Strong Induction, CAV 2019.
• Patrick Cousot, Roberto Giacobazzi, Francesco Ranzato: A²I: abstract² interpretation, POPL 2019.
• Johannes Späth, Karim Ali, Eric Bodden: Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems, POPL 2019.
  
• Daniel Neider, P. Madhusudan, Pranav Garg, Shambwaditya Saha and Daejun Park: Invariant Synthesis for Incomplete Verification Engines, TACAS 2018.
  
• K. L. McMillan: Lazy Abstraction with Interpolants, CAV 2006.
• B. Wachter, D. Kroening, and J. Ouaknine: Verifying multi-threaded software with impact, FMCAD 2013.
  

Papers on SAT/SMT solving:

• Junaid Babar, Chuan Jiang, Gianfranco Ciardo, Andrew Miner: Edge-Specified Reduction Binary Decision Diagrams, TACAS 2019.
  
• 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

Others papers to present:

• E. Hrushovski, J. Ouaknine, A. Pouly, J. Worrell: Polynomial Invariants for Affine Programs, LICS 2018.
• K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop: Edit Distance for Pushdown Automata, ICALP 2015.
• 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.
• 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