kirancodes.me
To Proof Maintenance & Beyond!
ICSE 2015

Efficient Scalable Verification of LTL Specifications

Luciano Baresi, Mohammad Mehdi Pourhashem Kallehbasti, Matteo Rossi

Full textDOI 10.1109/icse.2015.84dblp

Abstract

Linear Temporal Logic (LTL) has been used in computer science for decades to formally specify programs, systems, desired properties, and relevant behaviors. This paper presents a novel, efficient technique for verifying LTL specifications in a fully automated way. Our technique belongs to the category of Bounded Satisfiability Checking approaches, where LTL formulae are encoded as formulae of another decidable logic that can be solved through modern satisfiability solvers. The target logic in our approach is Bit-Vector Logic. We present our novel encoding, show its correctness, and experimentally compare it against existing encodings implemented in well-known formal verification tools.

BibTeX
@inproceedings{Baresi-al:ICSE15,
  author    = {Luciano Baresi and
               Mohammad Mehdi Pourhashem Kallehbasti and
               Matteo Rossi},
  title     = {Efficient Scalable Verification of {LTL} Specifications},
  booktitle = {ICSE (Part I)},
  pages     = {711--721},
  publisher = {{IEEE} Computer Society},
  year      = {2015},
}

Related papers