{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:46Z","timestamp":1761597226939},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223429"},{"type":"electronic","value":"9783540278139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27813-9_2","type":"book-chapter","created":{"date-parts":[[2010,9,14]],"date-time":"2010-09-14T04:57:57Z","timestamp":1284440277000},"page":"15-30","source":"Crossref","is-referenced-by-count":30,"title":["Static Program Analysis via 3-Valued Logic"],"prefix":"10.1007","author":[{"given":"Thomas W.","family":"Reps","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Wilhelm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Softw. Tools for Tech. Transfer\u00a02 (2000)","DOI":"10.1007\/s100090050043"},{"key":"2_CR2","unstructured":"Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. Network and Dist. Syst. Security (2000)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. Op. Syst. Design and Impl., 1\u201316 (2000)","DOI":"10.21236\/ADA419626"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Z.H.: Bandera: Extracting finite-state models from Java source code. In: Int. Conf. on Softw. Eng., pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"2_CR5","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. Bush","year":"2000","unstructured":"Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Software\u2013Practice&Experience\u00a030, 775\u2013802 (2000)","journal-title":"Software\u2013Practice&Experience"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Chen, H., Wagner, D.: MOPS: An infrastructure for examining security properties of software. In: Conf. on Comp. and Commun. Sec., pp. 235\u2013244 (2002)","DOI":"10.1145\/586139.586142"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Andersen, L.O.: Binding-time analysis and the taming of C pointers. Part. Eval. and Semantics-Based Prog. Manip., 47\u201358 (1993)","DOI":"10.1145\/154630.154636"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Steensgaard, B.: Points-to analysis in almost-linear time. Princ. of Prog. Lang., 32\u201341 (1996)","DOI":"10.1145\/237721.237727"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Das, M.: Unification-based pointer analysis with directional assignments. Prog. Lang. Design and Impl., 35\u201346 (2000)","DOI":"10.1145\/358438.349309"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Rehof, J., Das, M.: Scalable context-sensitive flow analysis using instantiation constraints. Prog. Lang. Design and Impl., 253\u2013263 (2000)","DOI":"10.1145\/358438.349332"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Cheng, B.C., Hwu, W.: Modular interprocedural pointer analysis using access paths: Design, implementation, and evaluation. Prog. Lang. Design and Impl., 57\u201369 (2000)","DOI":"10.1145\/358438.349311"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Foster, J., F\u00e4hndrich, M., Aiken, A.: Polymorphic versus monomorphic flow-insensitive points-to analysis for C. In: Static Analysis Symp., pp. 175\u2013198 (2000)","DOI":"10.1007\/978-3-540-45099-3_10"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Whaley, J., Lam, M.: Cloning-based context-sensitive pointer alias analyses using binary decision diagrams. Prog. Lang. Design and Impl (2004) (to appear)","DOI":"10.1145\/996841.996859"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Zhu, J., Calman, S.: Symbolic pointer analysis revisited. Prog. Lang. Design and Impl (2004) (to appear)","DOI":"10.1145\/996841.996860"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Das, M., Liblit, B., F\u00e4hndrich, M., Rehof, J.: Estimating the impact of scalable pointer analysis on optimization. In: Static Analysis Symp., pp. 260\u2013278 (2001)","DOI":"10.1007\/3-540-47764-0_15"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst.\u00a024, 217\u2013298 (2002)","journal-title":"Trans. on Prog. Lang. and Syst."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. Princ. of Prog. Lang., 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280\u2013301 (2000)","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"2_CR20","unstructured":"TVLA system , http:\/\/www.math.tau.ac.il\/~rumster\/TVLA\/"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Gopan, D., DiMaio, F.: Numeric domains with summarized dimensions. Tools and Algs. for the Construct. and Anal. of Syst., 512\u2013529 (2004)","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: European Symp. On Programming, pp. 380\u2013398 (2003)","DOI":"10.1007\/3-540-36575-3_26"},{"key":"2_CR23","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement for 3-valued-logic analysis. Tech. Rep. 1504, Comp. Sci. Dept., Univ. of Wisconsin (2004)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. Princ. of Prog. Lang., 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N. Rinetzky","year":"2001","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol.\u00a02027, pp. 133\u2013149. Springer, Heidelberg (2001)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. Tech. Rep. 1505, Comp. Sci. Dept., Univ. of Wisconsin (2004)","DOI":"10.1007\/978-3-540-27864-1_19"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. Princ. of Prog. Lang., 27\u201340 (2001)","DOI":"10.1145\/373243.360206"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Emerson, E., Sistla, A.: Symmetry and model checking. In: Courcoubetis, C. (ed.) Int. Conf. on Computer Aided Verif., pp. 463\u2013478 (1993)","DOI":"10.1007\/3-540-56922-7_38"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. Princ. of Prog. Lang (1978)","DOI":"10.1145\/512760.512770"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Dill, D.: Timing assumptions and verification of finite-state concurrent systems. Automatic Verification Methods for Finite State Systems, 197\u2013212 (1989)","DOI":"10.1007\/3-540-52148-8_17"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: A few graph-based relational numerical abstract domains. In: Static Analysis Symp., pp. 117\u2013132 (2002)","DOI":"10.1007\/3-540-45789-5_11"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Simon, A., King, A., Howe, J.: Two variables per linear inequality as an abstract domain. In: Int. Workshop on Logic Based Prog. Dev. and Transformation , pp.71\u201389 (2002)","DOI":"10.1007\/3-540-45013-0_7"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. Verif., Model Checking, and Abs. Interp., 252\u2013266 (2004)","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. Tools and Algs. for the Construct. and Anal. of Syst., 530\u2013545 (2004)","DOI":"10.1007\/978-3-540-24730-2_39"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Int. Symp. on Softw. Testing and Analysis, pp. 26\u201338 (2000)","DOI":"10.1145\/347324.348031"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. Prog. Lang. Design and Impl., 83\u201394 (2002)","DOI":"10.1145\/543552.512540"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. In: Workshop on Software Model Checking (2003)","DOI":"10.1016\/S1571-0661(05)80006-4"},{"key":"2_CR39","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Int. Conf. on Computer Aided Verif.,","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Int. Conf. on Computer Aided Verif.,, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. Princ. of Prog. Lang., 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.: Boolean and Cartesian abstraction for model checking C programs. Tools and Algs. for the Construct. and Anal. of Syst., 268\u2013283 (2001)","DOI":"10.1007\/3-540-45319-9_19"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Int. Conf. on Computer Aided Verif., pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"2_CR43","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. Trans. on Prog. Lang. and Syst.\u00a016, 1512\u20131542 (1994)","journal-title":"Trans. on Prog. Lang. and Syst."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27813-9_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:22:00Z","timestamp":1605759720000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27813-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223429","9783540278139"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27813-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}