Příští seminář:
| Přednáší: | Lukáš Charvát |
|---|---|
| Téma: | SAT-Based Model Checking Without Unrolling |
| Místnost: | A218 |
| Datum a čas: | 14. 2. 2012, 10:00 |
| Reference: |
A. Bradley: SAT-Based Model Checking Without Unrolling |
Historie seminářů:
| Datum: | 13. 12. 2011 |
|---|---|
| Přednášel: | Jan Strejček a kol. (FI MU) |
| Téma: | Combining METAL with Symbolic Execution |
| Reference: |
| Datum: | 29. 11. 2011 |
|---|---|
| Přednášel: | Marcela Šimková (FIT VUT) |
| Téma: | HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware |
| Reference: |
M. Simkova, O. Lengal, M. Kajan: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware HAVEN |
| Datum: | 19. 9. 2011 |
|---|---|
| Přednášel: | Zdeněk Letko |
| Téma: | Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software |
| Reference: |
| Datum: | 19. 9. 2011 |
|---|---|
| Přednášel: | Vendula Hrubá |
| Téma: | DBMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking |
| Reference: |
| Datum: | 11. 7. 2011 |
|---|---|
| Přednášel: | Kamil Dudka |
| Téma: | Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic |
| Reference: |
| Datum: | 11. 7. 2011 |
|---|---|
| Přednášel: | Jiří Šimáček |
| Téma: | Forest Automata for Verification of Heap Manipulation |
| Reference: |
| Datum: | 11. 5. 2011 |
|---|---|
| Přednášel: | Zdeněk Letko |
| Téma: | Reachability Testing of Concurrent Programs |
| Reference: |
Yu Lei, Richard H. Carver: Reachability Testing of Concurrent Programs |
| Datum: | 27. 4. 2011 |
|---|---|
| Přednášel: | Filip Konečný |
| Téma: | Loop Invariant Synthesis in a Combined Domain |
| Reference: |
Shengchao Qin, Guanhua He, Chenguang Luo and Wei-Ngan Chin: Loop Invariant Synthesis in a Combined Domain |
| Datum: | 23. 3. 2011 |
|---|---|
| Přednášel: | Ondřej Lengál |
| Téma: | Abstract interpretation |
| Reference: |
O. Lengál, T. Vojnar: Abstract interpretation (slides) |
| Datum: | 23. 2. 2011 |
|---|---|
| Přednášel: | Petr Müller |
| Téma: | Compositional Shape Analysis by Means of Bi-Abduction |
| Reference: |
Cristiano Calcagno, Dino Distefano, Peter O'Hearn, Hongseok Yang: Compositional shape analysis by means of bi-abduction Dino Distefano: Attacking Large Industrial Code with Bi-abductive Inference |
| Datum: | 16. 2. 2011 |
|---|---|
| Přednášel: | Miloš Minařík (FIT) |
| Téma: | Genetic programming and model checking |
| Reference: |
Katz, G., Peled, D.: Genetic programming and model checking: Synthesizing new mutual exclusion algorithms Model checking-based genetic programming with an application to mutual exclusion Synthesizing solutions to the leader election problem using model checking and genetic programming Code mutation in verification and automatic code correction MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming |
| Datum: | 15. 12. 2010 |
|---|---|
| Přednášel: | Michal Prívozník (FIT) |
| Téma: | Abstraction Learning |
| Reference: |
Joxan Jaffar, Jorge Navas, and Andrew E. Santosa: Abstraction Learning |
| Datum: | 8. 12. 2010 |
|---|---|
| Přednášel: | Pietro Braione (LTA UNIMIB, Milano) |
| Téma: | Structural Coverage of Feasible Code |
| Reference: |
Mauro Baluda, Pietro Braione, Giovanni Denaro, and Mauro Pezze: Structural Coverage of Feasible Code |
| Datum: | 1. 12. 2010 |
|---|---|
| Přednášel: | Kamil Dudka |
| Téma: | List Segment Auto-Discovery in a Symbolic Heap |
| Reference: |
Prezentace |
| Datum: | 10. 11. 2010 |
|---|---|
| Přednášel: | Peter Habermehl (Liafa, Paris) |
| Téma: | On the Use of Non-deterministic Automata for Presburger Arithmetic Systems |
| Reference: |
Antoine Durand-Gasselin and Peter Habermehl: On the Use of Non-deterministic Automata for Presburger Arithmetic |
| Datum: | 27. 10. 2010 |
|---|---|
| Přednášel: | Nikola Beneš (MU, Brno) |
| Téma: | On Verification of Disjunctive Modal Transition Systems |
| Reference: |
Abstrakt |
| Datum: | 21. 10. 2010 |
|---|---|
| Přednášel: | Antti Valmari (TUT, Tampere) |
| Téma: | Can Stubborn Sets Be Optimal? |
| Reference: |
Antti Valmari, Henri Hansen: Can Stubborn Sets Be Optimal? |
| Datum: | 13. 10. 2010 |
|---|---|
| Přednášel: | Marek Trtík (MU, Brno) |
| Téma: | Efficient Loop Navigation for Symbolic Execution |
| Reference: |
Abstrakt |
| Datum: | 6. 10. 2010 |
|---|---|
| Přednášel: | Zdeněk Letko |
| Téma: | Precise Data Race Detection in a Relaxed Memory Model using Model Checking |
| Reference: |
KyungHee Kim, Tuba Yavuz-Kahveci, Beverly Sanders: Precise Data Race Detection in a Relaxed Memory Model using Model Checking |
| Datum: | 29. 9. 2010 |
|---|---|
| Přednášel: | Filip Konečný |
| Téma: | Relational Analysis of Non-deterministic Integer Programs |
| Reference: |
Marius Bozga, Radu Iosif, Filip Konečný: Fast Acceleration of Ultimately Periodic Relations |
| Datum: | 17. 3. 2010 |
|---|---|
| Přednášel: | Kamil Dudka |
| Téma: | Towards a Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic |
| Reference: | Prezentace z UITS semináře |
| Datum: | 24. 2. 2010 |
|---|---|
| Přednášel: | Radek Pyšný (FIT, Brno) |
| Téma: | Verifikační nástroj od Microsoftu: Static Driver Verifier |
| Reference: | Static Driver Verifier |
| Datum: | 17. 2. 2010 |
|---|---|
| Přednášel: | Filip Konečný |
| Téma: | Fast Acceleration of Ultimately Periodic Relations (pokračování) |
| Reference: |
Marius Bozga, Radu Iosif, Filip Konečný: Fast Acceleration of Ultimately Periodic Relations |
| Datum: | 12. 2. 2010 |
|---|---|
| Přednášel: | Filip Konečný |
| Téma: | Fast Acceleration of Ultimately Periodic Relations |
| Reference: |
Marius Bozga, Radu Iosif, Filip Konečný: Fast Acceleration of Ultimately Periodic Relations |
| Datum: | 5. 2. 2010 |
|---|---|
| Přednášel: | Kamil Dudka |
| Téma: | A Polynomial Time Algorithm for Graph Isomorphism |
| Reference: |
A. Dharwadker, J.-T. Tevet: The Graph Isomorphism Algorithm |
| Datum: | 11. 12. 2009 |
|---|---|
| Přednášel: | Lukáš Holík |
| Téma: | Mediating for Reduction |
| Reference: |
P.A. Abdulla, Y.-F. Chen, L. Holik, and T. Vojnar: Mediating for Reduction (On Minimizing Alternating Büchi Automata) |
| Datum: | 27. 11. 2009 |
|---|---|
| Přednášel: | Milan Češka (MU, Brno) |
| Téma: | Probabilistic LTL Model Checking |
| Reference: |
J. Barnat, L. Brim, I. Černá, M. Češka, J. Tůmová: ProbDiVinE-MC: Multi-Core LTL Model Checker for Probabilistic Systems J. Barnat, L. Brim, I. Černá, M. Češka, J. Tůmová: Local Quantitative LTL Model Checking |
| Datum: | 9. 10. 2009 |
|---|---|
| Přednášel: | Marek Gach |
| Téma: | Návrh a implementace nástroje pro hierarchickou grafickou specifikaci systémů pracujících v reálném čase |
| Reference: |
M. Gach: Návrh a implementace nástroje pro hierarchickou grafickou specifikaci systémů pracujících v reálném čase |
| Datum: | 2. 10. 2009 |
|---|---|
| Přednášel: | Jan Fiedor |
| Téma: | Návrh a implementace nástroje pro formální verifikaci systémů specifikovaných jazykem RT logiky |
| Reference: |
J. Fiedor: Návrh a implementace nástroje pro formální verifikaci systémů specifikovaných jazykem RT logiky |
| Datum: | 11. 9. 2009 |
|---|---|
| Přednášel: | Adam Rogalewicz |
| Téma: | Automata based termination proving |
| Reference: |
R. Iosif, A. Rogalewicz: Automata based termination proving |
| Datum: | 12. 6. 2009 |
|---|---|
| Přednášel: | Peter Habermel (Liafa, Paris) |
| Téma: | Angluin-Style Learning of NFA |
| Reference: |
B. Bollig, P. Habermehl, C. Kern, M. Leucker: Angluin-Style Learning of NFA D. Angluin: Learning Regular Sets From Queries and Counterexamples |
| Datum: | 29. 5. a 5. 6. 2009 |
|---|---|
| Přednášel: | Jiří Šimáček |
| Téma: | Separační logika |
| Reference: |
J. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures |
| Datum: | 17. 4. 2009 |
|---|---|
| Přednášel: | Zdeněk Letko |
| Téma: | Statická analýza pro výpočet May Happen in Parallel (MHP) |
| Reference: |
G. Naumovich, G.S. Avrunin, L.A. Clarke: An Efficient Algorithm for Computing MHP Information for Concurrent Java Programs R. Barik: Efficient Computation of May-Happen-in-Parallel Information for Concurrent Java Programs |
| Datum: | 10. 4. 2009 |
|---|---|
| Přednášel: | Vendula Hrubá |
| Téma: | Základy bezzámkové synchronizace |
| Reference: |
L. Lamport: Concurrent Reading and Writing |
| Datum: | 27. 2. 2009 |
|---|---|
| Přednášel: | Filip Konečný |
| Téma: | Čítačové automaty - pokračování |
| Reference: |
M. Bozga, P. Habermehl, R. Iosif, F. Konecny, T. Vojnar: Automatic Verification of Integer Array Programs A. Miné: A New Numerical Abstract Domain Based on Difference-Bound Matrices |
| Datum: | 13. 2. 2009 |
|---|---|
| Přednášel: | Lukáš Holík |
| Téma: | Abstraktní interpretace - pokračování |
| Reference: |
M. Erne, J. Koslowski, A. Melton, G. E. Strecker.: A Primer on Galois Connestions P. Cousot and R. Cousot.: Basic Concepts of Abstract Interpretation P. Cousot: A Tutorial on Abstract Interpretation |
| Datum: | 6. 2. 2009 |
|---|---|
| Přednášel: | Lukáš Holík |
| Téma: | Abstraktní interpretace - úvod |
| Reference: | viz. Abstraktní interpretace - pokračování |
| Datum: | 16. 1. 2009 |
|---|---|
| Přednášel: | Adam Rogalewicz |
| Téma: | Použití ARTMC pro programy s ukazateli (3. díl úspěšného seriálu) |
| Reference: | tbd |
| Datum: | 12. 12. 2008 |
|---|---|
| Přednášel: | Adam Rogalewicz |
| Téma: | Verifikace dynamických datových struktur pomocí ARTMC (2. díl úspěšného seriálu) |
| Reference: | tbd |
| Datum: | 5. 12. 2008 |
|---|---|
| Přednášel: | Zdeněk Letko |
| Téma: | Goldilocks - efektivní počítání Happens-before pomocí množin zámků |
| Reference: |
Elmas T., Quadeer S., Tasiran S.: Goldilocks: a race and transaction-aware java runtime |
| Datum: | 21. 11. 2008 |
|---|---|
| Přednášel: | Filip Konečný |
| Téma: | Čítačové automaty |
| Reference: | tbd |
| Datum: | 7. 11. 2008 |
|---|---|
| Přednášel: | Petr Muller |
| Téma: | tbd |
| Reference: | tbd |
| Datum: | 31. 10. 2008 |
|---|---|
| Přednášel: | Jiří Šimáček |
| Téma: | Verifikace paralelních programů s ukazatali pomocí ARTMC |
| Reference: | tbd |
| Datum: | 24. 10. 2008 |
|---|---|
| Přednášel: | Vendula Hrubá |
| Téma: | Partial Order Redukce a prohledávání stavového prostoru |
| Reference: | Hrubá V.: Bounded model checking v nástroji Java PathFinder |
| Datum: | 17. 10. 2008 |
|---|---|
| Přednášel: | Lukáš Holík |
| Téma: | Využití simulace a bisimulace v analýze programů s ukazateli |
| Reference: |
| Datum: | 10. 10. 2008 |
|---|---|
| Přednášel: | Zdeněk Letko |
| Téma: | Existující přístupy k dynamické detekci data race a porušení atomicity |
| Reference: | Letko Z.: Dynamic Data Race Detection and Healing in Java |
