|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'506'133
Articles rated: 2609
26 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
SMT-based Bounded Model Checking with Difference Logic Constraints | | Marcello M. Bersani
; Achille Frigeri
; Angelo Morzenti
; Matteo Pradella
; Matteo Rossi
; Pierluigi San Pietro
; | | Date: |
7 Apr 2010 | | Abstract: | Traditional Bounded Model Checking (BMC) is based on translating the model
checking problem into SAT, the Boolean satisfiability problem. This paper
introduces an encoding of Linear Temporal Logic with Past operators (PLTL) into
the Quantifier-Free Difference Logic with Uninterpreted Functions (QF-UFIDL).
The resulting encoding is a simpler and more concise version of existing
SATbased encodings, currently used in BMC. In addition, we present an extension
of PLTL augmented with arithmetic relations over integers, which can express
unbounded counters; as such, the extended logic is more expressive than PLTL.
We introduce suitable restrictions and assumptions that are shown to make the
verification problem for the extended logic decidable, and we define an
encoding of the new logic into QF-UFIDL. Finally, a performance comparison with
the SAT-based approach on purely PLTL examples shows significant improvements
in terms of both execution time and memory occupation. | | Source: | arXiv, 1004.1077 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER