Bounded Model Checking for Verifying Concurrent Programs

Reference:

Toni Jussila. Bounded model checking for verifying concurrent programs. Research Report A73, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science, Espoo, Finland, August 2002.

Abstract:

A simple, parallel programming language is introduced and an operational semantics for it is developed. The language combines the syntax of C and Java together with the communication primitives taken from PROMELA.

A verification method for specifications given in the language is developed for detecting the violation of temporal reachability and safety properties. The method is known as Bounded Model Checking (BMC) where the idea is to reduce the model checking problem to propositional satisfiability.

A compact boolean encoding of parallel programs is devised, together with the proofs of its soundness and completeness. Encoding of the reachability and safety properties is developed and finally semantical models for strengthening the encoding are discussed.

Keywords:

bounded model checking, verification, concurrent program

Suggested BibTeX entry:

@techreport{HUT-TCS-A73,
    address = {Espoo, Finland},
    author = {Toni Jussila},
    institution = {Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science},
    month = {August},
    number = {A73},
    pages = {55},
    title = {Bounded Model Checking for Verifying Concurrent Programs},
    type = {Research Report},
    year = {2002},
}