Article

Sufficient preconditions for modular assertion checking

Author:

Yannick MoyAuthors Info & Claims

VMCAI'08: Proceedings of the 9th international conference on Verification, model checking, and abstract interpretation

Pages 188 - 202

Published: 07 January 2008 Publication History

Abstract

Assertion checking is the restriction of program verification to validity of program assertions. It encompasses safety checking, which is program verification of safety properties, like memory safety or absence of overflows. In this paper, we consider assertion checking of program parts instead of whole programs, which we call modular assertion checking. Classically, modular assertion checking is possible only if the context in which a program part is executed is known. By default, the worst-case context must be assumed, which may impair the verification task. It usually takes user effort to detail enough the execution context for the verification task to succeed, by providing strong enough preconditions. We propose a method to automatically infer sufficient preconditions in the context of modular assertion checking of imperative pointer programs. It combines abstract interpretation, weakest precondition calculus and quantifier elimination. We instantiate this method to prove memory safety for C and Java programs, under some memory separation conditions.

References

[1]

Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol. 2304, pp. 159-178. Springer, London (2002).

Digital Library

[2]

http://www.lri.fr/~moy/publis/moy08vmcai-ext.pdf

[3]

Filliâtre, J.C.,Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, Springer, Heidelberg (2007).

Digital Library

[4]

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. POPL 1978, pp. 84-96. ACM, New York (1978).

Digital Library

[5]

Suzuki, N., Ishihata, K.: Implementation of an array bound checker. In: Proc. POPL 1977, pp. 132-143. ACM, New York (1977).

Digital Library

[6]

Xu, Z., Miller, B.P., Reps, T.: Safety checking of machine code. ACM SIGPLAN Notices 35(5), 70-82 (2000).

Digital Library

[7]

Xu, Z.: Safety checking of machine code. PhD thesis, Univ. of Wisconsin, Madison (2000).

Digital Library

[8]

Bourdoncle, F.: Assertion-based debugging of imperative programs by abstract interpretation. In: Sommerville, I., Paul, M. (eds.) ESEC 1993. LNCS, vol. 717, pp. 501-516. Springer, London (1993).

Digital Library

[9]

Rival, X.: Understanding the origin of alarms in ASTRÉE. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 303-319. Springer, London (2005).

Digital Library

[10]

Gulwani, S., Tiwari, A.: Assertion checking unified. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, Springer, Heidelberg (2007).

Digital Library

[11]

International Organization for Standardization (ISO) (The ANSI C standard (C99)).

[12]

Aiken, A., et al.: Checking and inferring local non-aliasing. In: Proc. PLDI 2003, pp. 129- 140. ACM, New York (2003).

Digital Library

[13]

Koes, D., Budiu, M., Venkataramani, G.: Programmer specified pointer independence. In: MSP 2004, pp. 51-59. ACM, New York (2004).

Digital Library

[14]

Calcagno, C., et al.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, Springer, Heidelberg (2007).

Digital Library

[15]

Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119-134. Springer, Heidelberg (2005).

Digital Library

[16]

Leino, K.R.M., Logozzo, F.: Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain. Technical Report RISC-Linz Report Series No. 07-07, RISC, Hagenberg, Austria, Proc. WING 2007 (2007).

[17]

Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 147-166. Springer, Heidelberg (2007).

Digital Library

[18]

Wagner, D., et al.: A first step towards automated detection of buffer overrun vulnerabilities. In: NDSS Symposium, San Diego, CA, pp. 3-17 (2000).

[19]

Dor, N., Rodeh, M., Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Proc. PLDI 2003, pp. 155-167. ACM Press, New York (2003).

Digital Library

[20]

Allamigeon, X., Godard, W., Hymans, C.: Static analysis of string manipulations in critical embedded C programs. In: SAS. LNCS, pp. 35-51. Springer, Heidelberg (2006).

Digital Library

[21]

Filliâtre, J.C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15-29. Springer, Heidelberg (2004).

[22]

Moy, Y., Marché, C.: Inferring local (non-)aliasing and strings for memory safety. In: Heap Analysis and Verification (HAV 2007), Braga, Portugal (2007).

