Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen 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

verfasst von: Jeremy Morse, Lucas Cordeiro, Denis Nicole, Bernd Fischer

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.
Vorheriger Artikel BDD-based software verification
Nächster Artikel Analyzing program behavior through active automata learning

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
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.
 
Literatur
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.
Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)CrossRefMATHMathSciNet
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.
Visser, W.: Personal communication (2012)
Metadaten
Titel
Applying symbolic bounded model checking to the 2012 RERS greybox challenge
verfasst von
Jeremy Morse
Lucas Cordeiro
Denis Nicole
Bernd Fischer
Publikationsdatum
01.10.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 5/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0335-0

Weitere Artikel der Ausgabe 5/2014

International Journal on Software Tools for Technology Transfer 5/2014 Zur Ausgabe

RERS

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

RBT

Approaches for the combined use of risk analysis and testing: a systematic literature review

RBT

Risk-based testing via active continuous quality control

Introduction

A taxonomy of risk-based testing

Rers

Analyzing program behavior through active automata learning

RERS

BDD-based software verification

Premium Partner

    Bildnachweise