• 22. 9. 2023 - Arrangements (Jan not present)
  
• 29. 9. 2023 - Tereza Schwarzová - T. Schwarzová, J. Strejček, and J. Major: Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving, SAT 2023.
  
• 6. 10. 2023 - David Dokoupil - Simple Complementation of Generalized Büchi Automata
  
• 13. 10. 2023 - cancelled (no speaker)
  
• 20. 10. 2023 - Tomáš Krchňák - P. Yao, Q. Shi, H. Huang, and C. Zhang: Fast bit-vector satisfiability, ISSTA 2020.
  
• 27. 10. 2023 - Tomáš Krchňák - S. Graham-Lengrand, D. Jovanovic, and B. Dutertre: Solving Bitvectors with MCSAT: Explanations from Bits and Pieces, IJCAR 2020.
  
• 3. 11. 2023 - Robert Konicar - J. Tafese, A. Gurfinkel, and I. Garcia-Contreras: Btor2MLIR: A Format for Hardware Verification. FMCAD 2023.
• 10. 11. 2023 - Richard Jandušík - Shaowei Cai, Xindi Zhang, Mathias Fleury, and Armin Biere: Better Decision Heuristics in CDCL through Local Search and Target Phases, JAIR 74 (2022).
• 24. 11. 2023 - cancelled
  
• 30. 11. 2023 at 15:00 (moved from 1. 12. 2023) - cancelled 
  
• 14. 12. 2023 at 16:00 (moved from 8. 12. 2023) in C525 - Paulína Ayaziová - Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, and Philipp Rümmer: Automatic Program Instrumentation for Automatic Verification. CAV 2023.
• 15. 12. 2023 -  Suyash Shandilya - Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, Klaus Wehrle: Symbolic Partial-Order Execution for Testing Multi-Threaded Programs, CAV 2020.
  

Suggested papers for presentation

Papers on automata (mostly omega-automata):

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

• Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken: Induction duality: primal-dual search for invariants. POPL 2022.
• Alessandro Cimatti, Alberto Griggio, and Gianluca Redondi: Verification of SMT Systems with Quantifiers. ATVA 2022
• Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta: Infinite-state invariant checking with IC3 and predicate abstraction. FMSD 49(3) (2016).
  (This is an extended version of TACAS 2014 paper IC3 Modulo Theories via Implicit Predicate Abstraction)
• Arie Gurfinkel, Anton Belov, and João Marques-Silva: Synthesizing Safe Bit-Precise Invariants. TACAS 2014
• Matthias Güdemann and Klaus Riedl: Level-Up - From Bits to Words. SBMF 2022
• Aman Goel and Karem A. Sakallah: Model Checking of Verilog RTL Using IC3 with Syntax-Guided Abstraction. NFM 2019
• Isabel Garcia-Contreras, Arie Gurfinkel, and Jorge A. Navas: Efficient Modular SMT-Based Model Checking of Pointer Programs. SAS 2022
• Martin Blicha, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina: Transition Power Abstractions for Deep Counterexample Detection. TACAS 2022
  
• 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
  
• 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.
  
• 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.
• R. Ji and M. Xu: Finding Specification Blind Spots via Fuzz Testing, SP 2023.
  

Papers on SAT/SMT solving:

• Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier: QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. CADE 2023.
  
• Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, and Arie Gurfinkel: Fast Approximations of Quantifier Elimination. CAV 2023.
  
• Haokun Li, Bican Xia, and Tianqi Zhao: Local Search for Solving Satisfiability of Polynomial Formulas. CAV 2023.
  
• Kevin Lotz, Amit Goel, Bruno Dutertre, Benjamin Kiesl-Reiter, Soonho Kong, Rupak Majumdar, and Dirk Nowotka:
  Solving String Constraints Using SAT. CAV 2023.
  
• Eszter Couillard, Philipp Czerner, Javier Esparza, and Rupak Majumdar: Making IP=PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms, CAV 2023.
• Dror Fried, Alexander Nadel, and Yogev Shalmon: AllSAT for Combinational Circuits. SAT 2023.
• Gabriele Masina, Giuseppe Spallitta, and Roberto Sebastiani: On CNF Conversion for Disjoint SAT Enumeration. SAT 2023.
• Nikolaj Bjørner and Katalin Fazekas: On Incremental Pre-processing for SMT. CADE 2023.
  
• Masood Feyzbakhsh Rankooh and Jussi Rintanen: Propositional Encodings of Acyclicity and Reachability by Using Vertex Elimination, AAAI 2022.
• Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang: Fast bit-vector satisfiability. ISSTA 2020
• 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

SMT solving of arrays:

• Jürgen Christ and Jochen Hoenicke: Weakly Equivalent Arrays. FroCos 2015
  
• Aaron R. Bradley, Zohar Manna, and Henny B. Sipma: What's Decidable About Arrays? VMCAI 2006
  

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