• 22. 2. 2013 - Arrangements
• 1. 3. 2013 - Marek Trtík - Alternate and Learn: Finding witnesses without looking all over.
• 8. 3. 2013 - Petr Bauch - Control Explicit---Data Symbolic Model Checking: An Introduction (joint work with J. Barnat)

A comprehensive verification of parallel software imposes three crucial requirements on the procedure that implements it. Apart from accepting real code as program input and temporal formulae as specification input, the verification should be exhaustive, with respect to both control and data flows. This paper is concerned with the third requirement, using explicit model checking to handle the control and symbolic set representations to handle the data. The combination of explicit and symbolic approaches is first investigated theoretically and we report the requirements on the symbolic representation and the changes to the model checking process the combination entails. The feasibility and efficiency of the combination is demonstrated on two case studies and we report a marked improvement in scalability in the Simulink case study against previous solutions. The results described in this paper show the potential to meet all three requirements for automatic verification in a single procedure combining explicit model checking with symbolic set representations.

• 15. 3. 2013 - Viktor Toman - KLEE
• 22. 3. 2013 - cancelled (ETAPS 2013)
• 29. 3. 2013 - cancelled (Easter)
• 5. 4. 2013 - Tomáš Brukner - Method for symbolic computation of abstract operations.
• 12. 4. 2013 - no speaker
• 19. 4. 2013 - Fanda Blahoudek - Determinization of May/Must Automata

Translation of LTL to deterministic omega-automata is needed in model checking
of probabilistic systems or in LTL synthesis. May/Must alternating automata
(MMAA) is a subclass of very weak alternating automata that corresponds to the
fragment of LTL which uses only strict Future and strict Globally as temporal
operators. We show a doubly exponential determinization procedure for MMAA
which translate them into transition-based generalized Rabin automata (TGDRA).
TGDRA can be further translated into standard Rabin automata.

• 26. 4. 2013 - no speaker
• 3. 5. 2013 - no speaker
• 10. 5. 2013 - Pavel Čadek - Loop bound analysis: An overview
• 17. 5. 2013 - cancelled (talk of Martin Kučera moved to the next semester)

Papers to present:

• B. Elkarablieh, P. Godefroid, and M. Y. Levin: Precise pointer reasoning for dynamic test generation, ISSTA 2009.

• P. Madhusudan, G. Parlato, and X. Qiu: Decidable logics combining heap structures and data, POPL 2011.

• D. Vanoverberghe, N. Tillmann, and F. Piessens: Test Input Generation for Programs with Pointers, TACAS 2000.

• S. Gulwani, K. K. Mehra, and T. Chilimbi: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity, POPL 2009.

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

• K. Dudka, P. Peringer, and T. Vojnar: Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic, CAV 2011.
• K. J. Ottenstein and L. M. Ottenstein: The Program Dependence Graph in a Software Development Environment, ACM SIGPLAN Notices, 1984.
• D. Distefano: Attacking Large Industrial Code with Bi-Abductive Inference, FMICS 2009.
• 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