Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
International Journal on Software Tools for Technology Transfer
Published in: International Journal on Software Tools for Technology Transfer 4/2013

01-08-2013 | TACAS 2009

From tests to proofs

Authors: Ashutosh Kumar Gupta, Rupak Majumdar, Andrey Rybalchenko

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2013

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We describe the design and implementation of an automatic invariant generator for imperative programs. While automatic invariant generation through constraint solving has been extensively studied from a theoretical viewpoint as a classical means of program verification, in practice existing tools do not scale even to moderately sized programs. This is because the constraints that need to be solved even for small programs are already too difficult for the underlying (non-linear) constraint solving engines. To overcome this obstacle, we propose to strengthen static constraint generation with information obtained from static abstract interpretation and dynamic execution of the program. The strengthening comes in the form of additional linear constraints that trigger a series of simplifications in the solver, and make solving more scalable. We demonstrate the practical applicability of the approach by an experimental evaluation on a collection of challenging benchmark programs and comparisons with related tools based on abstract interpretation and software model checking.
previous article Model checking and abstract interpretation as building blocks of advanced program analysis techniques
next article Falsification of LTL safety properties in hybrid systems

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
1
Due to short running times, we present the aggregated data and do not provide any table containing entries for individual programs.
 
Literature
1.
Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis, In: Proc. POPL. ACM, pp. 1–3 (2002)
2.
Beyer, D., Henzinger, T., Majumdar, R., RybalchenkoA.: Invariant synthesis for combined theories. In: Proc. VMCAI. LNCS 4349. Springer, pp. 378–394 (2007a)
3.
Beyer, D., Henzinger, T. A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proc. PLDI. ACM Press, pp. 300–309 (2007b)
4.
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. PLDI. ACM, pp. 196–207 (2003)
5.
Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Proc. CAV. LNCS 2725. Springer, pp. 420–432 (2003)
6.
Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Proc. VMCAI. Springer, pp. 1–24 (2005)
7.
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL’78. ACM Press, pp. 84–96 (1978)
8.
de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Proc. TACAS. LNCS 4963. Springer, pp. 337–340 (2008)
9.
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Software Eng. 27(2), 1–25 (2001)
10.
Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science. AMS, pp. 19–32 (1967)
11.
Godefroid, P.: Compositional dynamic test generation. In: Proc. POPL. ACM, pp. 47–54 (2007)
12.
Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proc. PLDI. ACM, pp. 213–223 (2005)
13.
Gonnord, L., Halbwachs, N.: Combining widening and acceleration in Linear Relation Analysis. In: Proc. SAS. LNCS 4134. Springer, pp. 144–160 (2006)
14.
Gopan, D., Reps, T.: Lookahead widening. In: Proc. CAV. LNCS 4144. Springer, pp. 452–466 (2006)
15.
Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Proc. TACAS. LNCS 4963. Springer, pp. 443–458 (2008)
16.
Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI. ACM, pp. 281–292 (2008)
17.
Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Proc. TACAS (2009)
18.
19.
Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL 04: Principles of Programming Languages. ACM, pp. 232–244 (2004)
20.
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL. ACM, pp. 58–70 (2002)
21.
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)MATHCrossRef
22.
Holzbaur, C.: OFAI clp(q, r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, tR-95-09 (1995)
23.
Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: CAV. LNCS 4144. Springer, pp. 137–151 (2006)
24.
Kapur, D.: Automatically generating loop invariants using quantifier elimination. Tech. Rep. 05431 (Deduction and Applications), IBFI Schloss Dagstuhl (2006)
25.
Ku, K., Hart, T., Chechik, M., Lie, D.: A buffer overflow benchmark for software model checkers. In: Proc. ASE (2007)
26.
27.
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995)
28.
Miné, A.: The octagon abstract domain. Higher-Order and Symb. Comp. 19, 31–100 (2006)
29.
Necula, G. C., McPeak, S., Rahul, S. P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: Proc. CC. Springer, pp. 213–228 (2002)
30.
Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint-based linear-relations analysis. In: Proc. SAS. LNCS 3148. Springer, pp. 53–68 (2004a)
31.
Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: Proc. POPL. ACM, pp. 318–329 (2004b)
32.
Sankaranarayanan, S., Sipma, H., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Proc. VMCAI. LNCS 3385. Springer, pp. 25–41 (2005)
33.
Schrijver, A.: Theory of Linear and Integer Programming. Wiley,   (1986)MATH
34.
Sen, K., Marinov, D., Agha, G.: Cute: A concolic unit testing engine for C. In: Proc. FSE. ACM, pp. 263–272 (2005)
35.
The Intelligent Systems Laboratory.: SICStus Prolog User’s Manual. Swedish Institute of Computer Science, release 3.8.7 (2001)
Metadata
Title
From tests to proofs
Authors
Ashutosh Kumar Gupta
Rupak Majumdar
Andrey Rybalchenko
Publication date
01-08-2013
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 4/2013
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-012-0267-5

Other articles of this Issue 4/2013

International Journal on Software Tools for Technology Transfer 4/2013 Go to the issue

TACAS 2009

Falsification of LTL safety properties in hybrid systems

TACAS 2009

Static analysis for concurrent programs with applications to data race detection

Regular Paper

An integrated framework for checking the behaviour of fUML models using CSP

Introduction

Model checking and abstract interpretation as building blocks of advanced program analysis techniques

Regular Paper

A model-driven co-simulation environment for heterogeneous systems

TACAS 2009

Selected dynamic issues in software model checking

Premium Partner

    Image Credits