Previous article
05 September 2016
Master Thesis Defence by Mr Thanh Hai Tran
Mr Thanh Hai Tran defended his master thesis on 'User-guided predicate abstraction of TLA+ specification'
Mr Thanh Hai Tran defended his master thesis on 'User-guided predicate abstraction of TLA+ specification' at TUW on 22 June 2016.
Abstract: TLA+ is a general-purposed languaged introduced by Leslie Lamport to formally specify and analyse systems. To make the verification process automatic, the model checker TLC was developed. While many advanced techniques have been introduced to scope with the state-space explosion problem, TLC is still a explicit-state model checker. The goal of this thesis is to develop a technique for applying predicate abstraction and IC3 to verify safety properties of Systems.