ParaDiSe Seminar
The ParaDiSe Seminar is a working forum for the presentation of ongoing and finished research in the areas related to the specification, modelling, analysis, and verification of software systems.
The meetings are held on Thursday at the Faculty of Informatics, Masaryk University, starting at 12:00.
Seminar Programme — Spring 2018
There will be two kinds of presentations this semester.
- paper presentations
- You will be presenting paper of your choice (but relevant to lab topics). You can have a look into recommended conferences and papers lower on this page. You should focus on the higher level ideas and message of the paper. The presentations should be rougly 60 minutes, but keep in mind there will be questions during the presentation.
- work presentation
- You will present your work. The presentation should include motivation for your work, what will be the results you hope to achieve. You can also speak about what makes the work iteresting for your, what you learned, what makes it difficult, … Try not to be too technical. Presentations should be short – maximum is 20 minutes, there will be three such presentations in work presentation session.
Each member of the lab is expected to do both presentations.
Recommended Conferences and Papers
(more will be added hopefully)
- NASA Formal Methods 2018 (most papers are not available yet)
- SPIN 2017
- Principles of Programming Languages 2018
- Programming Language Design and Implementation 2017
- Principles and Practice of Parallel Programming 2017
- Formal Methods in Computer-Aided Design 2017
- K-Induction without Unrolling (probably too theoretical for us)
- Automated Technology for Verification and Analysis 2017
- Computer Aided Verification 2017
Schedule
-
February 19, 2018
Semester start (max 30 minutes)
-
February 26, 2018
Work Presentations I
Vladimír Štill: Lazy x86-TSO Memory Model for C++ Verification
Tadeáš Kučera: My DIVINE Contribution
Jaroslav Bendík: Finding Minimal Unsatisfiable Subsets
-
March 5, 2018: slides
Effective stateless model checking for C/C++ concurrency (POPL 2018)
(Vladimír Štill) -
March 12, 2018: slides
Concurrent Program Verification With Invariant-guided Underapproximation (ATVA 2017)
(Jan Mrázek) -
March 19, 2018: slides
Graph-based optimal reconfiguration planning for self-reconfigurable robots
(Viktória Vozárová) -
March 26, 2018
Context-Sensitive Dynamic Partial Order Reduction (CAV 2017)
(Jan Tušil) -
April 2, 2018
Cancelled (Easter Monday)
-
April 9, 2018
Stateless model checking of the Linux kernel’s hierarchical read-copy-update (tree RCU) (SPIN 2017)
(Adam Matoušek) -
April 16, 2018
Lasso Detection using Partial-State Caching (FMCAD 2017)
(Zuzana Baranová) -
April 23, 2018
Explicit state model checking with generalized Büchi and Rabin automata (SPIN 2017)
(Tadeáš Kučera) -
April 30, 2018
Work Presentations II
Lukáš Korenčík: TBA
Adam Matoušek: TBA
-
May 7, 2018
Checking Concurrent Data Structures Under the C/C++11 Memory Model (PPoPP 2017)
(Lukáš Korenčík) -
May 14, 2018
Work Presentations III
Zuzana Baranová: TBA
Henrich Lauko: TBA
-
May 21, 2018: slides
Work Presentations IV: RoFI
Viktóra Vozárová
Jan Mrázek