{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T06:13:32Z","timestamp":1740118412696,"version":"3.37.3"},"reference-count":43,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2014,11,1]],"date-time":"2014-11-01T00:00:00Z","timestamp":1414800000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/100012950","name":"INRIA","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012950","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1016\/j.scico.2013.09.014","type":"journal-article","created":{"date-parts":[[2013,10,10]],"date-time":"2013-10-10T15:10:34Z","timestamp":1381417834000},"page":"154-182","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":16,"special_numbering":"PB","title":["Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions"],"prefix":"10.1016","volume":"93","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-3179","authenticated-orcid":false,"given":"A.","family":"Min\u00e9","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2013.09.014_br0010","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.entcs.2012.09.009","article-title":"Inferring sufficient conditions with backward polyhedral under-approximations","volume":"287","author":"Min\u00e9","year":"2012","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"11","key":"10.1016\/j.scico.2013.09.014_br0020","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1109\/MC.2003.1244535","article-title":"Uncovering hidden contracts: The .NET example","volume":"36","author":"Arnout","year":"2003","journal-title":"Computer"},{"key":"10.1016\/j.scico.2013.09.014_br0030","series-title":"NASA Formal Methods","first-page":"54","article-title":"Inferring definite counterexamples through under-approximation","volume":"vol. 7226","author":"Brauer","year":"2012"},{"key":"10.1016\/j.scico.2013.09.014_br0040","series-title":"Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'08)","first-page":"177","article-title":"A practical and precise inference and specializer for array bound checks elimination","author":"Popeea","year":"2008"},{"year":"2002","series-title":"Temporal property-driven verification by abstract interpretation","author":"Mass\u00e9","key":"10.1016\/j.scico.2013.09.014_br0050"},{"issue":"8","key":"10.1016\/j.scico.2013.09.014_br0060","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, non-determinacy and formal derivation of programs","volume":"18","author":"Dijkstra","year":"1975","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2013.09.014_br0070","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/S0020-0190(97)00023-9","article-title":"Non-deterministic expressions and predicate transformers","volume":"61","author":"Morris","year":"1997","journal-title":"Inf. Process. Lett."},{"issue":"5","key":"10.1016\/j.scico.2013.09.014_br0080","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-011-0211-0","article-title":"Deductive software verification","volume":"13","author":"Filli\u00e2tre","year":"2011","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.scico.2013.09.014_br0090","series-title":"25 Years of Model Checking","first-page":"27","article-title":"The beginning of model checking: A personal perspective","author":"Emerson","year":"2008"},{"issue":"1","key":"10.1016\/j.scico.2013.09.014_br0100","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","article-title":"Bounded model checking of software using SMT solvers instead of SAT solvers","volume":"11","author":"Armando","year":"2009","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"5","key":"10.1016\/j.scico.2013.09.014_br0110","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","article-title":"Counterexample-guided abstraction refinement for symbolic model checking","volume":"50","author":"Clarke","year":"2003","journal-title":"J. ACM"},{"year":"1978","series-title":"M\u00e9thodes it\u00e9ratives de construction et d'approximation de points fixes d'op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes","author":"Cousot","key":"10.1016\/j.scico.2013.09.014_br0120"},{"key":"10.1016\/j.scico.2013.09.014_br0130","series-title":"AIAA Infotech@Aerospace, No. 2010-3385","first-page":"1","article-title":"Static analysis and verification of aerospace software by abstract interpretation","author":"Bertrane","year":"2010"},{"key":"10.1016\/j.scico.2013.09.014_br0140","series-title":"Proc. of the Second Int. Symp. on Programming","first-page":"106","article-title":"Static determination of dynamic properties of programs","author":"Cousot","year":"1976"},{"key":"10.1016\/j.scico.2013.09.014_br0150","series-title":"Proc. of the 5th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL'78)","first-page":"84","article-title":"Automatic discovery of linear restraints among variables of a program","author":"Cousot","year":"1978"},{"issue":"1","key":"10.1016\/j.scico.2013.09.014_br0160","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","article-title":"The octagon abstract domain","volume":"19","author":"Min\u00e9","year":"2006","journal-title":"High.-Order Symb. Comput."},{"key":"10.1016\/j.scico.2013.09.014_br0170","series-title":"Proc. of the ACM Conf. on Programing Language Design and Implementation (PLDI'93)","first-page":"46","article-title":"Abstract debugging of higher-order imperative languages","author":"Bourdoncle","year":"1993"},{"key":"10.1016\/j.scico.2013.09.014_br0180","series-title":"Proc. of the 11th Int. Symp. on Static Analysis (SAS'04)","first-page":"22","article-title":"Closed and logical relations for over- and under-approximation of powersets","volume":"vol. 3148","author":"Schmidt","year":"2004"},{"key":"10.1016\/j.scico.2013.09.014_br0190","series-title":"Proc. of the 9th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'08)","first-page":"188","article-title":"Sufficient preconditions for modular assertion checking","volume":"vol. 4905","author":"Moy","year":"2008"},{"issue":"7","key":"10.1016\/j.scico.2013.09.014_br0200","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"King","year":"1976","journal-title":"Commun. ACM"},{"year":"2007","series-title":"Backward analysis for inferring quantified pre-conditions","author":"Lev-Ami","key":"10.1016\/j.scico.2013.09.014_br0210"},{"key":"10.1016\/j.scico.2013.09.014_br0220","series-title":"Proc. of 13th Int. Symp. on Static Analysis (SAS'06)","first-page":"127","article-title":"Underapproximating predicate transformers","volume":"vol. 4134","author":"Schmidt","year":"2006"},{"key":"10.1016\/j.scico.2013.09.014_br0230","series-title":"Proc. of the 14th Int. Symp. on Static Analysis (SAS'07)","first-page":"137","article-title":"Under-approximations of computations in real numbers based on generalized affine arithmetic","volume":"vol. 4634","author":"Goubault","year":"2007"},{"key":"10.1016\/j.scico.2013.09.014_br0240","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pac. J. Math."},{"issue":"1","key":"10.1016\/j.scico.2013.09.014_br0250","doi-asserted-by":"crossref","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","article-title":"Constructive versions of Tarski's fixed point theorems","volume":"81","author":"Cousot","year":"1979","journal-title":"Pac. J. Math."},{"key":"10.1016\/j.scico.2013.09.014_br0260","series-title":"Proc. of the 12th Int. Symp. on Static Analysis (SAS'05)","first-page":"303","article-title":"Understanding the origin of alarms in Astr\u00e9","volume":"vol. 3672","author":"Rival","year":"2005"},{"key":"10.1016\/j.scico.2013.09.014_br0270","series-title":"Proc. of the 12th Int. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI'11)","first-page":"150","article-title":"Precondition inference from intermittent assertions and application to contracts on collections","volume":"vol. 6538","author":"Cousot","year":"2011"},{"key":"10.1016\/j.scico.2013.09.014_br0280","series-title":"Conf. Rec. of the 39th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages","first-page":"245","article-title":"An abstract interpretation framework for termination","author":"Cousot","year":"2012"},{"author":"Lalire","key":"10.1016\/j.scico.2013.09.014_br0290"},{"key":"10.1016\/j.scico.2013.09.014_br0300","series-title":"Proc. of the 4th ACM Symp. on Principles of Programming Languages (POPL'77)","first-page":"238","article-title":"Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/j.scico.2013.09.014_br0310","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/j.entcs.2009.07.082","article-title":"Abstract interpretation from a denotational semantics perspective","volume":"249","author":"Schmidt","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.09.014_br0320","series-title":"Proc. of the Int. Conf. on Formal Methods in Programming and Their Applications (FMPA'93)","first-page":"128","article-title":"Efficient chaotic iteration strategies with widenings","volume":"vol. 735","author":"Bourdoncle","year":"1993"},{"year":"2010","series-title":"Robust and generic abstract domain for static program analysis: the polyhedral case","author":"Nguyen Que","key":"10.1016\/j.scico.2013.09.014_br0330"},{"key":"10.1016\/j.scico.2013.09.014_br0340","series-title":"IEEE RTSS'97","first-page":"14","article-title":"Efficient verification of real-time systems: Compact data structure and state-space reduction","author":"Larsen","year":"1997"},{"key":"10.1016\/j.scico.2013.09.014_br0350","series-title":"Proc. of the Int. Workshop on Programming Language Implementation and Logic Programming (PLILP'92)","first-page":"269","article-title":"Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation, invited paper","volume":"vol. 631","author":"Cousot","year":"1992"},{"issue":"1\u20132","key":"10.1016\/j.scico.2013.09.014_br0360","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","article-title":"Precise widening operators for convex polyhedra","volume":"58","author":"Bagnara","year":"2005","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"10.1016\/j.scico.2013.09.014_br0370","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s10703-009-0073-1","article-title":"Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness","volume":"35","author":"Bagnara","year":"2009","journal-title":"Form. Methods Syst. Des."},{"key":"10.1016\/j.scico.2013.09.014_br0380","series-title":"Proc. of the 7th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'06)","first-page":"348","article-title":"Symbolic methods to enhance the precision of numerical abstract domains","volume":"vol. 3855","author":"Min\u00e9","year":"2006"},{"key":"10.1016\/j.scico.2013.09.014_br0390","series-title":"Proc. of the 21st Int. Conf. on Computer Aided Verification (CAV'09)","first-page":"661","article-title":"Apron: A library of numerical abstract domains for static analysis","volume":"vol. 5643","author":"Jeannet","year":"2009"},{"key":"10.1016\/j.scico.2013.09.014_br0400","series-title":"Conf. Rec. of the Sixth Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL'79)","first-page":"269","article-title":"Systematic design of program analysis frameworks","author":"Cousot","year":"1979"},{"key":"10.1016\/j.scico.2013.09.014_br0410","series-title":"Proc. of the 20th Int. Symp. on Static Analysis (SAS'13)","first-page":"43","article-title":"The abstract domain of segmented ranking functions","volume":"vol. 7935","author":"Urban","year":"2013"},{"author":"Min\u00e9","key":"10.1016\/j.scico.2013.09.014_br0420"},{"key":"10.1016\/j.scico.2013.09.014_br0430","series-title":"Proc. of the SIGPLAN Conf. on Programming Language Design and Implementation (PLDI'02)","first-page":"234","article-title":"Extended static checking for Java","author":"Flanagan","year":"2002"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016764231300244X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016764231300244X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,12]],"date-time":"2018-11-12T17:39:32Z","timestamp":1542044372000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S016764231300244X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11]]},"references-count":43,"alternative-id":["S016764231300244X"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2013.09.014","relation":{},"ISSN":["0167-6423"],"issn-type":[{"type":"print","value":"0167-6423"}],"subject":[],"published":{"date-parts":[[2014,11]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2013.09.014","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2013 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}