{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:03Z","timestamp":1776333543568,"version":"3.51.2"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,7,7]],"date-time":"2009-07-07T00:00:00Z","timestamp":1246924800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1007\/s10703-009-0078-9","type":"journal-article","created":{"date-parts":[[2009,7,6]],"date-time":"2009-07-06T10:28:30Z","timestamp":1246876110000},"page":"73-97","source":"Crossref","is-referenced-by-count":111,"title":["Reducing concurrent analysis under a context bound to\u00a0sequential analysis"],"prefix":"10.1007","volume":"35","author":[{"given":"Akash","family":"Lal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,7,7]]},"reference":[{"key":"78_CR1","doi-asserted-by":"crossref","unstructured":"Ball T, Majumdar R, Millstein T, Rajamani SK (2001) Automatic predicate abstraction of C programs. In: PLDI","DOI":"10.1145\/378795.378846"},{"key":"78_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani S (2000) Bebop: a symbolic model checker for Boolean programs. In: SPIN","DOI":"10.1007\/10722468_7"},{"key":"78_CR3","unstructured":"Berger F, Schwoon S, Suwimonteerabuth D (2005) jMoped. http:\/\/www7.in.tum.de\/tools\/jmoped\/"},{"key":"78_CR4","unstructured":"Bouajjani A, Fratani S, Qadeer S (2007) Context-bounded analysis of multithreaded programs with dynamic linked structures. In: CAV"},{"key":"78_CR5","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke EM, Kidd N, Reps TW, Touili T (2006) Verifying concurrent message-passing C programs with recursive calls. In: TACAS","DOI":"10.1007\/11691372_22"},{"key":"78_CR6","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL","DOI":"10.1145\/512760.512770"},{"key":"78_CR7","doi-asserted-by":"crossref","unstructured":"Henzinger T, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: POPL","DOI":"10.1145\/503272.503279"},{"key":"78_CR8","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R (2004) Race checking by context inference. In: PLDI","DOI":"10.1145\/996841.996844"},{"key":"78_CR9","unstructured":"Kiefer S, Schwoon S, Suwimonteerabuth D. Moped. http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/"},{"key":"78_CR10","doi-asserted-by":"crossref","unstructured":"Knoop J, Steffen B (1992) The interprocedural coincidence theorem. In: CC","DOI":"10.1007\/3-540-55984-1_13"},{"key":"78_CR11","doi-asserted-by":"crossref","unstructured":"Lal A, Kidd N, Reps T, Touili T (2007) Abstract error projection. In: SAS","DOI":"10.1007\/978-3-540-74061-2_13"},{"key":"78_CR12","unstructured":"Lal A, Touili T, Kidd N, Reps T (2007) Interprocedural analysis of concurrent programs under a context bound. TR-1598, University of Wisconsin, July 2007"},{"key":"78_CR13","unstructured":"Lal A, Touili T, Kidd N, Reps T (2008) Interprocedural analysis of concurrent programs under a context bound. In: TACAS"},{"key":"78_CR14","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm M, Seidl H (2004) Precise interprocedural analysis through linear algebra. In: POPL","DOI":"10.1145\/964001.964029"},{"key":"78_CR15","unstructured":"Murphy B, Lam M (2000) Program analysis with partial transfer functions. In: PEPM"},{"key":"78_CR16","doi-asserted-by":"crossref","unstructured":"Musuvathi M, Qadeer S (2007) Iterative context bounding for systematic testing of multithreaded programs. In: PLDI","DOI":"10.1145\/1250734.1250785"},{"key":"78_CR17","unstructured":"Pel\u00e1nek R (2007) BEEM: Benchmarks for explicit model checkers. In: SPIN"},{"key":"78_CR18","unstructured":"Qadeer S, Rajamani S (2005) Deciding assertions in programs with references. Technical Report MSR-TR-2005-08, Microsoft Research, Redmond, January 2005"},{"key":"78_CR19","doi-asserted-by":"crossref","unstructured":"Qadeer S, Rajamani SK, Rehof J (2004) Summarizing procedures in concurrent programs. In: POPL","DOI":"10.1145\/964001.964022"},{"key":"78_CR20","doi-asserted-by":"crossref","unstructured":"Qadeer S, Rehof J (2005) Context-bounded model checking of concurrent software. In: TACAS","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"78_CR21","doi-asserted-by":"crossref","unstructured":"Qadeer S, Wu D (2004) KISS: keep it simple and sequential. In: PLDI","DOI":"10.1145\/996841.996845"},{"key":"78_CR22","doi-asserted-by":"crossref","unstructured":"Ramalingam G (2000) Context-sensitive synchronization-sensitive analysis is undecidable. In: TOPLAS","DOI":"10.1145\/349214.349241"},{"key":"78_CR23","doi-asserted-by":"crossref","unstructured":"Reps T, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: POPL","DOI":"10.1145\/199448.199462"},{"key":"78_CR24","doi-asserted-by":"crossref","unstructured":"Reps T, Schwoon S, Jha S, Melski D (2005) Weighted pushdown systems and their application to interprocedural dataflow analysis. In: SCP, vol\u00a058","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"78_CR25","unstructured":"Schwoon S (2002) Model-checking pushdown systems. PhD thesis, Technical University of Munich, Munich, Germany, July 2002"},{"key":"78_CR26","volume-title":"Program flow analysis: theory and applications","author":"M Sharir","year":"1981","unstructured":"Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Program flow analysis: theory and applications. Prentice-Hall, New York"},{"key":"78_CR27","unstructured":"Suwimonteerabuth D, Esparza J, Schwoon S (2008) Symbolic context-bounded analysis of multithreaded Java programs. In: SPIN"},{"key":"78_CR28","doi-asserted-by":"crossref","unstructured":"Witkowski T, Blanc N, Kroening D, Weissenbacher G (2007) Model checking concurrent linux device drivers. In: ASE","DOI":"10.1145\/1321631.1321719"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0078-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0078-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0078-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,20]],"date-time":"2020-05-20T08:08:23Z","timestamp":1589962103000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0078-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7,7]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["78"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0078-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,7,7]]}}}