research-article

Open access

A type system equivalent to a model checker

Authors:

Jens PalsbergAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 5

Article No.: 29, Pages 1 - 24

https://doi.org/10.1145/1387673.1387678

Published: 04 September 2008 Publication History

Abstract

Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a semantic and whole-program style. This difference between the two approaches makes them complementary to each other: type systems are good at explaining why a program was accepted while model checkers are good at explaining why a program was rejected.

We present a type system that is equivalent to a model checker for verifying temporal safety properties of imperative programs. The model checker is natural and may be instantiated with any finite-state abstraction scheme such as predicate abstraction. The type system, which is also parametric, type checks exactly those programs that are accepted by the model checker. It uses a variant of function types to capture flow sensitivity and intersection and union types to capture context sensitivity. Our result sheds light on the relationship between type systems and model checking, provides a methodology for studying their relative expressiveness, is a step towards sharing results between the two approaches, and motivates synergistic program analyses involving interplay between them.

References

[1]

Amadio, R. M. and Cardelli, L. 1993. Subtyping recursive types. ACM Trans. Program. Lang. Syst. 15, 4, 575--631.

Digital Library

[2]

Amtoft, T. and Turbak, F. 2000. Faithful translations between polyvariant flows and polymorphic types. In Proceedings of the 14th European Symposium on Programming. Springer, 26--40.

Digital Library

[3]

Ball, T. and Rajamani, S. 2002. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1--3.

Digital Library

[4]

Banerjee, A. 1997. A modular, polyvariant and type-based closure analysis. In Proceedings of the 2nd ACM SIGPLAN International Conf. on Functional Programming. ACM Press, 1--10.

Digital Library

[5]

Beaven, M. and Stansifer, R. 1993. Explaining type errors in polymorphic languages. ACM Lett. on Program. Lang. Syst. 2, 1-4, 17--30.

Digital Library

[6]

Brylow, D. and Palsberg, J. 2004. Deadline analysis of interrupt-driven software. IEEE Trans. Soft. Engin. 30, 10, 634--655.

Digital Library

[7]

Chaki, S., Clarke, E. M., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In Proceedings of the 25th International on Software Engineering. IEEE Computer Society Press, 385--395.

Digital Library

[8]

Chaki, S., Rajamani, S. K., and Rehof, J. 2002. Types as models: Model checking message-passing programs. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 45--57.

Digital Library

[9]

Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., and Palsberg, J. 2004. Stack size analysis of interrupt driven software. Inform. Comput. 194, 2, 144--174.

Digital Library

[10]

Chitil, O. 2001. Compositional explanation of types and algorithmic debugging of type errors. In Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming. 193--204.

Digital Library

[11]

Cousot, P. 1997. Types as abstract interpretations. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 316--331.

Digital Library

[12]

Cousot, P. and Cousot, R. 2000. Temporal abstract interpretation. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 12--25.

Digital Library

[13]

Debbabi, M., Benzakour, A., and Ktari, B. 1999. A synergy between model-checking and type inference for the verification of value-passing higher-order processes. In Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology. Springer, 214--230.

Digital Library

[14]

DeLine, R. and Fahndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 59--69.

Digital Library

[15]

Duggan, D. and Bent, F. 1996. Explaining type inference. Sci. Comput. Program. 27, 1, 37--83.

Digital Library

[16]

Flanagan, C. and Freund, S. N. 2004. Type inference against races. Sci. Comput. Program. 64, 1, 140--165.

Digital Library

[17]

Flanagan, C., Freund, S. N., and Lifshin, M. 2005. Type inference for atomicity. In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation. ACM Press, 47--58.

Digital Library

[18]

Foster, J. S., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 1--12.

Digital Library

[19]

Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer-Aided Verification. Springer, 72--83.

Digital Library

[20]

Haack, C. and Wells, J. B. 2003. Type error slicing in implicitly typed higher-order languages. In Proceedings of the 12th European Symposium on Programming. Springer, 284--301.

Digital Library

[21]

Heintze, N. 1995. Control-flow analysis and type systems. In Proceedings of the 2nd International Symposium on Static Analysis. Springer, 189--206.

Digital Library

[22]

Henzinger, T. A., Jhala, R., Majumdar, R., Necula, G. C., Sutre, G., and Weimer, W. 2002. Temporal-safety proofs for systems code. In Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 526--538.

Digital Library

[23]

Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with Blast. In Proceedings of the 10th International SPIN Workshop on Model Checking Software. Springer, 235--239.

Digital Library

[24]

Igarashi, A. and Kobayashi, N. 2002. Resource usage analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 331--342.

Digital Library

[25]

Johnson, G. F. and Walz, J. A. 1986. A maximium flow approach to anomaly isolation in unification-based incremental type inference. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages. ACM Press, 44--57.

Digital Library

[26]

Lerner, B., Flower, M., Grossman, D., and Chambers, C. 2007. Searching for type-error messages. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 425--434.

Digital Library

[27]

Ma, D. 2004. Bounding the stack size of interrupt-driven programs. Ph.D. thesis, Purdue University.

Digital Library

[28]

Mandelbaum, Y., Walker, D., and Harper, R. 2003. An effective theory of type refinements. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming. ACM Press, 213--225.

Digital Library

[29]

Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.

[30]

Mossin, C. 1997. Exact flow analysis. In Proceedings of the 4th International Symposium on Static Analysis. Springer, 250--264.

Digital Library

[31]

Naik, M. 2004. A type system equivalent to a model checker. M.S. thesis, Purdue University.

[32]

Namjoshi, K. S. 2001. Certifying model checkers. In Proceedings of the 13th International Conference on Computer-Aided Verification. Springer, 2--12.

Digital Library

[33]

