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
International Journal on Software Tools for Technology Transfer
Published in: International Journal on Software Tools for Technology Transfer 5/2014

01-10-2014 | Rers

Applying symbolic bounded model checking to the 2012 RERS greybox challenge

Authors: Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer

Published in: International Journal on Software Tools for Technology Transfer | Issue 5/2014

Log in

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

search-config
loading …

Abstract

We describe the application of ESBMC, a symbolic bounded model checker for C programs, to the 2012 RERS greybox challenge. We checked the reachability properties via reachability of the error labels, and the behavioral properties via a bounded LTL model checking approach. Our approach could solve about 700 properties for the small and medium problems from the offline phase, and scored overall about 5,000 marks but still ranked last in the competition.
previous article BDD-based software verification
next article Analyzing program behavior through active automata learning

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
Appendix
Available only for authorised users
Footnotes
1
With further improvements by Babiak et al. [1].
 
2
Note that the internal program structure still plays a role: for the same unwinding bound the hard problems take one to two orders of magnitude longer than the easy or moderate ones; see Table 1 for details.
 
3
Since this specific LTL formula only uses output the traces (and thus prefixes) consist of output-literals only. However, the corresponding input values can still be extracted from the BMC counterexamples.
 
Literature
1.
Babiak, T., Kr̆etínský, M., Rehák, V., Strejc̆ek, J.: LTL to Büchi Automata translation: fast and more deterministic. TACAS, LNCS 7241, 95–109 (2012)
2.
Bauer, A., Haslum, P.: LTL goal specifications revisited. ECAI’10 Front. Artif. Intell. Appl. 215, 881–886 (2010)
3.
4.
Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. TACAS, LNCS 5505, 174–177 (2009)
5.
Chai, M., Li, X., Zhao, L.: Runtime verification based on 4-valued past time LTL. In: Intl. Conf. Computer Science and Information Processing, pp. 567–570 (2012)
6.
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. TACAS, LNCS 2988, 168–176 (2004)
7.
Clarke, E., Lerda, F.: Model checking: software and beyond. J. Univ. Computer Sci. 13, 639–649 (2007)MathSciNet
8.
Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. ICSE, pp. 331–340 (2011)
9.
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957–974 (2012)CrossRef
10.
Cordeiro, L., Morse, J., Nicole, D., Fischer, B.: Context-bounded model checking with ESBMC 1.17. TACAS, LNCS 7214, 533–536 (2012)
11.
de Moura, L.M., Bjørner, N.: An efficient SMT solver:Z3. TACAS, LNCS 4963, 337–340 (2008)
12.
Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. CAV, LNCS 2102, 53–65 (2001)MathSciNet
13.
Holzmann, G.: The SPIN Model Checker—Primer and Reference Manual. Addison-Wesley, Boston (2004)
14.
15.
Lamport, L.: What good is temporal logic? Inf. Process. 83, 657–668 (1983)
16.
Li, X., Chai, M., Zhao, L., Tang, T., Xu, T.: Safety monitoring for ETCS with 4-valued LTL. In: Intl. Symposium Autonomous Decentralized Systems, pp. 86–91 (2011)
17.
Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Context-bounded model checking of LTL properties for ANSI-C software. SEFM, LNCS 7041, 302–317 (2011)
18.
Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Model checking LTL properties over ANSI-C programs with bounded traces. J. Softw. Syst. Model (2013) (Online first)
19.
Pnueli, A.: The temporal logic of programs. FOCS, pp. 46–57 (1977)
20.
van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful Brute force attack of the RERS 2012 and 2013 challenges. STTT, this volume (2014)
21.
Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. STTT. doi:10.​1007/​s10009-014-0336-z (2014)
22.
Metadata
Title
Applying symbolic bounded model checking to the 2012 RERS greybox challenge
Authors
Jeremy Morse
Lucas Cordeiro
Denis Nicole
Bernd Fischer
Publication date
01-10-2014
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 5/2014
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0335-0

Other articles of this Issue 5/2014

International Journal on Software Tools for Technology Transfer 5/2014 Go to the issue

Introduction

A taxonomy of risk-based testing

RERS

Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges

RBT

A multiple case study on risk-based testing in industry

RBT

Dynamic test planning: a study in an industrial context

RERS

Tailored generation of concurrent benchmarks

RBT

Risk-based testing via active continuous quality control

Premium Partner

    Image Credits