Upcoming seminar talks:
Speaker: | Jan Kofroň |
---|---|
Topic: | Dynamic Predicate Abstraction |
Room: | A218 |
Date and time: | 29. 04. 2014, 13:00 |
References: |
Abstract |
Speaker: | Jan Kofroň |
---|---|
Topic: | Weverca - web verification for PHP |
Room: | A218 |
Date and time: | 29. 04. 2014, 13:00 |
References: |
Abstract |
History of seminar talks:
Date: | 17. 1. 2014 |
---|---|
Speaker: | Florian Zuleger |
Topic: | A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis |
References: |
Abstract |
Date: | 9. 1. 2014 |
---|---|
Speaker: | Shmuel Ur |
Topic: | Shift-left Methodology and Testing Lessons |
References: |
Date: | 13. 06. 2013 |
---|---|
Speaker: | Ondřej Lengál |
Topic: | Fully Automated Shape Analysis Based on Forest Automata |
References: |
Abstract Preliminary version of the paper |
Date: | 11. 06. 2013 |
---|---|
Speaker: | Kamil Dudka |
Topic: | Byte-Precise Verification of Low-Level List Manipulation |
References: |
Abstract Technical report |
Date: | 23. 05. 2013 |
---|---|
Speaker: | Lukáš Holík |
Topic: | An Integrated Specification and Verification Technique for Highly Concurrent Data Structures |
References: | Abstract |
Date: | 10. 05. 2013 |
---|---|
Speaker: | Lukáš Holík |
Topic: | Various Approaches to Coverability |
References: |
Date: | 12. 03. 2013 |
---|---|
Speaker: | Adam Rogalewicz |
Topic: | The Tree Width of Separation Logic with Recursive Definitions |
References: | Abstract |
2012
Date: | 11. 12. 2012 |
---|---|
Speaker: | Antonio Carzaniga (USI) |
Topic: | SHADE: a Self HeAling DEsign methodology |
References: | Project page, Abstract |
Date: | 7. 12. 2012 |
---|---|
Speaker: | Lukáš Charvát |
Topic: | Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description |
References: | Abstrakt |
Date: | 9. 11. 2012 |
---|---|
Speaker: | Jana Tůmová (FI MUNI) |
Topic: | Least-violating Robot Path Planning with LTL Specifications |
References: | Abstrakt |
Date: | 2. 11. 2012 |
---|---|
Speaker: | Marek Trtík (FI MUNI) |
Topic: | Compact Symbolic Execution |
References: | Abstrakt |
Date: | 31. 10. 2012 |
---|---|
Speaker: | David Monniaux |
Topic: | Distinguishing paths (for fun and profit) |
References: | Abstrakt |
Date: | 24. 10. 2012 |
---|---|
Speaker: | Jiří Šimáček |
Topic: | Harnessing Forest Automata for Verification of Heap Manipulating Programs |
References: | Abstrakt |
Date: | 21. 9. 2012 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Testing of Concurrent Programs Using Genetic Algorithms |
References: | V. Hruba, B. Krena, Z. Letko, S. Ur, and T. Vojnar. Testing of Concurrent Programs Using Genetic Algorithms |
Date: | 21. 9. 2012 |
---|---|
Speaker: | Jan Fiedor |
Topic: | ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level |
References: | J. Fiedor and T. Vojnar. ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level |
Date: | 15. 5. 2012 |
---|---|
Speaker: | Tomáš Masopust (ÚM, Akademie věd ČR) |
Topic: | Introduction to Supervisory Control of Discrete-Event Systems and a Coordination Extension |
References: | Decentralized and coordination supervisory control project |
Date: | 27. 3. 2012 |
---|---|
Speaker: | Stanislav Bohm (VSB, Ostrava) |
Topic: | Kaira: Tvorba paralelnich aplikaci s vyuzitim Petriho siti |
References: |
Date: | 20. 3. 2012 |
---|---|
Speaker: | Trinh Cong Quy (Uppsala University, Sweden) |
Topic: | Formal Verification of Skiplist Algorithms |
References: |
Abstract Formal Verification of Skiplist Algorithms |
Date: | 6. 3. 2012 |
---|---|
Speaker: | Kamil Dudka |
Topic: | Common Errors in C/C++ Code and Static Analysis |
References: | Common Errors in C/C++ Code and Static Analysis |
Date: | 14. 2. 2012 |
---|---|
Speaker: | Lukáš Charvát |
Topic: | SAT-Based Model Checking Without Unrolling |
References: |
A. Bradley: SAT-Based Model Checking Without Unrolling |
2011
Date: | 13. 12. 2011 |
---|---|
Speaker: | Jan Strejček a kol. (FI MU) |
Topic: | Combining METAL with Symbolic Execution |
References: |
Date: | 29. 11. 2011 |
---|---|
Speaker: | Marcela Šimková (FIT VUT) |
Topic: | HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware |
References: |
M. Simkova, O. Lengal, M. Kajan: HAVEN: An Open Framework for FPGA-Accelerated Functional Verification of Hardware HAVEN |
Date: | 19. 9. 2011 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Coverage Metrics for Saturation-based and Search-based Testing of Concurrent Software |
References: |
Date: | 19. 9. 2011 |
---|---|
Speaker: | Vendula Hrubá |
Topic: | DBMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking |
References: |
Date: | 11. 7. 2011 |
---|---|
Speaker: | Kamil Dudka |
Topic: | Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic |
References: |
Date: | 11. 7. 2011 |
---|---|
Speaker: | Jiří Šimáček |
Topic: | Forest Automata for Verification of Heap Manipulation |
References: |
Date: | 11. 5. 2011 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Reachability Testing of Concurrent Programs |
References: |
Yu Lei, Richard H. Carver: Reachability Testing of Concurrent Programs |
Date: | 27. 4. 2011 |
---|---|
Speaker: | Filip Konečný |
Topic: | Loop Invariant Synthesis in a Combined Domain |
References: |
Shengchao Qin, Guanhua He, Chenguang Luo and Wei-Ngan Chin: Loop Invariant Synthesis in a Combined Domain |
Date: | 23. 3. 2011 |
---|---|
Speaker: | Ondřej Lengál |
Topic: | Abstract interpretation |
References: |
O. Lengál, T. Vojnar: Abstract interpretation (slides) |
Date: | 23. 2. 2011 |
---|---|
Speaker: | Petr Müller |
Topic: | Compositional Shape Analysis by Means of Bi-Abduction |
References: |
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 |
Date: | 16. 2. 2011 |
---|---|
Speaker: | Miloš Minařík (FIT) |
Topic: | Genetic programming and model checking |
References: |
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 |
2010
Date: | 15. 12. 2010 |
---|---|
Speaker: | Michal Prívozník (FIT) |
Topic: | Abstraction Learning |
References: |
Joxan Jaffar, Jorge Navas, and Andrew E. Santosa: Abstraction Learning |
Date: | 8. 12. 2010 |
---|---|
Speaker: | Pietro Braione (LTA UNIMIB, Milano) |
Topic: | Structural Coverage of Feasible Code |
References: |
Mauro Baluda, Pietro Braione, Giovanni Denaro, and Mauro Pezze: Structural Coverage of Feasible Code |
Date: | 1. 12. 2010 |
---|---|
Speaker: | Kamil Dudka |
Topic: | List Segment Auto-Discovery in a Symbolic Heap |
References: |
Prezentace |
Date: | 10. 11. 2010 |
---|---|
Speaker: | Peter Habermehl (Liafa, Paris) |
Topic: | On the Use of Non-deterministic Automata for Presburger Arithmetic Systems |
References: |
Antoine Durand-Gasselin and Peter Habermehl: On the Use of Non-deterministic Automata for Presburger Arithmetic |
Date: | 27. 10. 2010 |
---|---|
Speaker: | Nikola Beneš (MU, Brno) |
Topic: | On Verification of Disjunctive Modal Transition Systems |
References: |
Abstrakt |
Date: | 21. 10. 2010 |
---|---|
Speaker: | Antti Valmari (TUT, Tampere) |
Topic: | Can Stubborn Sets Be Optimal? |
References: |
Antti Valmari, Henri Hansen: Can Stubborn Sets Be Optimal? |
Date: | 13. 10. 2010 |
---|---|
Speaker: | Marek Trtík (MU, Brno) |
Topic: | Efficient Loop Navigation for Symbolic Execution |
References: |
Abstrakt |
Date: | 6. 10. 2010 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Precise Data Race Detection in a Relaxed Memory Model using Model Checking |
References: |
KyungHee Kim, Tuba Yavuz-Kahveci, Beverly Sanders: Precise Data Race Detection in a Relaxed Memory Model using Model Checking |
Date: | 29. 9. 2010 |
---|---|
Speaker: | Filip Konečný |
Topic: | Relational Analysis of Non-deterministic Integer Programs |
References: |
Marius Bozga, Radu Iosif, Filip Konečný: Fast Acceleration of Ultimately Periodic Relations |
Date: | 17. 3. 2010 |
---|---|
Speaker: | Kamil Dudka |
Topic: | Towards a Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic |
References: | Prezentace z UITS semináře |
Date: | 24. 2. 2010 |
---|---|
Speaker: | Radek Pyšný (FIT, Brno) |
Topic: | Verifikační nástroj od Microsoftu: Static Driver Verifier |
References: | Static Driver Verifier |
Date: | 17. 2. 2010 |
---|---|
Speaker: | Filip Konečný |
Topic: | Fast Acceleration of Ultimately Periodic Relations (pokračování) |
References: |
Marius Bozga, Radu Iosif, Filip Konečný: Fast Acceleration of Ultimately Periodic Relations |
Date: | 12. 2. 2010 |
---|---|
Speaker: | Filip Konečný |
Topic: | Fast Acceleration of Ultimately Periodic Relations |
References: |
Marius Bozga, Radu Iosif, Filip Konečný: Fast Acceleration of Ultimately Periodic Relations |
Date: | 5. 2. 2010 |
---|---|
Speaker: | Kamil Dudka |
Topic: | A Polynomial Time Algorithm for Graph Isomorphism |
References: |
A. Dharwadker, J.-T. Tevet: The Graph Isomorphism Algorithm |
2009
Date: | 11. 12. 2009 |
---|---|
Speaker: | Lukáš Holík |
Topic: | Mediating for Reduction |
References: |
P.A. Abdulla, Y.-F. Chen, L. Holik, and T. Vojnar: Mediating for Reduction (On Minimizing Alternating Büchi Automata) |
Date: | 27. 11. 2009 |
---|---|
Speaker: | Milan Češka (MU, Brno) |
Topic: | Probabilistic LTL Model Checking |
References: |
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 |
Date: | 9. 10. 2009 |
---|---|
Speaker: | Marek Gach |
Topic: | Návrh a implementace nástroje pro hierarchickou grafickou specifikaci systémů pracujících v reálném čase |
References: |
M. Gach: Návrh a implementace nástroje pro hierarchickou grafickou specifikaci systémů pracujících v reálném čase |
Date: | 2. 10. 2009 |
---|---|
Speaker: | Jan Fiedor |
Topic: | Návrh a implementace nástroje pro formální verifikaci systémů specifikovaných jazykem RT logiky |
References: |
J. Fiedor: Návrh a implementace nástroje pro formální verifikaci systémů specifikovaných jazykem RT logiky |
Date: | 11. 9. 2009 |
---|---|
Speaker: | Adam Rogalewicz |
Topic: | Automata based termination proving |
References: |
R. Iosif, A. Rogalewicz: Automata based termination proving |
Date: | 12. 6. 2009 |
---|---|
Speaker: | Peter Habermel (Liafa, Paris) |
Topic: | Angluin-Style Learning of NFA |
References: |
B. Bollig, P. Habermehl, C. Kern, M. Leucker: Angluin-Style Learning of NFA D. Angluin: Learning Regular Sets From Queries and Counterexamples |
Date: | 29. 5. a 5. 6. 2009 |
---|---|
Speaker: | Jiří Šimáček |
Topic: | Separační logika |
References: |
J. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures |
Date: | 17. 4. 2009 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Statická analýza pro výpočet May Happen in Parallel (MHP) |
References: |
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 |
Date: | 10. 4. 2009 |
---|---|
Speaker: | Vendula Hrubá |
Topic: | Základy bezzámkové synchronizace |
References: |
L. Lamport: Concurrent Reading and Writing |
Date: | 27. 2. 2009 |
---|---|
Speaker: | Filip Konečný |
Topic: | Čítačové automaty - pokračování |
References: |
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 |
Date: | 13. 2. 2009 |
---|---|
Speaker: | Lukáš Holík |
Topic: | Abstraktní interpretace - pokračování |
References: |
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 |
Date: | 6. 2. 2009 |
---|---|
Speaker: | Lukáš Holík |
Topic: | Abstraktní interpretace - úvod |
References: | viz. Abstraktní interpretace - pokračování |
Date: | 16. 1. 2009 |
---|---|
Speaker: | Adam Rogalewicz |
Topic: | Použití ARTMC pro programy s ukazateli (3. díl úspěšného seriálu) |
References: | tbd |
2008
Date: | 12. 12. 2008 |
---|---|
Speaker: | Adam Rogalewicz |
Topic: | Verifikace dynamických datových struktur pomocí ARTMC (2. díl úspěšného seriálu) |
References: | tbd |
Date: | 5. 12. 2008 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Goldilocks - efektivní počítání Happens-before pomocí množin zámků |
References: |
Elmas T., Quadeer S., Tasiran S.: Goldilocks: a race and transaction-aware java runtime |
Date: | 21. 11. 2008 |
---|---|
Speaker: | Filip Konečný |
Topic: | Čítačové automaty |
References: | tbd |
Date: | 7. 11. 2008 |
---|---|
Speaker: | Petr Muller |
Topic: | tbd |
References: | tbd |
Date: | 31. 10. 2008 |
---|---|
Speaker: | Jiří Šimáček |
Topic: | Verifikace paralelních programů s ukazatali pomocí ARTMC |
References: | tbd |
Date: | 24. 10. 2008 |
---|---|
Speaker: | Vendula Hrubá |
Topic: | Partial Order Redukce a prohledávání stavového prostoru |
References: | Hrubá V.: Bounded model checking v nástroji Java PathFinder |
Date: | 17. 10. 2008 |
---|---|
Speaker: | Lukáš Holík |
Topic: | Využití simulace a bisimulace v analýze programů s ukazateli |
References: |
Date: | 10. 10. 2008 |
---|---|
Speaker: | Zdeněk Letko |
Topic: | Existující přístupy k dynamické detekci data race a porušení atomicity |
References: | Letko Z.: Dynamic Data Race Detection and Healing in Java |