article

Lightweight Reasoning about Program Correctness

Authors:

Marsha Chechik,

Wei DingAuthors Info & Claims

Information Systems Frontiers, Volume 4, Issue 4

Pages 363 - 377

https://doi.org/10.1023/A:1020883625495

Published: 01 December 2002 Publication History

Abstract

Automated verification tools vary widely in the types of properties they are able to analyze, the complexity of their algorithms, and the amount of necessary user involvement. In this paper we propose a framework for step-wise automatic verification and describe a lightweight scalable program analysis tool that combines abstraction and model checking. The tool guarantees that its True and False answers are sound with respect to the original system. We also check the effectiveness of the tool on an implementation of the Safety-Injection System.

References

[1]

Bharadwaj R, Heitmeyer C. Model checking complete requirements specifications using abstraction. Journal of Automated Software Engineering 1999;6(1).

Digital Library

[2]

Bruns G, Godefroid P. Model checking partial state spaces with 3- valued temporal logics. In: Proceedings of CAV'99, vol. 1633 of LNCS, 1999:274-287.

[3]

Bruns G, Godefroid P. Generalized model checking: Reasoning about partial state spaces. In: Proceedings of CONCUR'00, vol. 877 of LNCS, 2000:168-182.

[4]

Bultan T, Gerber R, League C. Verifying systems with integer constraints and boolean predicates: A composite approach. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA'98), 1998:113-123.

Digital Library

[5]

Bultan T, Gerber R, League C. Composite model checking: Verification with type-specific symbolic representations. ACM Transactions on Software Engineering and Methodology 2000;9(1):3-50.

Digital Library

[6]

Bultan T, Gerber R, Pugh W. Model checking concurrent systems with unbounded integer variables: Symbolic representations, approximations and experimental results. ACM Transactions on Programming Languages and Systems, 1999.

Digital Library

[7]

