nach oben

Automated Software Engineering

Erschienen in:

01.03.2007

Inferring specifications to detect errors in code

verfasst von: Mana Taghdiri, Daniel Jackson

Erschienen in: Automated Software Engineering | Ausgabe 1/2007

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

A new technique is presented to statically check a given procedure against a user-provided property. The method requires no annotations; it automatically infers a context-dependent specification for each procedure call, so that only as much information about a procedure is used as is needed to analyze its caller. Specifications are inferred iteratively. Empty specifications are initially used to over-approximate the effects of all procedure calls; these are later refined in response to spurious counterexamples. When the analysis terminates, any remaining counterexample is guaranteed to be valid. However, since the heap is finitized, the absence of a counterexample does not guarantee the validity of the given property in general.

Vorheriger Artikel The design and implementation of a dataflow language for scriptable debugging

Nächster Artikel Dessert Island

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

Special cases, e.g. updating arrays which are passed as parameters, can be easily added to this algorithm.

Balaban, I., Pnueli, A., Zuck, L.: Shape analysis by predicate abstraction. In: Proc. of VMCAI (2005)

Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: SPIN 2000 Workshop on Model Checking of Software, pp. 113–130 (2000)

Ball, T., Rajamani, S.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software, pp. 103–122 (2001)

Ball, T., Rajamani, S.K.: Generating abstract explanations of spurious counterexamples in C programs, MSR-TR-2002-09, pp. 113–130 (2002)

Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: International Conference on Software Engineering (2003)

Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: Proc. Programming Languages Design and Implementation (1990)

Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. International Conference on Computer-Aided Verification, pp. 154–169 (2000)

Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from java source code. In: Proc. International Conference on Software Engineering (2000)

Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press (1990)

Detlefs, D.L., Nelson, G., Saxe, J.B.: A theorem prover for program checking. Research Report 178, Compaq SRC (2002)

Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ (1976)

Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw. Eng. 27(2), (2001)

Flanagan, C.: Software model checking via iterative abstraction refinement of constraint logic queries. In: Workshop on Constraint Programming and Constraints for Verification (2004)

Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proff explication. In: International Conference on Computer Aided Verification (2003)

Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for java. In: Proc. Conference on Programming Language Design and Implementation, pp. 234–245 (2002)

Graf, S., Saidi, H.: Construction of abstract state graphs via PVS. In: Proc. International Conference on Computer Aided Verification, pp. 72–83 (1997)

Hatcliff, J., Dwyer, M.: Slicing software for model construction. In: Proc. ACM Workshop of Partial Evaluation and Program Manipulation (1999)

Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Proc. International Conference on Computer-Aided Verification, pp. 526–538 (2002)

Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–294 (1997)

Jackson, D., Schechter, I., Shlyakhter, I.: Alcoa: the alloy constraint analyzer. In: Proc. International Conference on Software Engineering (2000)

Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: Proc. ACM SIGSOFT Conference on Foundations of Software Engineering (2001)

Jaffar, J., Maher, M.J.: Constraint logic programing: a survey. J. Log. Program. 19(20), 503–581 (1994)

Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: Proc. of SAS (2004)

McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers (1993)

Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference (2001)

Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2, 293–304 (1986)

Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst. 20(1), 1–50 (1998)

Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

Shlyakhter, I.: Declarative symbolic pure logic model checking. Ph.D Thesis, Electrical Engineering and Computer Science Department, MIT (2005)

Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging declarative models using unsatisfiable core. Autom. Softw. Engine. (2003)

Sitaraman, M., Gandi, D.P., Kuchlin, W., Sinz, C., Weide, B.W.: The humane bugfinder: modular static analysis using a SAT solver. Technical Report RSRG-03-05, Dept. of Computer Science, Clemson Univ. (2003)

Taghdiri, M.: Inferring specifications to detect errors in code. Autom. Softw. Engin. (2004)

Vaziri, M.: Finding bugs in software with a constraint solver. Ph.D Thesis, Electrical Engineering and Computer Science Department, MIT (2004)

Visser, W., Brat, G., Havelund, K., Park, S.: Model checking programs. In: Proc. IEEE International Conference on Automated Software Engineering (2000)

Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: Proc. Symposium on Principles of Programming Languages, pp. 351–363 (2005)

Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Design, Automation and Test in Europe(DATE) (2003)

Titel: Inferring specifications to detect errors in code
verfasst von: Mana Taghdiri
Daniel Jackson
Publikationsdatum: 01.03.2007
Verlag: Kluwer Academic Publishers-Plenum Publishers
Erschienen in: Automated Software Engineering / Ausgabe 1/2007
Print ISSN: 0928-8910
Elektronische ISSN: 1573-7535
DOI: https://doi.org/10.1007/s10515-006-0005-x

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 1/2007

JDiff: A differencing technique and tool for object-oriented programs

The design and implementation of a dataflow language for scriptable debugging

On the effect of test-suite reduction on automatically generated model-based tests

Introduction

Dessert Island

Premium Partner