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
KI - Künstliche Intelligenz
Erschienen in: KI - Künstliche Intelligenz 1/2010

01.04.2010 | Fachbeitrag

Practical Aspects of Automated Deduction for Program Verification

verfasst von: Wolfgang Ahrendt, Bernhard Beckert, Martin Giese, Philipp Rümmer

Erschienen in: KI - Künstliche Intelligenz | Ausgabe 1/2010

Einloggen

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

search-config
loading …

Abstract

Software is vital for modern society. It is used in many safety- or security-critical applications, where a high degree of correctness is desirable. Over the last years, technologies for the formal specification and verification of software—using logic-based specification languages and automated deduction—have matured and can be expected to complement and partly replace traditional software engineering methods in the future. Program verification is an increasingly important application area for automated deduction. The field has outgrown the area of academic case studies, and industry is showing serious interest. This article describes the aspects of automated deduction that are important for program verification in practise, and it gives an overview of the reasoning mechanisms, the methodology, and the architecture of modern program verification systems.
Vorheriger Artikel Instance Based Methods—A Brief Overview
Nächster Artikel Logic-Based Question Answering

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

KI - Künstliche Intelligenz

The Scientific journal "KI – Künstliche Intelligenz" is the official journal of the division for artificial intelligence within the "Gesellschaft für Informatik e.V." (GI) – the German Informatics Society - with constributions from troughout the field of artificial intelligence.

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
Weitere Produktempfehlungen anzeigen
Literatur
1.
Ahrendt W (2002) Deductive search for errors in free data type specifications using model generation. In: Voronkov A (ed) Proceedings of 18th international conference on automated deduction (CADE-18), Copenhagen, Denmark. LNCS, vol 2392. Springer, Berlin
2.
Ahrendt W, Beckert B, Hähnle R, Rümmer P, Schmitt PH (2007) Verifying object-oriented programs with KeY: a tutorial. In: de Boer F, Bonsangue M, Graf S, de Roever W (eds) Revised lectures. 5th international symposium on formal methods for components and objects (FMCO 2006), Amsterdam, The Netherlands. LNCS, vol 4709. Springer, Berlin
3.
4.
Barnett M, Leino R, Schulte W (2005) The Spec# programming system: An overview. In: Construction and analysis of safe, secure, and interoperable smart devices (CASSIS). International workshop, 2004, Marseille, France, Revised Selected Papers. LNCS, vol 3362. Springer, Berlin, pp 49–69
5.
Barrett C, Tinelli C (2007) CVC3. In: Damm W, Hermanns H (eds) Proceedings of 19th international conference on computer aided verification (CAV ’07). LNCS, vol 4590. Springer, Berlin, pp 298–302 CrossRef
6.
Beckert B, Hähnle R, Schmitt PH (eds) (2007) Verification of object-oriented software: the KeY approach. LNCS, vol 4334. Springer, Berlin
7.
Beckert B., Moskal M. (2010) Deductive verification of system software in the Verisoft XT project. KI (in this issue)
8.
Bertot Y (2008) A short presentation of Coq. In: Aït Mohamed O, Muñoz C, Tahar S (eds) Proceedings of 21st international conference on theorem proving in higher order logics (TPHOLs), Montreal, Canada. LNCS, vol 5170. Springer, Berlin, pp 12–16 CrossRef
9.
Bradley AR, Manna Z, Sipma HB (2005) Termination of polynomial programs. In: Cousot R (ed) VMCAI. LNCS, vol 3385. Springer, Berlin, pp 113–129
10.
Claessen K, Sörensson N (2003) New techniques that improve MACE-style model finding. In: Proc of workshop on model computation (MODEL)
11.
de Moura L, Bjørner N (2008) Z3: An efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems. Proceedings of the 14th international conference, Budapest, Hungary. LNCS, vol 4963. Springer, Berlin, pp 337–340
12.
DeLine R, Leino KRM (2005) BoogiePL: a typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70. Microsoft Research
13.
Dutertre B (2007) System description: Yices 1.0.10. In: SMT-COMP’07
14.
Falke S, Kapur D (2009) A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt RA (ed) CADE. LNCS, vol 5663. Springer, Berlin, pp 277–293
15.
Filliâtre J-C, Marché C (2004) Multi-prover verification of C programs. In: Proceedings, formal methods and software engineering. LNCS, vol 3308. Springer, Berlin, pp 15–29 CrossRef
16.
Giese M (2001) Incremental closure of free variable tableaux. In: Proc intl joint conf on automated reasoning, Siena, Italy. LNCS, vol 2083. Springer, Berlin, pp 545–560
17.
Harrison J (1996) HOL light: a tutorial introduction. In: Srivas MK, Camilleri AJ (eds) Proceedings, first international conference on formal methods in computer-aided design (FMCAD), Palo Alto, USA. LNCS, vol 1166. Springer, Berlin, pp 265–269
18.
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580, 583 MATHCrossRef
19.
Ireland A, Kovács L (eds) (2009) WING 2009, Workshop on invariant generation
20.
Kaufmann M, Manolios P, Moore JS (2000) Computer-aided reasoning: an approach. Kluwer Academic, Boston
21.
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM symposium on operating systems principles, Big Sky, MT, USA. ACM, October 2009
22.
Podelski A, Rybalchenko A (2004) A complete method for the synthesis of linear ranking functions. In: VMCAI. LNCS, vol 2937. Springer, Berlin, pp 239–251
23.
Rümmer P (2007) A sequent calculus for integer arithmetic with counterexample generation. In: Proceedings, 4th international verification workshop (VERIFY’07). CEUR, vol 259 (http://​ceur-ws.​org/​)
24.
Rümmer P, Shah MA (2007) Proving programs incorrect using a sequent calculus for Java dynamic logic. In: Gurevich Y, Meyer B (eds) Tests and proofs, first international conference, TAP 2007, Zurich, Switzerland, February 12–13, 2007. Revised papers. LNCS, vol 4454. Springer, Berlin, pp 41–60
25.
Schulte W, Songtao X, Smans J, Piessens F (2007) A glimpse of a verifying C compiler. In: Proceedings, C/C++ Verification workshop
26.
Shankar N (2002) Little engines of proof. In: Proceedings, international symposium of formal methods Europe, Copenhagen, Denmark. LNCS, vol 2391. Springer, Berlin, pp 1–20
27.
Velroyen H, Rümmer P (2008) Non-termination checking for imperative programs. In: Beckert B, Hähnle R (eds) Tests and proofs, second international conference, TAP 2008, Prato, Italy. LNCS, vol 4966. Springer, Berlin, pp 154–170
28.
Wenzel M, Paulson LC, Nipkow T (2008) The Isabelle framework. In: Mohamed OA, Muñoz C, Tahar S (eds) Proceedings of 21st international conference on theorem proving in higher order logics (TPHOLs), Montreal, Canada. LNCS, vol 5170. Springer, Berlin, pp 33–38 CrossRef
Metadaten
Titel
Practical Aspects of Automated Deduction for Program Verification
verfasst von
Wolfgang Ahrendt
Bernhard Beckert
Martin Giese
Philipp Rümmer
Publikationsdatum
01.04.2010
Verlag
Springer-Verlag
Erschienen in
KI - Künstliche Intelligenz / Ausgabe 1/2010
Print ISSN: 0933-1875
Elektronische ISSN: 1610-1987
DOI
https://doi.org/10.1007/s13218-010-0001-y

Weitere Artikel der Ausgabe 1/2010

KI - Künstliche Intelligenz 1/2010 Zur Ausgabe

Projekt

Deductive Verification of System Software in the Verisoft XT Project

Fachbeitrag

Instance Based Methods—A Brief Overview

Editorial

Künstliche Intelligenz ab 2010 bei Springer

Editorial

Special Issue on Automated Deduction

Editorial

Willkommen bei Springer

Fachbeitrag

Current Trends in Automated Deduction

Premium Partner

    Bildnachweise