• 22. 2 . 2019 - Arrangements
  
• 1. 3. 2019 - Cancelled (no speaker)
  
• 8. 3. 2019 - Cancelled (DUVOD)
  
• 15. 3. 2019 - Cancelled (DUVOD)
  
• 22. 3. 2019 - Cancelled
  
• 29. 3. 2019 - Vláďa Štill - H. Günther, A. Laarman, A. Sokolova, and G. Weissenbacher: Dynamic Reductions for Model Checking Concurrent Software, VMCAI 2017.
• 5. 4. 2019 (at 10:30, FIT VUT, room E104) - prof. Marta Kwiatkowska - Safety verification for deep neural networks with provable guarantees
  
  Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. This lecture will describe progress with developing automated verification and testing techniques for deep neural networks to ensure safety and security of their classification decisions with respect to input manipulations. The techniques exploit Lipschitz continuity of the networks and aim to approximate, for a given set of inputs, the reachable set of network outputs in terms of lower and upper bounds, in anytime manner, with provable guarantees. We develop novel algorithms based on feature-guided search, games and global optimisation, and evaluate them on state-of-the-art networks. We also develop foundations for probabilistic safety verification for Gaussian processes, with application to neural networks.


• 12. 4. 2019 - Juraj Major - D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata, GandALF 2017.
• 26. 4. 2019 - Adam Fiedler - J. D. Allred and U. Ultes-Nitsche: A Simple and Optimal Complementation Algorithm for Büchi Automata, LICS 2018.
• 3. 5. 2019 - Cancelled (ATVA deadline approaching and no speaker)
  
• 10. 5. 2019 - Cancelled (no speaker)
  
• 17. 5. 2019 - Marek Chalupa - IC3/PDR introduction based on:
  • A. R. Bradley: SAT-based model checking without unrolling, VMCAI 2011.
  • N. Een, A. Mishchenko, and R. Brayton: Efficient implementation of property directed reachability, FMCAD 2011.
  • F. Somenzi and A. R. Bradley: IC3: Where Monolithic and Incremental Meet, FMCAD 2011.
  • A. R. Bradley: Understanding IC3, SAT 2012.
    
• 23. 5. 2019 - Martin Jonáš - On the complexity of the quantified bit-vector arithmetic with binary encoding

Papers on omega-automata:

• J. Espara, J. Křetínský, S. Sickert: One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata, LICS 2018.
• Y. Li, Y.-F. Chen, L. Zhang, and D. Liu: A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees, TACAS 2017.
• 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.
• J. Křetínský, T. Meggendorfer, C. Waldmann, and M. Weininger: Index Appearance Record for Transforming Rabin Automata into Parity Automata, TACAS 2017.

Papers on SAT/SMT solving:

• 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

Papers on slicing:

• S. Horwitz and T. W. Reps: The Use of Program Dependence Graphs in Software Engineering, ICSE 1992.
• D. W. Binkley and K. B. Gallagher: Program Slicing, Advances in Computers 43, 1996.
• 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:

• K. L. McMillan: Lazy Abstraction with Interpolants, CAV 2006.
• B. Wachter, D. Kroening, and J. Ouaknine: Verifying multi-threaded software with impact, FMCAD 2013.

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. Kroening, M. Lewis, and G. Weissenbacher: Under-Approximating Loops in C Programs for Fast Counterexample Detection, CAV 2013.
• 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