Result Details

Experience from Verifying in TVLA

ERLEBACH, P. Experience from Verifying in TVLA. EEICT'05. volume 3. Brno: Faculty of Electrical Engineering and Communication BUT, 2005. p. 648-652. ISBN: 80-214-2890-2.

Type

conference paper

Language

English

Authors

Erlebach Pavel, Ing., Ph.D., FIT (FIT), DITS (FIT)

Abstract

This paper aims at analysis of capabilities of the TVLA verification tool. There are used InsertBST procedure, which inserts a new node to the binary sorted tree, and Bakery algorithm, which is one of the most famous mutual exclusion algorithms, as examined examples.

Keywords

TVLA, InsertBST, formal verification, Bakery algorithm

Published

2005

Pages

648–652

Proceedings

EEICT'05

Series

volume 3

Conference

STUDENT EEICT 2005

ISBN

80-214-2890-2

Publisher

Faculty of Electrical Engineering and Communication BUT

Place

Brno

BibTeX

@inproceedings{BUT17968,
  author="Pavel {Erlebach}",
  title="Experience from Verifying in TVLA",
  booktitle="EEICT'05",
  year="2005",
  series="volume 3",
  pages="648--652",
  publisher="Faculty of Electrical Engineering and Communication BUT",
  address="Brno",
  isbn="80-214-2890-2"
}

Projects

Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems, GACR, Postdoktorandské granty, GP102/03/D211, start: 2003-09-01, end: 2006-09-01, completed
Automated methods and tools supporting development of reliable parallel and distributed systems, GACR, Standardní projekty, GA102/04/0780, start: 2004-01-01, end: 2006-12-31, completed
Integrated approach to education of PhD students in the area of parallel and distributed systems, GACR, Doktorské granty, GD102/05/H050, start: 2005-01-01, end: 2008-12-31, completed

Departments

Department of Intelligent Systems (DITS)