The seminar will have the form of Zoom meeting, usually on Friday at 10am.

The current schedule follows (and it will be updated)

• 9. 10. 2020 - Arrangement (starting exceptionally at 11:00)
  
• 16. 10. 2020 - Anička Řechtáčková - Value relations analysis
  
• 23. 10. 2020 - Adam Fiedler - Introduction to description logics [slides]
  
• 30. 10. 2020 - Tomáš Jašek - Johannes Späth, Karim Ali, Eric Bodden: Context-, Flow- and Field-Sensitive Data-Flow Analysis using Synchronized Pushdown Systems, POPL 2019. [slides]
• 6. 11. 2020 - cancelled (no speaker)
  
• 13. 11. 2020 - Marek Jankola - H. Rahmani and J. M. O'Kane: What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints, to appear at IROS 2020.
  
• 20. 11. 2020 - Terka Schwarzová - S. Sickert and J. Esparza: An Efficient Normalisation Procedure for LinearTemporal Logic and Very Weak Alternating Automata, LICS 2020.
• 27. 11. 2020 - cancelled (no speaker)
• 4. 12. 2020 - Ján Jančár - Formal verification in constant-time cryptography [slides]
  
• 11. 12. 2020 - cancelled (no speaker)
• 18. 12. 2020 - cancelled (no speaker)
• 8. 1. 2021 - cancelled (no speaker)
  
• 15. 1. 2021 - cancelled (no speaker)
  
• 19. 2. 2021 - Marek Chalupa - TBA

Suggested papers for presentation

Papers on automata (mostly omega-automata):

• 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.
• V. Dave, P. Gastin, and K. S: Regular Transducer Expressions for Regular Transformations over infinite words, LICS 2018.
• Florian Renkin. Alexandre Duret-Lutz, and Adrien Pommellet : Practical “Paritizing” of Emerson-Lei Automata
  

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.
• Magnus Lång and Konstantinos Sagonas : Parallel Graph-Based Stateless Model Checking, ATVA 2020
  
  
• 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.
• 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:

•  Ali Asadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, Andreas Pavlogiannis Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth, ATVA 2020
  
• K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop: Edit Distance for Pushdown Automata, ICALP 2015.
• R. Bodik and B. Jobstmann: Algorithmic program synthesis: introduction, STTT 15(5-6), 2013.
• 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