[23]

APRON numerical abstract domain library, http://apron.cri.ensmp.fr/

[24]

Barnett, M., et al.: Boogie: A modular reusable verifier for object-oriented programs. In: FMCO, Springer, Heidelberg (2005).

Digital Library

[25]

MINIX 3 Operating System, http://www.minix3.org/

[26]

Ku, K., et al.: A buffer overflow benchmark for software model checkers. In: Proc. ASE 2007 (2007).

Digital Library

[27]

Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proc. POPL 2007, pp. 97-108. ACM, Nice, France (2007).

Digital Library

Cited By

Ferles KWüstholz VChristakis MDillig IBodden ESchäfer WDeursen AZisman A(2017)Failure-directed program trimmingProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106249(174-185)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106249
Padhi SSharma RMillstein T(2016)Data-driven precondition inference with learned featuresACM SIGPLAN Notices10.1145/2980983.290809951:6(42-56)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908099
Padhi SSharma RMillstein TKrintz CBerger E(2016)Data-driven precondition inference with learned featuresProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908099(42-56)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2908080.2908099
Show More Cited By

Sufficient preconditions for modular assertion checking

Recommendations

Modular Model Checking
COMPOS'97: Revised Lectures from the International Symposium on Compositionality: The Significant Difference

In modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...
Context-sensitive multivariant assertion checking in modular programs
LPAR'06: Proceedings of the 13th international conference on Logic for Programming, Artificial Intelligence, and Reasoning

We propose a modular, assertion-based system for verification and debugging of large logic programs, together with several interesting models for checking assertions statically in modular programs, each with different characteristics and representing ...
Performance assertion checking

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

VMCAI'08: Proceedings of the 9th international conference on Verification, model checking, and abstract interpretation

January 2008

324 pages

ISBN:3540781625

Editors:
Francesco Logozzo,
Doron A. Peled
Bar-Ilan University, Department of Computer Science, Ramat Gan, Israel
,
Lenore D. Zuck
University of Illinois at Chicago, Department of Computer Science, Chicago, IL

Sponsors

Microsoft: Microsoft
University of Illinois: University of Illinois

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 January 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
13
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ferles KWüstholz VChristakis MDillig IBodden ESchäfer WDeursen AZisman A(2017)Failure-directed program trimmingProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106249(174-185)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106249
Padhi SSharma RMillstein T(2016)Data-driven precondition inference with learned featuresACM SIGPLAN Notices10.1145/2980983.290809951:6(42-56)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908099
Padhi SSharma RMillstein TKrintz CBerger E(2016)Data-driven precondition inference with learned featuresProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908099(42-56)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2908080.2908099
Logozzo FLahiri SFähndrich MBlackshear S(2014)Verification modulo versionsACM SIGPLAN Notices10.1145/2666356.259432649:6(294-304)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2666356.2594326
Logozzo FLahiri SFähndrich MBlackshear SO'Boyle MPingali K(2014)Verification modulo versionsProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2594291.2594326(294-304)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2594291.2594326
Lopes NMonteiro J(2014)Weakest Precondition Synthesis for Compiler OptimizationsProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_12(203-221)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_12
Seghir MKroening D(2013)Counterexample-Guided precondition inferenceProceedings of the 22nd European conference on Programming Languages and Systems10.1007/978-3-642-37036-6_25(451-471)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-37036-6_25
Cousot PCousot RFähndrich MLogozzo F(2013)Automatic Inference of Necessary PreconditionsProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_10(128-148)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_10
(2012)FASTProceedings of the Tenth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2012.6292298(33-42)Online publication date: 1-Jul-2012
https://dl.acm.org/doi/10.1109/MEMCOD.2012.6292298
Cousot PCousot RLogozzo F(2011)Precondition inference from intermittent assertions and application to contracts on collectionsProceedings of the 12th international conference on Verification, model checking, and abstract interpretation10.5555/1946284.1946296(150-168)Online publication date: 23-Jan-2011
https://dl.acm.org/doi/10.5555/1946284.1946296
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents