{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:43:40Z","timestamp":1768002220932,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319668444","type":"print"},{"value":"9783319668451","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_19","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T15:37:20Z","timestamp":1503761840000},"page":"295-311","source":"Crossref","is-referenced-by-count":5,"title":["Triggerless Happy"],"prefix":"10.1007","author":[{"given":"YuTing","family":"Chen","sequence":"first","affiliation":[]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-33693-0_6","volume-title":"Integrated Formal Methods","author":"M Ameri","year":"2016","unstructured":"Ameri, M., Furia, C.A.: Why just Boogie? Translating between intermediate verification. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79\u201395. Springer, Cham (2016). doi: 10.1007\/978-3-319-33693-0_6"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-09099-3_2","volume-title":"Tests and Proofs","author":"N Amin","year":"2014","unstructured":"Amin, N., Leino, K.R.M., Rompf, T.: Computing with an SMT solver. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 20\u201335. Springer, Cham (2014). doi: 10.1007\/978-3-319-09099-3_2"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_14"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-71067-7_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S B\u00f6hme","year":"2008","unstructured":"B\u00f6hme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie \u2014 an interactive prover for the boogie program-verifier. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 150\u2013166. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71067-7_15"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-22438-6_15","volume-title":"Automated Deduction \u2013 CADE-23","author":"S B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Moskal, M.: Heaps and data structures: a challenge for automated provers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 177\u2013191. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_15"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"19_CR7","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52, 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Dross, C., Conchon, S., Kanig, J., Paskevich, A.: Reasoning with triggers. In: SMT. EPiC Series, pp. 22\u201331. EasyChair (2012)","DOI":"10.29007\/3c1n"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: POPL, pp. 193\u2013205. ACM (2001)","DOI":"10.1145\/360204.360220"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Meyer, B., Velder, S.: Loop invariants: analysis, classification, and examples. ACM Comp. Sur. 46(3) (2014)","DOI":"10.1145\/2506375"},{"key":"19_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. Springer, New York (1981)"},{"key":"19_CR12","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: PAAR at IJCAR. CEUR Workshop Proceedings, vol. 1635, pp. 41\u201355. CEUR-WS.org (2016)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: SIGPLAN CPP, pp. 37\u201348. ACM (2016)","DOI":"10.1145\/2854065.2854071"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Suda, M., Voronkov, A.: A clausal normal form translation for FOOL. In: GCAI. EPiC, vol. 41, pp. 53\u201371. EasyChair (2016)","DOI":"10.29007\/ltkk"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_1"},{"issue":"6","key":"19_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: SAC, pp. 615\u2013622. ACM (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-41528-4_20","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2016","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 361\u2013381. Springer, Cham (2016). doi: 10.1007\/978-3-319-41528-4_20"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Liew, D., Cadar, C., Donaldson, A.F.: Symbooglix: a symbolic execution engine for Boogie programs. In: ICST, pp. 45\u201356. IEEE Computer Society (2016)","DOI":"10.1109\/ICST.2016.11"},{"key":"19_CR20","unstructured":"Nelson, C.G.: Techniques for program verification. Ph.D. thesis, Xerox PARC (1981). CSL-81-10"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-40787-1_15","volume-title":"Runtime Verification","author":"N Polikarpova","year":"2013","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: executing an intermediate verification language. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 251\u2013268. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40787-1_15"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-28717-6_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2012","unstructured":"R\u00fcmmer, P.: E-matching with free variables. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 359\u2013374. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28717-6_28"},{"issue":"4","key":"19_CR23","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T03:33:36Z","timestamp":1750822416000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}