• 21. 2. 2020 - cancelled (Honza not in Brno)
  
• 28. 2 . 2020 - Arrangement
• 6. 3. 2020 - cancelled (no speaker and doctoral promotion of Martin Jonáš; the promotion has been eventually cancelled due to coronavirus in Italy)

The rest of the programme is moved to Gmail videocalls due to the coronavirus quarantine. We currently plan the following videocalls: (Please be logged in gmail.com slightly before 10am to set up the call. This instruction is for students as well as for teachers.)

•  27. 3. 2020 - Juraj Major - R. Dimitrova, B. Finkbeiner, and H. Torfah: Approximate Automata for Omega-regular Languages, ATVA 2019. [potential research topic]
  
• 3. 4. 2020 - Tomáš Jašek - D. Kroening, M. Lewis, and G. Weissenbacher: Under-Approximating Loops in C Programs for Fast Counterexample Detection, CAV 2013.
• 17. 4. 2020 [pushed to 14:00] - Marek Jankola - L. D'Antoni, T. Ferreira, M. Sammartino, and A. Silva: Symbolic Register Automata, CAV 2019.
  
• 24. 4. 2020 - Tereza Šťastná - G. D. Plotkin: A Note on Inductive Generalization, Machine Intelligence 5, 1970.
  
• 1. 5. 2020 - May Day
• 8. 5. 2020 - Victory Day
• 15. 5. 2020 - cancelled (no speaker)
  
• 29. 5. 2020 [pushed to 15:00] - Marek Chalupa - S. Danicic, R. W. Barraclough, M. Harman, J. D. Howroyd, Á. Kiss, and M. R.Laurence: A unifying theory of control dependence and its application to arbitrary program structures, TCS 412, 2011.
  

Suggested papers for presentation

Papers on automata (mostly omega-automata):

• S. Sickert and J. Esparza: An Efficient Normalisation Procedure for LinearTemporal Logic and Very Weak Alternating Automata, LICS 2020.
  
• S. Bansal, Y. Li, L. M. Tabajara, and M. Y. Vardi: Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications.
  
• Y.-F. Chen, Y. Li, X. Sun, A. Turrini, and J. Xu: ROLL 1.0: 𝜔-Regular Language Learning Library, TACAS 2019.
• G. Argyros and L. D'Antoni: The Learnability of Symbolic Automata, CAV 2018.
• V. Dave, P. Gastin, and K. 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. 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