... PraSe ;-)

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