{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T17:07:31Z","timestamp":1774631251802,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540421245","type":"print"},{"value":"9783540451396","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_7","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T14:39:56Z","timestamp":1186756796000},"page":"102-122","source":"Crossref","is-referenced-by-count":183,"title":["Automatically validating temporal safety properties of interfaces"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 01: Programming Language Design and Implementation (to appear). ACM, 2001.","DOI":"10.1145\/378795.378846"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In TACAS 01: Tools and Algorithms for Construction and Analysis of Systems(to appear). Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45319-9_19"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN 00: SPIN Workshop","author":"T. Ball","year":"2000","unstructured":"T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for Boolean programs. In SPIN 00: SPIN Workshop, LNCS 1885, pages 113\u2013130. Springer-Verlag, 2000."},{"key":"7_CR4","unstructured":"D. Blei and et al. Vampyre: A proof generating theorem prover \u2014 http:\/\/www.eecs.berkeley.edu\/ rupak\/vampyre ."},{"issue":"8","key":"7_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"7","key":"7_CR6","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W. R. Bush","year":"2000","unstructured":"W. R. Bush, J. D. Pincus, and D. J. Sielaff. A static analyzer for finding dynamic programming errors. Software-Practice and Experience, 30(7):775\u2013802, June 2000.","journal-title":"Software-Practice and Experience"},{"key":"7_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"CAV 00: Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV 00: Computer Aided Verification, LNCS 1855, pages 154\u2013169. Springer-Verlag, 2000."},{"key":"7_CR8","unstructured":"J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In ICSE 2000: International Conference on Software Engineering, pages 439\u2013448. ACM, 2000."},{"key":"7_CR9","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a uni_ed lattice model for the static analysis of programs by construction or approximation of fix points. In POPL 77: Principles of Programming Languages, pages 238\u2013252. ACM, 1977."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Temporal abstract interpretation. In POPL 00: Principles of Programming Languages, pages 12\u201325. ACM, 2000.","DOI":"10.1145\/325694.325699"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"M. Das. Unification-based pointer analysis with directional assignments. In PLDI 00: Programming Language Design and Implementation, pages 35\u201346. ACM, 2000.","DOI":"10.1145\/349299.349309"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"R. DeLine and M. F\u00e4hndrich. Enforcing high-level protocols in low-level software In PLDI 01: Programming Language Design and Implementation(to appear). ACM, 2001.","DOI":"10.1145\/378795.378811"},{"key":"7_CR13","unstructured":"D. Detlefs, G. Nelson, and J. Saxe. Simplify theorem prover \u2014 http:\/\/research.compaq.com\/src\/esc\/simplify.html ."},{"key":"7_CR14","unstructured":"D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report Research Report 159, Compaq Systems Research Center, December 1998."},{"key":"7_CR15","unstructured":"E. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"M. Dwyer and L. Clarke. Data flow analysis for verifying properties of concurrent programs. In FSE 94: Foundations of Software Engineering, pages 62\u201375. ACM, 1994.","DOI":"10.1145\/193173.195295"},{"key":"7_CR17","unstructured":"M. Dwyer, J. Hatcliff, R. Joehanes, S. Laubach, C. Pasareanu, Robby, W. Visser, and H. Zheng. Tool-supported program abstraction for finite-state verification. In ICSE 01: Software Engineering (to appear), 2001."},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI 00: Operating System Design and Implementation. Usenix Association, 2000.","DOI":"10.21236\/ADA419626"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"C. Flanagan, R. Joshi, and K. R. M. Leino. Annotation inference for modular checkers. Information Processing Letters (to appear), 2001.","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"7_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"CAV 97: Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In CAV 97: Computer Aided Verification, LNCS 1254, pages 72\u201383. Springer-Verlag, 1997."},{"issue":"5","key":"7_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The Spin model checker. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1007\/10722468_8","volume-title":"SPIN 00: SPIN Workshop","author":"G. Holzmann","year":"2000","unstructured":"G. Holzmann. Logic verification of ANSI-C code with Spin. In SPIN 00: SPIN Workshop, LNCS 1885, pages 131\u2013147. Springer-Verlag, 2000."},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-aided Verification of Coordinating Processes. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"issue":"2","key":"7_CR24","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125\u2013143, 1977.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"7_CR25","series-title":"Lect Notes Comput Sci","first-page":"302","volume-title":"CC 98: Compiler Construction","author":"K. R. M. Leino","year":"1998","unstructured":"K. R. M. Leino and G. Nelson. An extended static checker for Modula-3. In CC 98: Compiler Construction, LNCS 1383, pages 302\u2013305. Springer-Verlag, 1998."},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"G. Necula. Proof carrying code. In POPL 97: Principles of Programming Languages, pages 106\u2013119. ACM, 1997.","DOI":"10.1145\/263699.263712"},{"key":"7_CR27","unstructured":"G. Nelson. Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981."},{"key":"7_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"CAV 96: Computer-Aided Verification","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In CAV 96: Computer-Aided Verification, LNCS 1102, pages 411\u2013414. Springer-Verlag, 1996."},{"key":"7_CR29","unstructured":"J. Pincus. personal communication, October 2000."},{"issue":"8","key":"7_CR30","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102\u2013114, August 1992.","journal-title":"Communications of the ACM"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL 95: Principles of Programming Languages, pages 49\u201361. ACM, 1995.","DOI":"10.1145\/199448.199462"},{"key":"7_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"CAV 99: Computer-aided Verification","author":"H. Saidi","year":"1999","unstructured":"H. Saidi and N. Shankar. Abstract and model check while you prove. In CAV 99: Computer-aided Verification, LNCS 1633, pages 443\u2013454. Springer-Verlag, 1999."},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"D. Schmidt. Data flow analysis is model checking of abstract interpretation. In POPL 98: Principles of Programming Languages, pages 38\u201348. ACM, 1998.","DOI":"10.1145\/268946.268950"},{"key":"7_CR34","unstructured":"M. Sharir and A. Pnueli. Two approaches to interprocedural data dalow analysis. In Program Flow Analysis: Theory and Applications, pages 189\u2013233. Prentice-Hall, 1981."},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"N. Suzuki and K. Ishihata. Implementation of an array bound checker. In POPL 77: Principles of Programming Languages, pages 132\u2013143. ACM, 1977.","DOI":"10.1145\/512950.512963"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Z. Xu, B. P. Miller, and T. Reps. Safety checking of machine code. In PLDI 00: Programming Language Design and Implementation, pages 70\u201382. ACM, 2000.","DOI":"10.1145\/349299.349313"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T22:17:28Z","timestamp":1556749048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}