{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:34Z","timestamp":1725471154622},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540367499"},{"type":"electronic","value":"9783540367505"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11804192_7","type":"book-chapter","created":{"date-parts":[[2006,9,29]],"date-time":"2006-09-29T04:20:46Z","timestamp":1159503646000},"page":"138-160","source":"Crossref","is-referenced-by-count":11,"title":["Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs"],"prefix":"10.1007","author":[{"given":"Dennis R.","family":"Dams","sequence":"first","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"(FlexeLint), http:\/\/www.gimpel.com"},{"key":"7_CR2","unstructured":"(Coverity), http:\/\/www.coverity.com"},{"key":"7_CR3","unstructured":"(Fortify), http:\/\/www.fortifysoftware.com\/products\/sca.jsp"},{"key":"7_CR4","unstructured":"Holzmann, G.: Static source code checking for user-defined properties. In: Proc. IDPT 2002, Pasadena, CA, USA (2002), http:\/\/www.cs.bell-labs.com\/what\/uno\/index.html"},{"key":"7_CR5","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.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 260. Springer, Heidelberg (2001)"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, L.S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE (2001), http:\/\/www.cis.ksu.edu\/santos\/bandera","DOI":"10.1145\/337180.337234"},{"issue":"5","key":"7_CR7","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 526. Springer, Heidelberg (2002)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/964001.964021"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Karp, R., Miller, R.: Parallel program schemata. J. CSS\u00a03(2) (1969)","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"7_CR11","unstructured":"Merrill, J.: GENERIC and GIMPLE: A new tree representation for entire functions. In: First GCC Developers Summit (2003), At: http:\/\/www.gcc.gnu.org"},{"key":"7_CR12","unstructured":"(Simplify), http:\/\/research.compaq.com\/SRC\/esc\/Simplify.html"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-49727-7_22","volume-title":"Static Analysis","author":"D. Schmidt","year":"1998","unstructured":"Schmidt, D., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol.\u00a01503, pp. 351\u2013380. Springer, Heidelberg (1998)"},{"key":"7_CR15","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. Aho","year":"1987","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, Reading (1987)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Lamport, L., Martin, A.J., Scholten, C.S., Steffens, E.F.M.: On-the-fly garbage collection: An excercise in cooperation. CACM\u00a021(11) (1978)","DOI":"10.1145\/359642.359655"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM\u00a018(8) (1975)","DOI":"10.1145\/360933.360975"},{"key":"7_CR18","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of programming languages\u00a03, 121\u2013189 (1995)","journal-title":"Journal of programming languages"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Dams, D.: Comparing abstraction refinement algorithms. In: SoftMC: Workshop on Software Model Checking (2003)","DOI":"10.1016\/S1571-0661(05)80003-9"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: POPL (2002)","DOI":"10.1145\/503272.503286"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: POPL (1997)","DOI":"10.1145\/263699.263717"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proc. of the ACM SIGPLAN (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: ICSE (2000), http:\/\/ase.arc.nasa.gov\/visser\/jpf","DOI":"10.1109\/ASE.2000.873645"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: PLDI (2002)","DOI":"10.21236\/ADA419593"},{"key":"7_CR25","unstructured":"(PolySpace), http:\/\/www.polyspace.com"},{"key":"7_CR26","unstructured":"(Klocwork), http:\/\/www.klocwork.com"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: PLDI (2002)","DOI":"10.1145\/512537.512538"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Brand, D.: A software falsifier. In: International symposium on Software Reliability Engineering, pp. 174\u2013185 (2000)","DOI":"10.1109\/ISSRE.2000.885870"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Finkel, A.: Reduction and covering of infinite reachability trees. Information and Computation\u00a089(2) (1990)","DOI":"10.1016\/0890-5401(90)90009-7"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS (1998)","DOI":"10.1109\/LICS.1998.705644"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.M., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. In: PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"7_CR32","unstructured":"Larochelle, D., Evans, D.: Statically detecting likely buffer overflow vulnerabilities. In: USENIX Security Symposium (2001)"},{"issue":"7","key":"7_CR33","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":"Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software: Practice and Experience\u00a030(7), 775\u2013802 (2000)","journal-title":"Software: Practice and Experience"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/3-540-48224-5_54","volume-title":"Automata, Languages and Programming","author":"M. Benedikt","year":"2001","unstructured":"Benedikt, M., Godefroid, P., Reps, T.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 652\u2013666. Springer, Heidelberg (2001)"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-44585-4_18","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 207. Springer, Heidelberg (2001)"},{"key":"7_CR36","unstructured":"(CVC Lite), http:\/\/chicory.stanford.edu\/CVCL\/"},{"key":"7_CR37","unstructured":"(CBMC), http:\/\/www.cs.cmu.edu\/~modelcheck\/cbmc\/"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E Analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/11513988_45","volume-title":"Computer Aided Verification","author":"C.L. Conway","year":"2005","unstructured":"Conway, C.L., Namjoshi, K.S., Dams, D., Edwards, S.A.: Incremental algorithms for inter-procedural analysis of safety properties. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 449\u2013461. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11804192_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T06:55:10Z","timestamp":1555829710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11804192_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540367499","9783540367505"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/11804192_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}