Chan W, Anderson RJ, Beame P, Jones DH, Notkin D, Warner WE. Decoupling synchronization from local control for efficient symbolic model checking of statecharts. In: Proceedings of the 1999 International Conference on Software Engineering (ICSE'99), 1999:142-151.

Digital Library

[8]

Chechik M, Easterbrook S, Petrovykh V. Model-checking over multi-valued logics. In: Proceedings of Formal Methods Europe (FME'01), vol. 2021 of LNCS, Springer, 2001:72- 98.

[9]

Clarke E, Emerson E, Sistla A. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 1986;8(2):244-263.

Digital Library

[10]

Clarke E, Grumberg O, Hiraishi H, Jha S, Long D, McMillan K, Ness L. Verification of the futurebus+ cache coherence protocol. In: Formal Methods in System Design 1995;6:217- 232.

Digital Library

[11]

Clarke EM, Grumberg O, Long DE. Model checking and abstraction. IEEE Transactions on Programming Languages and Systems 1994;19(2).

Digital Library

[12]

Colon M, Uribe T. Generating finite-state abstractions of reactive systems using decision procedures. In: Proceedings of the 10th Conference on Computer-Aided Verification, vol. 1427 of LNCS. Springer-Verlag, 1980.

Digital Library

[13]

Corbett J, Dwyer M, Hatcliff J, Laubach S, Pasareanu C, Robby, Zheng H. Bandera: Extracting finite-state models from Java Source code. In: Proceedings of 22nd International Conference on Software Engineering, 2000.

Digital Library

[14]

Courtois P-J, Parnas DL. Documentation for safety critical software. In: Proceedings of the 15th International Conference on Software Engineering, 1993:315-323.

Digital Library

[15]

Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Proceedings of the "Colloque sur la Programmation" , 1976.

[16]

Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th POPL, Los Angeles, California, 1977:238-252.

Digital Library

[17]

Cousot P, Cousot R. Refining model checking by abstract interpretation. Authomated Software Engineering, special issue on Automated Software Analysis 1999;6:69-95.

Digital Library

[18]

Dams D, Gerth R, Grumberg O. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems 1997;2(19):253-291.

Digital Library

[19]

Dams D, Grumberg O, Gerth R. Abstract interpretation of reactive system: Abstraction-preserving ¿CTL^*, CTL^* and CTL^*, North-Holland, 1994:573-592.

[20]

Demartini C, Iosif R, Sisto R. dSPIN: A dynamic extension of SPIN. In: Proceedings of the 6th SPIN Workshop on Practical Aspects of Model-Checking, 1999.

[21]

Dill D. The Murø verification system. In: Alur R, Henzinger T, eds. Computer-Aided Verification Computer, vol. 1102 of Lecture Notes in Computer Science, New York, N.Y. Springer-Verlag, 1996:390-393.

Digital Library

[22]

Ding W. Analyzing infinite-state programs with abstract interpretation. Master's Thesis, University of Toronto, Department of Computer Science, 2000.

[23]

Dwyer M, Carr V, Hines L. Model checking graphical user interfaces using abstractions. In: Proceedings of Foundations of Software Engineering, Zurich, Switzerland, 1997.

Digital Library

[24]

Godefroid P. VeriSoft: A tool for the automatic analysis of concurrent reactive software. In: Proceedings of CAV'97, 1997:476-479.

Digital Library

[25]

Havelund K, Pressburger T. Model checking Java programs using Java pathfinder. International Journal on Software Tools for Technology Transfer, 1999.

[26]

Holzmann G. The model checker SPIN. IEEE Transactions on Software Engineering 1997;23(5):279-295.

Digital Library

[27]

Holzmann G. A practical method for verifying event-driven software. In: Proceedings of the 21st International Conference on Software Engineering (ICSE'99), 1999:597-607.

Digital Library

[28]

Huth M, Jagadeesan R, Schmidt DA. Modal transition systems: A foundation for three-valued program analysis. In: Proceedings of 10th European Symposium on Programming (ESOP), vol. 2028 of LNCS, Springer, 2001:155-169.

[29]

Jackson D. Abstract model checking of infinite specifications. In: Proceedings of FME'94: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, 1994:519-531.

Digital Library

[30]

Jackson D, Wing J. Lightweight formal methods. IEEE Computer, 1996.

[31]

Janssen W, Mateescu R, Mauw S, Fennema P, van der Stappen P. Model checking for managers. In: Theoretical and Practical Aspects of SPIN Model Checking, vol. 1680 of LNCS, Springer-Verlag, 1999:92-107.

[32]

Kamel M, Leue S. Validation of remote object invocation and object migration in CORBA GIOP using Promela/Spin. In: Proceedings of the 4th International SPIN Workshop (SPIN'4), Paris, France, 1998.

[33]

Kelb P, Dams D, Gerth R. Practical symbolic model checking of the full µ-calculus using compositional abstractions. Technical Report 95-31, Department of Computer Science, Eindhoven University of Technology, 1995.

[34]

Kelly W, Maslov V, Pugh W, Rosser E, Shpeisman T, Wonnacott D. The Omega calculator and library, version 1.1.0. Technical Report, University of Maryland, 1996.

[35]

Kleene SC. Introduction to metamathematics. New York: Van Nostrand, 1952.

[36]

Kozen D. Results on the propositional µ-calculus. Theoretical Computer Science 1983;27:334-354.

[37]

Larsen K, Thomsen B. A modal process logic. In: Third Annual Symposium on Logic in Computer Sciences, IEEE Computer Society Press, 1988:203-210.

[38]

McMillan K. Symbolic model checking. Dordrecht: Kluwer Academic, 1993.

Digital Library

[39]

Norrish M. An abstract dynamic semantics for C. Technical Report TR421- mn200, University of Cambridge Computer Laboratory, 1997.

[40]

Oppen D. A 2² ² ^pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences 1978;16(3):323-332.

[41]

Pardo A, Hachtel GD. Automatic abstraction techniques for propositional µ-calculus model checking. In: Proceedings of 9th International Conference on Computer-Aided Verification (CAV'97), vol. 1254 of LNCS, Springer-Verlag, 1997:12- 23.

Digital Library

[42]

Pugh W. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Comm. of the ACM, 1992.

[43]

Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3- valued logic. In: Proceedings of 26th Annual ACM Symposium on Principles of Programming Languages, 1999.

Digital Library

[44]

Saidi H. Modular and incremental analysis of concurrent software systems. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering, 1999:92- 101.

Digital Library

[45]

Somenzi F. Binary decision diagrams. In Broy M, Steinbrüggen R, eds. Calculational System Design, vol. 173 of NATO Science Series F: Computer and Systems Sciences, IOS Press, 1999:303- 366.

[46]

Sreemani T, Atlee JM. Feasibility of model checking software requirements: A case study. In: Proceedings of COMPASS'96, Gaithersburg, Maryland, 1996.

[47]

Visser W, Park S, Penix J. Applying predicate abstraction to model check object-oriented programs. In: Proceedings of 4th International Workshop on Formal Methods in Software Practice, 2000.

Digital Library

Cited By

Easterbrook SChechik MDevereux BGurfinkel ALai APetrovykh VTafliovich AThompson-Walsh CClarke LDillon LTichy W(2003)χChekProceedings of the 25th International Conference on Software Engineering10.5555/776816.776960(804-805)Online publication date: 3-May-2003
https://dl.acm.org/doi/10.5555/776816.776960
Chechik MDevereux BEasterbrook SGurfinkel A(2003)Multi-valued symbolic model-checkingACM Transactions on Software Engineering and Methodology (TOSEM)10.1145/990010.99001112:4(371-408)Online publication date: 1-Oct-2003
https://dl.acm.org/doi/10.1145/990010.990011

Index Terms

Lightweight Reasoning about Program Correctness
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Correctness witnesses: exchanging verification results between verifiers
FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Standard verification tools provide a counterexample to witness a specification violation, and, since a few years, such a witness can be validated by an independent validator using an exchangeable witness format. This way, information about the ...
Temporal property verification as a program analysis task

We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by ...
Finding feasible abstract counter-examples

A strength of model checking is its ability to automate the detection of subtle system errors and produce traces that exhibit those errors. Given the high-computational cost of model checking most researchers advocate the use of aggressive property-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Information Systems Frontiers

Information Systems Frontiers Volume 4, Issue 4

December 2002

61 pages

ISSN:1387-3326

Issue’s Table of Contents

Copyright © Copyright © 2002 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 December 2002

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Easterbrook SChechik MDevereux BGurfinkel ALai APetrovykh VTafliovich AThompson-Walsh CClarke LDillon LTichy W(2003)χChekProceedings of the 25th International Conference on Software Engineering10.5555/776816.776960(804-805)Online publication date: 3-May-2003
https://dl.acm.org/doi/10.5555/776816.776960
Chechik MDevereux BEasterbrook SGurfinkel A(2003)Multi-valued symbolic model-checkingACM Transactions on Software Engineering and Methodology (TOSEM)10.1145/990010.99001112:4(371-408)Online publication date: 1-Oct-2003
https://dl.acm.org/doi/10.1145/990010.990011

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents