Máte zapnutý náhled celé osnovy, zpět na běžné zobrazení.
Načítání a prohlížení osnovy může být v závislosti na množství obsahu pomalejší.
Kapitola obsahuje:
1
Studijní text
Programme
- 21. 2. 2014 - Arrangements
- 28. 2. 2014 - Marek Trtík - Passing Info Between Verifiers
- 7. 3. 2014 - Petr Bauch - Model Checking Parallel Programs With Input
- 14. 3. 2014 - Karolína Malá - Antichains and Compositional Algorithms for LTL Synthesis, Formal Methods in System Design 2011 (by E. Filiot, N. Jin, and J.-F. Raskin) [slides]
- 21. 3. 2014 - Martin Jonáš - Decidable logics combining heap structures and data, POPL 2011 (by P. Madhusudan, G. Parlato, and X. Qiu)
- 28. 3. 2014 - Tomáš Brukner - Automatic Abstraction in SMT-Based Unbounded Software Model Checking, CAV 2013 (by A. Komuravelli, A. Gurfinkel, S. Chaki, and E. M. Clarke)
- 4. 4. 2014 - Jan Dupal - Bias-variance tradeoffs in program analysis, POPL 2014 (by R. Sharma, A. V. Nori, A. Aiken)
- 11. 4. 2014 - cancelled (no speaker)
- 18. 4. 2014 - cancelled (no speaker)
- 25. 4. 2014 - Viktor Toman - Multi-solver Support in Symbolic Execution, CAV 2013 (by H. Palikareva and C. Cadar)
- 2. 5. 2014 - (day after bank holiday)
- 9. 5. 2014 - (day after bank holiday)
- 16. 5. 2014 - Fanda Blahoudek - TBA
Papers to present:
-
V. D'Silva, L. Haller, and D. Kroening: Abstract satisfaction, POPL 2014.
-
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.
- B. Elkarablieh, P. Godefroid, and M. Y. Levin: Precise pointer reasoning for dynamic test generation, ISSTA 2009.
- 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.
- 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