Tipp
Weitere Kapitel dieses Buchs durch Wischen aufrufen
Tipp schließen
In prior work we proposed a mechanism of “witness generation and propagation” to construct proofs of the correctness of program transformations. Here we present a simpler theory, and describe our experience with an initial implementation based on the LLVM open-source compiler and the Z3 SMT solver.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
Springer Professional "Wirtschaft+Technik"
Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:
über 69.000 Bücher
über 500 Zeitschriften
aus folgenden Fachgebieten:
Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko
Testen Sie jetzt 30 Tage kostenlos.
Springer Professional "Technik"
Mit Springer Professional "Technik" erhalten Sie Zugriff auf:
über 50.000 Bücher
über 380 Zeitschriften
aus folgenden Fachgebieten:
Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe
Testen Sie jetzt 30 Tage kostenlos.
Springer Professional "Wirtschaft"
Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:
über 58.000 Bücher
über 300 Zeitschriften
aus folgenden Fachgebieten:
Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko
Testen Sie jetzt 30 Tage kostenlos.
Titel
A Witnessing Compiler: A Proof of Concept
Buch
Runtime Verification
Print ISBN: 978-3-642-40786-4
Electronic ISBN: 978-3-642-40787-1
Copyright-Jahr: 2013
https://doi.org/10.1007/978-3-642-40787-1
DOI
https://doi.org/10.1007/978-3-642-40787-1_22
Autoren:
Kedar S. Namjoshi
Verlag
Springer Berlin Heidelberg
Sequenznummer
22
