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
Erschienen in:
Partial Evaluation of Order-Sorted Equational Programs Modulo Axioms Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Symbolic Abstract Contract Synthesis in a Rewriting Framework

verfasst von : María Alpuente, Daniel Pardo, Alicia Villanueva

Erschienen in: Logic-Based Program Synthesis and Transformation

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the \(\mathbb {K}\) framework, we enrich the symbolic execution facilities recently provided by C with novel capabilities for assertion synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that explains the execution of a (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.0, which generates logical axioms that define the precise input/output behavior of the C routines.

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 A Productivity Checker for Logic Programming
Nächstes Kapitel On the Completeness of Selective Unification in Concolic Testing of Logic Programs
Fußnoten
1
Symbolic values are preceded by aquestion mark.
 
2
An object in C is a region of data storage in the execution environment.
 
3
By abuse, we assume a logical constraint representation \(x_1= v_1 \wedge \ldots \wedge x_n= v_n\) of the symbolic heap \(\{x_1\mapsto v_1, \ldots , x_n\mapsto v_n\}\), where every \(x_i\) refers to a field of a https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-63139-4_11/429227_1_En_11_IEq83_HTML.gif data object, or to a primitive-type program variable if \(x_i\) occurs in https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-63139-4_11/429227_1_En_11_IEq85_HTML.gif .
 
Literatur
1.
Alpuente, M., Feliú, M.A., Villanueva, A.: Automatic inference of specifications using matching logic. In: Proceedings of PEPM 2013, pp. 127–136. ACM (2013)
2.
Alpuente, M., Pardo, D., Villanueva, A.: Automatic inference of specifications in the K framework. EPTCS 200, 1–17 (2015)CrossRef
3.
Anand, S., Păsăreanu, C.S., Visser, W.: Symbolic execution with abstraction. STTT 11(1), 53–67 (2008)CrossRef
4.
Arusoaie, A., Lucanu, D., Rusu, V.: Symbolic execution based on language transformation. Comput. Lang. Syst. Struct. 44(Part A), 48–71 (2015)
5.
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Footprint analysis: a shape analysis that discovers preconditions. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402–418. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-74061-2_​25 CrossRef
6.
Claessen, K., Smallbone, N., Hughes, J.: QuickSpec: guessing formal specifications using testing. In: Fraser, G., Gargantini, A. (eds.) TAP 2010. LNCS, vol. 6143, pp. 6–21. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-13977-2_​3 CrossRef
7.
Cousot, P., Cousot, R., Fähndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128–148. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-35873-9_​10 CrossRef
8.
Ellison, C., Roşu, G.: An executable formal semantics of C with applications. In: Proceedings of POPL 2012, pp. 533–544. ACM (2012)
9.
Gulavani, B.S., Chakraborty, S., Ramalingam, G., Nori, A.V.: Bottom-up shape analysis using LISF. ACM Trans. Program. Lang. Syst. 33(5), 17 (2011)CrossRefMATH
10.
11.
Khurshid, S., PĂsĂreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003). doi:10.​1007/​3-540-36577-X_​40 CrossRef
12.
13.
Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)MATH
14.
Magill, S., Nanevski, A., Clarke, E., Lee, P.: Inferring invariants in separation logic for imperative list-processing programs. In: Proceedings of SPACE Workshop (2006)
15.
Meyer, B.: Applying ‘design by contract’. Computer 25(10), 40–51 (1992)CrossRef
16.
17.
Moy, Y., Marché, C.: Modular inference of subprogram contracts for safety checking. J. Symbolic Comput. 45(11), 1184–1211 (2010)MathSciNetCrossRefMATH
18.
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. JLAP 79(6), 397–434 (2010)MathSciNetMATH
19.
Tillmann, N., Chen, F., Schulte, W.: Discovering likely method specifications. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 717–736. Springer, Heidelberg (2006). doi:10.​1007/​11901433_​39 CrossRef
20.
Wei, Y., Furia, C.A., Kazmin, N., Meyer, B.: Inferring better contracts. In: Proceedings of the ICSE 2011, 191–200. ACM (2011)
Metadaten
Titel
Symbolic Abstract Contract Synthesis in a Rewriting Framework
verfasst von
María Alpuente
Daniel Pardo
Alicia Villanueva
Copyright-Jahr
2017
Buch
Logic-Based Program Synthesis and Transformation

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

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

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-63139-4_11