{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:48:57Z","timestamp":1764402537039},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,7,4]],"date-time":"2012-07-04T00:00:00Z","timestamp":1341360000000},"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":[[2013,2]]},"DOI":"10.1007\/s10703-012-0163-3","type":"journal-article","created":{"date-parts":[[2012,7,3]],"date-time":"2012-07-03T16:21:47Z","timestamp":1341332507000},"page":"91-118","source":"Crossref","is-referenced-by-count":40,"title":["SMT proof checking using a logical framework"],"prefix":"10.1007","volume":"42","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[]},{"given":"Duckki","family":"Oe","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Liana","family":"Hadarean","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,7,4]]},"reference":[{"key":"163_CR1","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Proceedings of the 13th international SPIN workshop on model checking of software (SPIN\u201906)","author":"A Armando","year":"2006","unstructured":"Armando A, Montovani J, Platania L (2006) Bounded model checking of software using SMT solvers instead of SAT solvers. In: Proceedings of the 13th international SPIN workshop on model checking of software (SPIN\u201906), Lecture notes in computer science, vol\u00a03925. Springer, Berlin, pp\u00a0146\u2013162"},{"key":"163_CR2","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified programs and proofs","author":"M Armand","year":"2011","unstructured":"Armand M, Faure G, Gr\u00e9goire B, Keller C, Th\u00e9ry L, Werner B (2011) A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud JP, Shao Z (eds) Certified programs and proofs, Lecture notes in computer science, vol\u00a07086. Springer, Berlin, pp\u00a0135\u2013150"},{"key":"163_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"4th international symposium on formal methods for components and objects","author":"M Barnett","year":"2006","unstructured":"Barnett M, yuh Evan Chang B, Deline R, Jacobs B, Leino KR (2006) Boogie: a modular reusable verifier for object-oriented programs. In: 4th international symposium on formal methods for components and objects, Lecture notes in computer science, vol\u00a04111. Springer, Berlin, pp\u00a0364\u2013387"},{"key":"163_CR4","first-page":"825","volume-title":"Handbook of satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol\u00a0185. IOS Press, Amsterdam, pp\u00a0825\u2013885, chap\u00a026"},{"key":"163_CR5","volume-title":"Proceedings of the 8th international workshop on satisfiability modulo theories","author":"C Barrett","year":"2010","unstructured":"Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. In: Gupta A, Kroening D (eds) Proceedings of the 8th international workshop on satisfiability modulo theories, Edinburgh, England. Available from www.smtlib.org"},{"key":"163_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Proceedings of the 19th international conference on computer aided verification (CAV\u201907)","author":"C Barrett","year":"2007","unstructured":"Barrett C, Tinelli C (2007) CVC3. In: Damm W, Hermanns H (eds) Proceedings of the 19th international conference on computer aided verification (CAV\u201907), Berlin, Germany, Lecture notes in computer science, vol\u00a04590. Springer, Berlin, pp\u00a0298\u2013302"},{"key":"163_CR7","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/11556992_31","volume-title":"Proceedings of the 8th information security conference (ISC\u201905)","author":"L Bauer","year":"2005","unstructured":"Bauer L, Garriss S, McCune JM, Reiter MK, Rouse J, Rutenbar P (2005) Device-enabled authorization in the Grey system. In: Proceedings of the 8th information security conference (ISC\u201905), pp 431\u2013445"},{"key":"163_CR8","series-title":"Texts in theoretical computer science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive theorem proving and program development. Coq\u2019Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin"},{"key":"163_CR9","volume-title":"Workshop on Proof eXchange for Theorem Proving (PxTP)","author":"F Besson","year":"2011","unstructured":"Besson F, Fontaine P, Th\u00e9ry L (2011) A flexible proof format for SMT: a proposal. In: Fontaine P, Stump\u00a0A (eds) Workshop on Proof eXchange for Theorem Proving (PxTP)"},{"key":"163_CR10","volume-title":"Boogie 2011: first international workshop on intermediate verification languages","author":"F Bobot","year":"2011","unstructured":"Bobot F, Filli\u00e2tre JC, March\u00e9 C, Paskevich A (2011) Why3: Shepherd your herd of provers. In: Boogie 2011: first international workshop on intermediate verification languages, Wroc\u0142aw, Poland"},{"key":"163_CR11","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive theorem proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme S, Weber T (2010) Fast LCF-style proof reconstruction for Z3. In: Kaufmann M, Paulson L (eds) Interactive theorem proving, Lecture notes in computer science, vol\u00a06172. Springer, Berlin, pp\u00a0179\u2013194"},{"key":"163_CR12","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Proceedings of the 22nd international conference on automated deduction (CADE), CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton T, Caminha B, De Oliveira D, D\u00e9harbe D, Fontaine P (2009) veriT: an open, trustable and efficient SMT-solver. In: Schmidt RA (ed) Proceedings of the 22nd international conference on automated deduction (CADE), CADE-22. Springer, Berlin, pp\u00a0151\u2013156"},{"key":"163_CR13","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1145\/1806596.1806643","volume-title":"Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI)","author":"J Chen","year":"2010","unstructured":"Chen J, Chugh R, Swamy N (2010) Type-preserving compilation of end-to-end verification of security enforcement. In: Proceedings of the ACM SIGPLAN conference on programming language design and implementation (PLDI). ACM, New York, pp\u00a0412\u2013423"},{"issue":"1","key":"163_CR14","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Methods Syst Des 19(1):7\u201334","journal-title":"Form Methods Syst Des"},{"key":"163_CR15","volume-title":"Workshop on proof exchange for theorem proving","author":"D Deharbe","year":"2011","unstructured":"Deharbe D, Fontaine P, Paleo BW (2011) Quantifier inference rules for SMT proofs. In: Workshop on proof exchange for theorem proving"},{"key":"163_CR16","first-page":"234","volume-title":"Proc ACM conference on programming language design and implementation","author":"C Flanagan","year":"2002","unstructured":"Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB (2002) Extended static checking for Java. In: Proc ACM conference on programming language design and implementation, pp\u00a0234\u2013245"},{"key":"163_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and algorithms for construction and analysis of systems (TACAS)","author":"P Fontaine","year":"2006","unstructured":"Fontaine P, Marion JY, Merz S, Nieto LP, Tiu A (2006) Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Tools and algorithms for construction and analysis of systems (TACAS), Lecture notes in computer science, vol\u00a03920. Springer, Berlin, pp\u00a0167\u2013181"},{"key":"163_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-45620-1_29","volume-title":"18th international conference on automated deduction (CADE)","author":"J Ford","year":"2002","unstructured":"Ford J, Shankar N (2002) Formal verification of a combination decision procedure. In: Voronkov A (ed) 18th international conference on automated deduction (CADE), Lecture notes in computer science, vol\u00a02392. Springer, Berlin, pp\u00a0347\u2013362"},{"key":"163_CR19","volume-title":"Proceedings of international workshop on satisfiability modulo theories","author":"Y Ge","year":"2008","unstructured":"Ge Y, Barrett C (2008) Proof translation and SMT-LIB benchmark certification: a preliminary report. In: Proceedings of international workshop on satisfiability modulo theories"},{"key":"163_CR20","series-title":"Lecture notes in artificial intelligence","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/978-3-642-02959-2_16","volume-title":"Proceedings of the 22nd international conference on automated deduction (CADE)","author":"A Goel","year":"2009","unstructured":"Goel A, Krsti\u0107 S, Tinelli C (2009) Ground interpolation for combined theories. In: Schmidt R (ed) Proceedings of the 22nd international conference on automated deduction (CADE), Lecture notes in artificial intelligence, vol\u00a05663. Springer, Berlin, pp\u00a0183\u2013198"},{"key":"163_CR21","first-page":"109","volume-title":"Proceedings of the 8th international conference on formal methods in computer-aided design","author":"G Hagen","year":"2008","unstructured":"Hagen G, Tinelli C (2008) Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Cimatti A, Jones R (eds) Proceedings of the 8th international conference on formal methods in computer-aided design, Portland, Oregon. IEEE, New York, pp\u00a0109\u2013117"},{"issue":"1","key":"163_CR22","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper R, Honsell F, Plotkin G (1993) A framework for defining logics. J ACM 40(1):143\u2013184","journal-title":"J ACM"},{"key":"163_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"R Jhala","year":"2006","unstructured":"Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: Tools and algorithms for the construction and analysis of systems (TACAS), Lecture notes in computer science, vol\u00a03920. Springer, Berlin, pp 459\u2013473"},{"key":"163_CR24","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"22nd ACM symposium on operating systems principles (SOSP)","author":"G Klein","year":"2009","unstructured":"Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2009) seL4: formal verification of an OS kernel. In: Matthews J, Anderson T (eds) 22nd ACM symposium on operating systems principles (SOSP). ACM, New York, pp\u00a0207\u2013220"},{"key":"163_CR25","first-page":"26","volume-title":"Proceedings of the ACM SIGCOMM 2011 conference on applications, technologies, architectures, and protocols for computer communications","author":"N Kothari","year":"2011","unstructured":"Kothari N, Mahajan R, Millstein TD, Govindan R, Musuvathi M (2011) Finding protocol manipulation attacks. In: Keshav S, Liebeherr J, Byers JW, Mogul JC (eds) Proceedings of the ACM SIGCOMM 2011 conference on applications, technologies, architectures, and protocols for computer communications, pp\u00a026\u201337"},{"key":"163_CR26","first-page":"173","volume-title":"Proceedings of 34th ACM symposium on principles of programming languages","author":"D Lee","year":"2007","unstructured":"Lee D, Crary K, Harper R (2007) Towards a mechanized metatheory of standard ML. In: Proceedings of 34th ACM symposium on principles of programming languages. ACM, New York, pp 173\u2013184"},{"key":"163_CR27","first-page":"42","volume-title":"33rd ACM symposium on principles of programming languages","author":"X Leroy","year":"2006","unstructured":"Leroy X (2006) Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Morrisett G, Jones SP (eds) 33rd ACM symposium on principles of programming languages. ACM, New York, pp\u00a042\u201354"},{"key":"163_CR28","volume-title":"Emerging trends of the 21st international conference on theorem proving in higher order logics (TPHOLs)","author":"S Lescuyer","year":"2008","unstructured":"Lescuyer S, Conchon S (2008) A reflexive formalization of a SAT solver in Coq. In: Emerging trends of the 21st international conference on theorem proving in higher order logics (TPHOLs)"},{"key":"163_CR29","doi-asserted-by":"crossref","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107 F (2010) Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor Comput Sci 411:4333\u20134356","journal-title":"Theor Comput Sci"},{"key":"163_CR30","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Proceedings of computer aided verification","author":"K McMillan","year":"2003","unstructured":"McMillan K (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr, Somenzi F (eds) Proceedings of computer aided verification, Lecture notes in computer science, vol\u00a02725. Springer, Berlin, pp\u00a01\u201313"},{"key":"163_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1007\/978-3-540-78800-3_38","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"M Moskal","year":"2008","unstructured":"Moskal M (2008) Rocket-fast proof checking for SMT solvers. In: Ramakrishnan C, Rehof J (eds) Tools and algorithms for the construction and analysis of systems (TACAS), Lecture notes in computer science, vol\u00a04963. Springer, Berlin, pp\u00a0486\u2013500"},{"key":"163_CR32","volume-title":"7th international workshop on the implementation of logics (IWIL)","author":"L Moura de","year":"2008","unstructured":"de Moura L, Bj\u00f8rner N (2008) Proofs and refutations, and Z3. In: Konev B, Schmidt R, Schulz S (eds) 7th international workshop on the implementation of logics (IWIL)"},{"key":"163_CR33","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"24th ACM SIGPLAN-SIGACT symposium on principles of programming languages","author":"G Necula","year":"1997","unstructured":"Necula G (1997) Proof-carrying code. In: 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp\u00a0106\u2013119"},{"key":"163_CR34","first-page":"93","volume-title":"13th annual IEEE symposium on logic in computer science","author":"G Necula","year":"1998","unstructured":"Necula G, Lee P (1998) Efficient representation and validation of proofs. In: 13th annual IEEE symposium on logic in computer science, pp 93\u2013104"},{"key":"163_CR35","first-page":"142","volume-title":"Proceedings of the 28th ACM symposium on principles of programming languages","author":"G Necula","year":"2001","unstructured":"Necula G, Rahul S (2001) Oracle-based checking of untrusted software. In: Proceedings of the 28th ACM symposium on principles of programming languages, pp 142\u2013154"},{"issue":"6","key":"163_CR36","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"163_CR37","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL\u2014a proof assistant for higher-order logic, Lecture notes in computer science, vol\u00a02283. Springer, Berlin"},{"key":"163_CR38","volume-title":"Proceedings of international workshop on satisfiability modulo theories","author":"D Oe","year":"2009","unstructured":"Oe D, Reynolds A, Stump A (2009) Fast and flexible proof checking for SMT. In: Dutertre B, Strichman O (eds) Proceedings of international workshop on satisfiability modulo theories"},{"key":"163_CR39","volume-title":"Proceedings of international workshop on satisfiability modulo theories","author":"A Reynolds","year":"2010","unstructured":"Reynolds A, Hadarean L, Tinelli C, Ge Y, Stump A, Barrett C (2010) Comparing proof systems for linear real arithmetic with LFSC. In: Gupta A, Kroening D (eds) Proceedings of international workshop on satisfiability modulo theories"},{"key":"163_CR40","volume-title":"Proceedings of the 9th international workshop on satisfiability modulo theories","author":"A Reynolds","year":"2011","unstructured":"Reynolds A, Tinelli C, Hadarean L (2011) Certified interpolant generation for EUF. In: Lahiri S, Seshia S (eds) Proceedings of the 9th international workshop on satisfiability modulo theories"},{"key":"163_CR41","volume-title":"Handbook of automated reasoning","author":"J Robinson","year":"2001","unstructured":"Robinson J, Voronkov AE (2001) Handbook of automated reasoning. Elsevier, Amsterdam"},{"issue":"3\u20134","key":"163_CR42","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani R (2007) Lazy satisability modulo theories. J Satisfiability Boolean Model Comput 3(3\u20134): 141\u2013224","journal-title":"J Satisfiability Boolean Model Comput"},{"key":"163_CR43","volume-title":"Proceedings of the international workshop on logical frameworks and metalanguages: theory and practice (LFMTP)","author":"A Stump","year":"2008","unstructured":"Stump A (2008) Proof checking technology for satisfiability modulo theories. In: Abel A, Urban C (eds) Proceedings of the international workshop on logical frameworks and metalanguages: theory and practice (LFMTP)"},{"key":"163_CR44","doi-asserted-by":"crossref","first-page":"392","DOI":"10.1007\/3-540-45620-1_32","volume-title":"18th international conference on automated deduction (CADE)","author":"A Stump","year":"2002","unstructured":"Stump A, Dill D (2002) Faster proof checking in the Edinburgh logical framework. In: 18th international conference on automated deduction (CADE), pp 392\u2013407"},{"key":"163_CR45","volume-title":"Proceedings of international workshop on satisfiability modulo theories","author":"A Stump","year":"2008","unstructured":"Stump A, Oe D (2008) Towards an SMT proof format. In: Barrett C, de Moura L (eds) Proceedings of international workshop on satisfiability modulo theories"},{"key":"163_CR46","unstructured":"Van Gelder A (2012) http:\/\/users.soe.ucsc.edu\/~avg\/ProofChecker\/ProofChecker-fileformat.txt (accessed Jan 10, 2005)"},{"key":"163_CR47","doi-asserted-by":"crossref","unstructured":"Watkins K, Cervesato I, Pfenning F, Walker D (2002) A concurrent logical framework I: judgments and properties. Tech. Rep. CMU-CS-02-101. Carnegie Mellon University","DOI":"10.21236\/ADA418517"},{"issue":"1","key":"163_CR48","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T Weber","year":"2009","unstructured":"Weber T, Amjad H (2009) Efficiently checking propositional refutations in HOL theorem provers. J Appl Log 7(1):26\u201340","journal-title":"J Appl Log"},{"key":"163_CR49","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1145\/1542476.1542514","volume-title":"Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation (PLDI)","author":"K Zee","year":"2009","unstructured":"Zee K, Kuncak V, Rinard MC (2009) An integrated proof language for imperative programs. In: Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation (PLDI), pp\u00a0338\u2013351"},{"key":"163_CR50","volume-title":"Workshop on logical frameworks and meta-languages: theory and practice (LFMTP)","author":"M Zeller","year":"2007","unstructured":"Zeller M, Stump A, Deters M (2007) Signature compilation for the Edinburgh logical framework. In: Sch\u00fcrmann C (ed) Workshop on logical frameworks and meta-languages: theory and practice (LFMTP)"},{"key":"163_CR51","volume-title":"Proceedings of 8th international conference on computer aided deduction (CADE)","author":"L Zhang","year":"2002","unstructured":"Zhang L, Malik S (2002) The quest for efficient Boolean satisfiability solvers. In: Proceedings of 8th international conference on computer aided deduction (CADE)"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0163-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0163-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0163-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,20]],"date-time":"2022-01-20T03:35:12Z","timestamp":1642649712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0163-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,4]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["163"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0163-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,4]]}}}