Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Analysis of Asynchronously Communicating Systems Read chapter Read first chapter

2016 | OriginalPaper | Chapter

ESBMC\(^{QtOM}\): A Bounded Model Checking Tool to Verify Qt Applications

Authors : Mário Garcia, Felipe Monteiro, Lucas Cordeiro, Eddie de Lima Filho

Published in: Model Checking Software

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We integrate a simplified model of the Qt framework, named as Qt operational model (QtOM), into the efficient SMT-based context-bounded model checker (ESBMC++), which results in ESBMC\(^{QtOM}\). In particular, ESBMC\(^{QtOM}\) is a bounded model checking tool to verify Qt-based applications, which focuses on the verification of code properties, such as invalid memory access and containers usage, through pre- and postconditions, data usage evaluation, and simulation features. Experimental results show that ESBMC\(^{QtOM}\) can be effectively and efficiently applied to verify Qt-based consumer electronics applications.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter River Basin Management with Spin
next chapter Autonomous Agent Behaviour Modelled in PRISM – A Case Study
Footnotes
Literature
1.
Berard, B., Bidoit, M., Finkel, A.: Systems and Software Verification: Model-Checking Techniques and Tool. Springer Publishing, Heidelberg (2010)MATH
2.
Ramalho, M., et al.: SMT-based bounded model checking of C++ programs. In: ECBS, pp. 147–156 (2013)
3.
4.
Mehlitz, P., Rungta, N., Visser, W.: A hands-on Java pathfinder tutorial. In: ICSE, pp. 1493–1495 (2013)
5.
Piesing, J.: The DVB multimedia home platform (MHP) and related specifications. Proc. IEEE 94(1), 237–247 (2006)CrossRef
6.
van der Merwe, H., et al.: Execution and property specifications for JPF-Android. ACM SIGSOFT Softw. Eng. Notes 39(1), 1–5 (2014)CrossRef
7.
van der Merwe, H., et al.: Generation of library models for verification of Android applications. ACM SIGSOFT Softw. Eng. Notes 40(1), 1–5 (2015)CrossRef
8.
Monteiro, F., Cordeiro, L., de Lima Filho, E.: Bounded model checking of C++ programs based on the Qt Framework. In: GCCE, pp. 179–180 (2015)
9.
10.
11.
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE TSE 38(4), 957–974 (2012)
12.
de la Cámara, P., Castro, J., Gallardo, M., Merino, P.: Verification support for ARINC-653-based avionics software. JSTVR 21(4), 267–298 (2011)
Metadata
Title
ESBMC: A Bounded Model Checking Tool to Verify Qt Applications
Authors
Mário Garcia
Felipe Monteiro
Lucas Cordeiro
Eddie de Lima Filho
Copyright Year
2016
Book
Model Checking Software

Print ISBN: 978-3-319-32581-1

Electronic ISBN: 978-3-319-32582-8

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-32582-8_6

Premium Partner

    Image Credits