• 16. 9. 2022 - Arrangements (presented by Marek, Honza at KLEE workshop 2022)
• 23. 9. 2022 - cancelled (no speaker)
  
• 30. 9. 2022 - Honza Tušil - R. Beutner and B. Finkbeiner: Software Verification of Hyperproperties Beyon k-Safety, CAV 2022.
  
• 7. 10. 2022 - Vincent Mihalkovič - K. Yakdan, S. Eschweiler, E. Gerhards-Padilla, M. Smith: No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantics-Preserving Transformations, NDSS 2015.
  
• 14. 10. 2022 - Marek Jankola - C. Stanford, M. Veanes, and N. Bjørner: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints, PLDI 2021.
• 21. 10. 2022 - Jakub Šárník - V. Dave, P. Gastin, and K. S: Regular Transducer Expressions for Regular Transformations over infinite words, LICS 2018.
• 4. 11. 2022 - Pavel Šímovec - M. Böhme, V. Pham and A. Roychoudhury: Coverage-Based Greybox Fuzzing as Markov Chain, IEEE 2019. (cancelled)
  
• 11. 11. 2022 - Robert Konicar - A. Pandey, P. R. Goutham, and S. Roy: Deferred Concretization in Symbolic Execution via Fuzzing, ISSTA 2019.
• 18. 11. 2022 - Jiří Gavenda - F. K. Aljaafari, R. Menezes, E. Manino, F. Shmarov, M. A. Mustafa, and L. C. Cordeiro: Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs, 2022.
• 25. 11. 2022 - Nastasia Kovářová - C. Calcagno and D. Distefano: Infer: an Automatic Program Verifier for Memory Safety of C Programs, NFM 2011.
• 2. 12. 2022 - Vincent (cancelled)
  
• 9. 12. 2022 - Paulína Ayaziová - F. Busse, P. Gharat, C. Cadar, and A. F. Donaldson: Combining Static Analysis Error Traces with Dynamic Symbolic Execution (Experience Paper), ISSTA 2022.

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, AAAI 2020.
• Y.-F. Chen, Y. Li, X. Sun, A. Turrini, and J. Xu: ROLL 1.0: 𝜔-Regular Language Learning Library, TACAS 2019.

Papers on slicing:

• M. Sridharan, S. J. Fink, and R. Bodík: Thin Slicing, PLDI 2007.

• L. Mecenero, R. Paramitha, I. Pashchenko, and F. Massacci: Lightweight Parsing and Slicing for Bug Identification in C, ARES 2022.

• B. Lisper, A. N. Masud, and H. Khanfar: Static Backward Demand-Driven Slicing, PEPM 2015.

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

• Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham, and James R. Wilcox: Learning the Boundary of Inductive Invariants, POPL 2021.
• Tzu-Han Hsu, César Sánchez, Borzoo Bonakdarpour. Bounded Model Checking for Hyperproperties
  
• Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
  
• Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat. Verifying Array Manipulating Programs with Full-Program Induction. TACAS 2021.
  
• Dirk Beyer and Matthias Dangl: Software Verification with PDR: An Implementation of the State of the Art, TACAS 2020.
• Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan: Deciding
  Memory Safety for Single-Pass Heap-Manipulating Programs, POPL 2020.
  
• Magnus Lång and Konstantinos Sagonas: Parallel Graph-Based Stateless Model Checking, ATVA 2020.
• 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.
• 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 of fuzzing:

• A long list of recent papers on fuzzing
  
• A. Vishnyakov, A. Fedotov, D. Kuts, A. Novikov, D. Parygina, E. Kobrin, V. Logunova, P. Belecky, and S. Kurmangaleev: Sydr: Cutting Edge Dynamic Symbolic Execution, ISPRAS 2020.
• H. Peng, Y. Shoshitaishvili and M. Payer: T-Fuzz: Fuzzing by Program Transformation, IEEEE 2018.
• D. Liu, G. Ernst, T. Murray, B. I. P. Rubinstein: LEGION: Best-First Concolic Testing, ASE 2020.
• M. Wang, J. Liang, Ch. Zhou, Z. Wu, X. Xu, and Y. Jiang: Odin: On-Demand Instrumentation with On-the-Fly Recompilation, PLDI 2022.
  
  

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:

• 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.
• The Calculus of Computation
• Counterexample-Guided Abstraction Refinement