Namjoshi, K. S. 2003. Lifting temporal proofs through abstractions. In Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 174--188.

Digital Library

[34]

Palsberg, J. 1998. Equality-based flow analysis versus recursive types. ACM Trans. Program. Lang. Syst. 20, 6, 1251--1264.

Digital Library

[35]

Palsberg, J. and Ma, D. 2002. A typed interrupt calculus. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems. Springer, 291--310.

Digital Library

[36]

Palsberg, J. and O'Keefe, P. M. 1995. A type system equivalent to flow analysis. ACM Trans. Program. Lang. Syst. 17, 4, 576--599.

Digital Library

[37]

Palsberg, J. and Pavlopoulou, C. 2001. From polyvariant flow information to intersection and union types. J. Funct. Program. 11, 3, 263--317.

Digital Library

[38]

Palsberg, J. and Smith, S. 1996. Constrained types and their expressiveness. ACM Transactions Program. Lang. Syst. 18, 5, 519--527.

Digital Library

[39]

Peled, D., Pnueli, A., and Zuck, L. D. 2001. From falsification to verification. In Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science. Springer, 292--304.

Digital Library

[40]

Peled, D. and Zuck, L. D. 2001. From model checking to a temporal proof. In Proceedings of the 8th International SPIN Workshop on Model Checking Software. Springer, 1--14.

Digital Library

[41]

Schmidt, D. and Steffen, B. 1998. Program analysis as model checking of abstract interpretations. In Proceedings of the 5th International Symposium on Static Analysis. Springer, 351--380.

[42]

Schmidt, D. A. 1998. Data flow analysis is model checking of abstract interpretations. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 38--48.

Digital Library

[43]

Steffen, B. 1991. Data flow analysis as model checking. In Proceedings of Theoretical Aspects of Computer Science. Springer, 346--364.

Digital Library

[44]

Tan, L. and Cleaveland, R. 2002. Evidence-based model checking. In Proceedings of the 14th International Conference on Computer-Aided Verification. Springer, 455--470.

Digital Library

[45]

Tip, F. and Dinesh, T. B. 2001. A slicing-based approach for locating type errors. ACM Trans. Soft. Engin. Method. 10, 1, 5--55.

Digital Library

[46]

Walker, D. and Morrisett, G. 2001. Alias types for recursive data structures. In Proceedings of the 3rd International Workshop on Types in Compilation. Springer, 177--206.

Digital Library

[47]

Wand, M. 1986. Finding the source of type errors. In Proceedings of the 13th ACM Symposium on Principles of Programming Languages. ACM Press, 38--43.

Digital Library

[48]

Xi, H. 2000. Imperative programming with dependent types. In Proceedings of the 15th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 375--387.

Digital Library

Cited By

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Dutt SNandi STrivedi G(2017)Analysis and Design of Adders for Approximate ComputingACM Transactions on Embedded Computing Systems10.1145/313127417:2(1-28)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3131274
Lu SLysecky R(2017)Time and Sequence Integrated Runtime Anomaly Detection for Embedded SystemsACM Transactions on Embedded Computing Systems10.1145/312278517:2(1-27)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3122785
Show More Cited By

Index Terms

A type system equivalent to a model checker
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
      2. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Proof theory
    2. Verification by model checking

Recommendations

The software model checker Blast: Applications to software engineering

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path ...
The software model checker Blast

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path ...
A type system equivalent to a model checker
ESOP'05: Proceedings of the 14th European conference on Programming Languages and Systems

Type systems and model checking are two prevalent approaches to program verification. A prominent difference between them is that type systems are typically defined in a syntactic and modular style whereas model checking is usually performed in a ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 5

August 2008

193 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1387673

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2008

Accepted: 01 December 2007

Revised: 01 September 2007

Received: 01 November 2005

Published in TOPLAS Volume 30, Issue 5

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
818
Total Downloads

Downloads (Last 12 months)72
Downloads (Last 6 weeks)10

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
Dutt SNandi STrivedi G(2017)Analysis and Design of Adders for Approximate ComputingACM Transactions on Embedded Computing Systems10.1145/313127417:2(1-28)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3131274
Lu SLysecky R(2017)Time and Sequence Integrated Runtime Anomaly Detection for Embedded SystemsACM Transactions on Embedded Computing Systems10.1145/312278517:2(1-27)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3122785
Akazaki THasuo ISuenaga K(2015)Input Synthesis for Sampled Data Systems by Program LogicElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.174.3174(22-39)Online publication date: 22-Jan-2015
https://doi.org/10.4204/EPTCS.174.3
Salvati SWalukiewicz I(2015)Typing Weak MSOL PropertiesFoundations of Software Science and Computation Structures10.1007/978-3-662-46678-0_22(343-357)Online publication date: 2015
https://doi.org/10.1007/978-3-662-46678-0_22
Kaki GJagannathan S(2014)A relational framework for higher-order shape analysisACM SIGPLAN Notices10.1145/2692915.262815949:9(311-324)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628159
Angiuli CMorehouse ELicata DHarper R(2014)Homotopical patch theoryACM SIGPLAN Notices10.1145/2692915.262815849:9(243-256)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628158
Schlesinger CGreenberg MWalker D(2014)Concurrent NetCoreACM SIGPLAN Notices10.1145/2692915.262815749:9(11-24)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628157
Nguyen PTobin-Hochstadt SVan Horn D(2014)Soft contract verificationACM SIGPLAN Notices10.1145/2692915.262815649:9(139-152)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628156
Chen SErwig M(2014)Type-based parametric analysis of program familiesACM SIGPLAN Notices10.1145/2692915.262815549:9(39-51)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628155
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Figures

Tables

Media

View Issue’s Table of Contents