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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Termination Analysis of Probabilistic Programs Through Positivstellensatz’s Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

RV-Match: Practical Semantics-Based Program Analysis

verfasst von : Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Roşu

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We present RV-Match, a tool for checking C programs for undefined behavior and other common programmer mistakes. Our tool is extracted from the most complete formal semantics of the C11 language. Previous versions of this tool were used primarily for testing the correctness of the semantics, but we have improved it into a tool for doing practical analysis of real C programs. It beats many similar tools in its ability to catch a broad range of undesirable behaviors. We demonstrate this with comparisons based on a third-party benchmark.

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
Vorheriges Kapitel From Shape Analysis to Termination Analysis in Linear Time
Nächstes Kapitel Under-Approximating Backward Reachable Sets by Polytopes
Fußnoten
5
Version 3.4.0, with \(\mathbb {K}\) Framework version 3.4.
 
6
These tests were run on a dual CPU 2.4 GHz Intel Xeon with 8 GB of memory. On more memory-intensive programs, we see an additional order of magnitude or more improvement in performance.
 
Literatur
1.
2.
Beyer, D.: Reliableand reproducible competition results with BenchExec and witnesses. In: Chechik, M., Raskin, J.-F. (eds.) Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference (TACAS 2016), (Report on SV-COMP 2016), pp. 887–904 (2016). ISBN: 978-3-662-49674-9, doi:10.​1007/​978-3-662-49674-9_​55
3.
Campbell, B.: An executable semantics for CompCert C. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 60–75. Springer, Heidelberg (2012)CrossRef
4.
Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: Conference Source Code Analysis and Manipulation (SCAM 2009), pp. 123–124. IEEE (2009). doi:10.​1109/​SCAM.​2009.​22
5.
6.
7.
Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 533–544 (2012). doi:10.​1145/​2103656.​2103719
8.
9.
Hathhorn, C., Ellison, C., Roşu, G.: Defining the undefinedness of C. In: 36th Conference on Programming Language Design and Implementation (PLDI 2015) (2015)
10.
ISO/IEC JTC 1, SC 22, WG 14. ISO/IEC 9899:2011: Programming Language C Technical report International Organisation for Standardization (2012)
11.
12.
13.
Nethercote, N., Seward, J.: Valgrind: a framework for heavy-weight dynamic binary instrumentation. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2007), pp. 89–100. ACM (2007). doi:10.​1145/​1250734.​1250746
14.
Shiraishi, S., Mohan, V., Marimuthu, H.: Test suites for benchmarks of static analysis tools. In: The 26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015), Industrial Track (2015)
Metadaten
Titel
RV-Match: Practical Semantics-Based Program Analysis
verfasst von
Dwight Guth
Chris Hathhorn
Manasvi Saxena
Grigore Roşu
Copyright-Jahr
2016
Buch
Computer Aided Verification

Print ISBN: 978-3-319-41527-7

Electronic ISBN: 978-3-319-41528-4

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41528-4_24

Premium Partner

    Bildnachweise