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
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2014 | OriginalPaper | Buchkapitel

Certified Complexity (CerCo)

verfasst von : Roberto M. Amadio, Nicolas Ayache, Francois Bobot, Jaap P. Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli

Erschienen in: Foundational and Practical Aspects of Resource Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We provide an overview of the FET-Open Project CerCo (‘Certified Complexity’). Our main achievement is the development of a technique for analysing non-functional properties of programs (time, space) at the source level with little or no loss of accuracy and a small trusted code base. The core component is a C compiler, verified in Matita, that produces an instrumented copy of the source code in addition to generating object code. This instrumentation exposes, and tracks precisely, the actual (non-asymptotic) computational cost of the input program at the source level. Untrusted invariant generators and trusted theorem provers may then be used to compute and certify the parametric execution time of the code.

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
Nächstes Kapitel On the Modular Integration of Abstract Semantics for WCET Analysis
Literatur
1.
2.
Amadio, R., Asperti, A., Ayache, N., Campbell, B., Mulligan, D.P., Pollack, R., Régis-Gianas, Y., Coen, C.S., Stark, I.: Certified complexity. Procedia Comput. Sci. 7, 175–177 (2011). Proceedings of the 2nd European Future Technologies Conference and Exhibition 2011 (FET 11)CrossRef
3.
Amadio, R.M., Régis-Gianas, Y.: Certifying and reasoning on cost annotations of functional programs. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2011. LNCS, vol. 7177, pp. 72–89. Springer, Heidelberg (2012). Extended version to appear in Higher Order and Symbolic ComputationCrossRef
4.
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011)CrossRef
5.
6.
7.
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: POPL, pp. 178–188. ACM Press (1987)
8.
Cazorla, F., Quiñones, E., Vardanega, T., Cucu, L., Triquet, B., Bernat, G., Berger, E., Abella, J., Wartel, F., Houston, M., Santinelli, L., Kosmidis, L., Lo, C., Maxim, D.: Proartis: probabilistically analysable real-time systems. Trans. Embed. Comput. Syst. (2012)
9.
10.
Correnson, L., Cuoq, P., Kirchner, F., Prevosto, V., Puccetti, A., Signoles, J., Yakobowski, B.: Frama-C user manual. CEA-LIST, Software Safety Laboratory, Saclay, F-91191. http://​frama-c.​com/​
11.
Hammond, K., Dyckhoff, R., Ferdinand, C., Heckmann, R., Hofmann, M., Jost, S., Loidl, H.W., Michaelson, G., Pointon, R.F., Scaife, N., Sérot, J., Wallace, A.: The EmBounded project (project start paper). Trends Funct. Program. TFP 6, 195–210 (2005)
12.
13.
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)CrossRef
14.
Mulligan, D.P., Sacerdoti Coen, C.: On the correctness of an optimising assembler for the intel MCS-51 microprocessor. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 43–59. Springer, Heidelberg (2012)CrossRef
15.
16.
Tranquilli, P.: Indexed labels for loop iteration dependent costs. In: QAPL. EPTCS, vol. 117, pp. 19–23 (2013)
17.
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenström, P.: The worst-case execution-time problem-overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 1–53 (2008)CrossRef
18.
Wögerer, W.: A survey of static program analysis techniques. Technical report, Technische Universität Wien (2005)
Metadaten
Titel
Certified Complexity (CerCo)
verfasst von
Roberto M. Amadio
Nicolas Ayache
Francois Bobot
Jaap P. Boender
Brian Campbell
Ilias Garnier
Antoine Madet
James McKinna
Dominic P. Mulligan
Mauro Piccolo
Randy Pollack
Yann Régis-Gianas
Claudio Sacerdoti Coen
Ian Stark
Paolo Tranquilli
Copyright-Jahr
2014
Buch
Foundational and Practical Aspects of Resource Analysis

Print ISBN: 978-3-319-12465-0

Electronic ISBN: 978-3-319-12466-7

Copyright-Jahr: 2014

DOI
https://doi.org/10.1007/978-3-319-12466-7_1

Neuer Inhalt

    Bildnachweise