{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:21:34Z","timestamp":1769750494348,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":59,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,5,27]],"date-time":"2018-05-27T00:00:00Z","timestamp":1527379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,5,27]]},"DOI":"10.1145\/3180155.3180259","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T12:16:01Z","timestamp":1528805761000},"page":"1182-1193","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Reducer-based construction of conditional verifiers"],"prefix":"10.1145","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[{"name":"LMU Munich, Germany"}]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[{"name":"LMU Munich, Germany"}]},{"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[{"name":"LMU Munich, Germany"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Paderborn University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2018,5,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/6448"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_20"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999437"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950351"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786867"},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. CAV (LNCS 9206)","author":"Beyer D.","unstructured":"D. Beyer, M. Dangl, and P. Wendler. 2015. Boosting k-Induction with Continuously-Refined Invariants. In Proc. CAV (LNCS 9206). Springer, 622--640."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393664"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770419"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.13"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_26"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180259"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032321"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998532"},{"key":"e_1_3_2_1_17_1","volume-title":"Software Verification: Testing vs. Model Checking. In Proc. HVC (LNCS 10629)","author":"Beyer D.","year":"2017","unstructured":"D. Beyer and T. Lemberger. 2017. Software Verification: Testing vs. Model Checking. In Proc. HVC (LNCS 10629). Springer, 99--114."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_12"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. FORTE (LNCS 9039)","author":"Beyer D.","unstructured":"D. Beyer, S. L\u00f6we, and P. Wendler. 2015. Sliced Path Prefixes: An Effective Method to Enable Refinement Selection. In Proc. FORTE (LNCS 9039). Springer, 228--243."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978428"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855756"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_28"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2231980"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_13"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884843"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","unstructured":"P. Cousot and R. Cousot. 1979. Systematic Design of Program Analysis Frameworks. In POPL. ACM Press 269--282. 10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1782734.1782757"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062533"},{"key":"e_1_3_2_1_35_1","volume-title":"Proc. EASE (LNCS 9033)","author":"Czech M.","unstructured":"M. Czech, M.-C. Jakobs, and H. Wehrheim. 2015. Just Test What You Cannot Verify!. In Proc. EASE (LNCS 9033). Springer, 100--114."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985971"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_30"},{"key":"e_1_3_2_1_41_1","volume-title":"Proc. CAV (LNCS 8044)","author":"Heizmann M.","unstructured":"M. Heizmann, J. Hoenicke, and A. Podelski. 2013. Software Model Checking for People Who Love Automata. In Proc. CAV (LNCS 8044). Springer, 36--52."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632372"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2695664.2695690"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1138912.1138916"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","unstructured":"R. Jhala and R. Majumdar. 2009. Software Model Checking. Comput. Surveys 41 4 Article 21 (2009) 54 pages 10.1145\/1592434.1592438","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"e_1_3_2_1_49_1","volume-title":"Proc. CSTVA@ISSTA (CEUR 1639)","author":"K\u00f6roglu Y.","unstructured":"Y. K\u00f6roglu and A. Sen. 2016. Design of a Modified Concolic Testing Algorithm with Smaller Constraints. In Proc. CSTVA@ISSTA (CEUR 1639). CEUR-WS.org, 3--14. http:\/\/ceur-ws.org\/Vol-1639\/paper-03.pdf"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656201"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.29"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635872"},{"key":"e_1_3_2_1_56_1","volume-title":"Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In Proc","author":"Stephens N.","year":"2016","unstructured":"N. Stephens, J. Grosen, C. Sails, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshi-taishvili, C. Kruegel, and G. Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In Proc. NDSS. The Internet Society, http :\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/25\/2017\/09\/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_45"},{"key":"e_1_3_2_1_58_1","volume-title":"Proc. CAV (LNCS 8044)","author":"Wonisch D.","unstructured":"D. Wonisch, A. Schremmer, and H. Wehrheim. 2013. Programs from Proofs - A PCC Alternative. In Proc. CAV (LNCS 8044). Springer, 912--927."},{"key":"e_1_3_2_1_59_1","volume-title":"Proc. ICST. IEEE, 1--10","author":"Yi Q.","unstructured":"Q. Yi, Z. Yang, S. Guo, C. Wang, J. Liu, and C. Zhao. 2015. Postconditioned Symbolic Execution. In Proc. ICST. IEEE, 1--10."}],"event":{"name":"ICSE '18: 40th International Conference on Software Engineering","location":"Gothenburg Sweden","acronym":"ICSE '18","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"]},"container-title":["Proceedings of the 40th International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3180155.3180259","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3180155.3180259","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:30Z","timestamp":1750210770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3180155.3180259"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,27]]},"references-count":59,"alternative-id":["10.1145\/3180155.3180259","10.1145\/3180155"],"URL":"https:\/\/doi.org\/10.1145\/3180155.3180259","relation":{},"subject":[],"published":{"date-parts":[[2018,5,27]]},"assertion":[{"value":"2018-05-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}