IA072 Seminar on Verification - jaro 2021
Programme
The seminar will be held in person (at least in September).
The current schedule follows (and it will be regularly updated):
- 17. 9. 2021 - Arrangement
- 24. 9. 2021 - cancelled (no speaker)
- 1. 10. 2021 - cancelled (no speaker)
- 8. 10. 2021 - cancelled (no speaker)
- 15. 10. 2021 - Ján Jančár - Verification of functional correctness in cryptography
- 22. 10. 2021 - Jan Tušil - X. Chen, D. Lucanu, and G. Roşu: Matching logic explained, JLAMP 120, 2021.
29. 10. 2021- [rescheduled to 25. 10. 2021 at 19:00 in C408, presence is voluntary] - Marek Chalupa - Formal analysis of an audiovisual work- 5. 11. 2021 - Tereza Schwarzová - A. Casares, T. Colcombet, and N. Fijalkow: Optimal Transformations of Games and Automata Using Muller Conditions, ICALP 2021.
- 12. 11. 2021 - Marek Chalupa - Backward Symbolic Execution with Loop Folding, SAS 2021.
- 19. 11. 2021 - Pavel Šímovec - Y. Smaragdakis, N. Grech, S. Lagouvardos, K. Triantafyllou, and I. Tsatiris: Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts, OOPSLA 2021. [slides]
- 26. 11. 2021 - Vincent Mihalkovič - F. Frohn: Calculus for Modular Loop Acceleration, TACAS 2020. [slides]
- 3. 12. 2021 - cancelled (no speaker)
- 10. 12. 2021 - Adam Fiedler - A. Bauer: Five Stages of Accepting Constructive Mathematics, Bull. Amer. Math. Soc. 54, 2017.
Suggested papers for presentation
Papers on automata (mostly omega-automata):
- C. Stanford, M. Veanes, and N. Bjørner: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints, PLDI 2021.
- 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:
- 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:
- Gidon Ernst: A Complete Approach to Loop Verification with Invariants and Summaries, VMCAI 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
- 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.
- 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
Následující