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 2016
The theme for this semester are verification tools with support for C/C++ (or LLVM). Each presentation should include:- what are the theoretical principles the tool builds on,
- what languages it support, how extensive is the support (i.e. library support, threading library, are exceptions supported if C++ is?),
- what tools it builds upon (i.e. SMT solvers, other verification tools)
- what is the main aim of the tool (if specified),
- is the tool free to get, did you manage to test it?
- February 22, 2016
Semester start
- February 29, 2016 (canceled)
buffer/preparation
- March 7, 2016
MU-CSeq/Lazy-CSeq: verificition of parallel code using sequentialization
(Vladimír Štill) (pdf) - March 14, 2016
The Vienna Verification Toolkit (VVT)
(Kristýna Pavlíčková) - March 21, 2016
The Concurrency Intermediate Verification Language (CIVL)
(Jan Mrázek) - March 28, 2016 (canceled)
Public Holiday: Easter Monday
- April 4, 2016 (canceled)
TACAS/SPIN
- April 11, 2016
ESBMC (Efficient SMT-Based Context-Bounded Model Checker)
(Eva Tesařová) - April 18, 2016
LTSmin
(Petr Bezděk) - April 25, 2016
CBMC
(Henrich Lauko) - May 2, 2016
SMACK: A Bounded Software Verifier for C Programs (paper)
(Tomáš Zábojník) - May 9, 2016
LLVMVF - LLVM Verification Framework
(Jaroslav Bendík) - May 16, 2016
Petangue Closed