{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T17:41:40Z","timestamp":1720806100439},"reference-count":50,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T00:00:00Z","timestamp":1617235200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Languages"],"published-print":{"date-parts":[[2021,4]]},"DOI":"10.1016\/j.cola.2021.101032","type":"journal-article","created":{"date-parts":[[2021,4,1]],"date-time":"2021-04-01T23:35:28Z","timestamp":1617320128000},"page":"101032","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"special_numbering":"C","title":["A binary decision diagram lifted domain for analyzing program families"],"prefix":"10.1016","volume":"63","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.cola.2021.101032_b1","series-title":"Software Product Lines: Practices and Patterns","author":"Clements","year":"2001"},{"key":"10.1016\/j.cola.2021.101032_b2","series-title":"Virtual Separation of Concerns: Toward Preprocessors 2.0","author":"K\u00e4stner","year":"2010"},{"key":"10.1016\/j.cola.2021.101032_b3","series-title":"Conference Record of the Fourth ACM Symp. on Principles of Programming Languages (POPL\u201977)","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.cola.2021.101032_b4","series-title":"Principles of Program Analysis","author":"Nielson","year":"1999"},{"key":"10.1016\/j.cola.2021.101032_b5","series-title":"Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, Proceedings","first-page":"21","article-title":"The astre\u00e9 analyzer","volume":"3444","author":"Cousot","year":"2005"},{"issue":"3\u20134","key":"10.1016\/j.cola.2021.101032_b6","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1561\/2500000034","article-title":"Tutorial on static inference of numeric invariants by abstract interpretation","volume":"4","author":"Min\u00e9","year":"2017","journal-title":"Found. Trends Program. Lang."},{"key":"10.1016\/j.cola.2021.101032_b7","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-642-36964-3_3","article-title":"Intraprocedural dataflow analysis for software product lines","volume":"10","author":"Brabrand","year":"2013","journal-title":"T. Aspect-Orient. Softw. Dev."},{"key":"10.1016\/j.cola.2021.101032_b8","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/j.scico.2015.04.005","article-title":"Systematic derivation of correct variability-aware program analyses","volume":"105","author":"Midtgaard","year":"2015","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.cola.2021.101032_b9","doi-asserted-by":"crossref","unstructured":"P. Cousot, R. Cousot, Systematic design of program analysis frameworks, in: POPL\u201979, 1979, pp. 269\u2013282.","DOI":"10.1145\/567752.567778"},{"key":"10.1016\/j.cola.2021.101032_b10","series-title":"Seventh IEEE Inter. Conf. on Software Engineering and Formal Methods, SEFM\u201909","first-page":"83","article-title":"Relational interprocedural verification of concurrent programs","author":"Jeannet","year":"2009"},{"key":"10.1016\/j.cola.2021.101032_b11","series-title":"Computer Aided Verification, 21st Inter. Conf., CAV\u201909.","first-page":"661","article-title":"Apron: A library of numerical abstract domains for static analysis","volume":"vol. 5643","author":"Jeannet","year":"2009"},{"issue":"1","key":"10.1016\/j.cola.2021.101032_b12","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":"Higher-Order Symbol. Comput."},{"key":"10.1016\/j.cola.2021.101032_b13","series-title":"Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL\u201978)","first-page":"84","article-title":"Automatic discovery of linear restraints among variables of a program","author":"Cousot","year":"1978"},{"key":"10.1016\/j.cola.2021.101032_b14","series-title":"Fundamental Approaches to Software Engineering - 23rd International Conference, FASE 2020, Proceedings","first-page":"182","article-title":"Computing program reliability using forward-backward precondition analysis and model counting","volume":"vol. 12076","author":"Dimovski","year":"2020"},{"issue":"1","key":"10.1016\/j.cola.2021.101032_b15","first-page":"13","article-title":"On calculating assertion probabilities for program families","volume":"41","author":"Dimovski","year":"2020","journal-title":"Prilozi Contribut. Sec. Nat. Math. Biotech. Sci, MASA"},{"key":"10.1016\/j.cola.2021.101032_b16","series-title":"Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019","first-page":"102","article-title":"Lifted static analysis using a binary decision diagram abstract domain","author":"Dimovski","year":"2019"},{"issue":"2","key":"10.1016\/j.cola.2021.101032_b17","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":"Pacific J. Math."},{"issue":"2\u20133","key":"10.1016\/j.cola.2021.101032_b18","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","article-title":"Abstract interpretation and application to logic programs","volume":"13","author":"Cousot","year":"1992","journal-title":"J. Log. Program."},{"issue":"8","key":"10.1016\/j.cola.2021.101032_b19","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"35","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Computers"},{"key":"10.1016\/j.cola.2021.101032_b20","series-title":"Logic in Computer Science - Modelling and Reasoning About Systems","author":"Huth","year":"2004"},{"key":"10.1016\/j.cola.2021.101032_b21","series-title":"Static Analysis - 17th International Symposium, SAS 2010. Proceedings","first-page":"287","article-title":"Boxes: A symbolic abstract domain of boxes","volume":"vol. 6337","author":"Gurfinkel","year":"2010"},{"key":"10.1016\/j.cola.2021.101032_b22","series-title":"Time for Verification, Essays in Memory of Amir Pnueli","first-page":"72","article-title":"A scalable segmented decision tree abstract domain","volume":"vol. 6200","author":"Cousot","year":"2010"},{"key":"10.1016\/j.cola.2021.101032_b23","series-title":"Static Analysis - 22nd International Symposium, SAS 2015, Proceedings","first-page":"36","article-title":"A binary decision tree abstract domain functor","volume":"vol. 9291","author":"Chen","year":"2015"},{"key":"10.1016\/j.cola.2021.101032_b24","series-title":"Static Analysis - 21st International Symposium, SAS 2014. Proceedings","first-page":"302","article-title":"A decision tree abstract domain for proving conditional termination","volume":"vol. 8723","author":"Urban","year":"2014"},{"key":"10.1016\/j.cola.2021.101032_b25","series-title":"Static Analysis - 18th International Symposium, SAS 2011. Proceedings","first-page":"233","article-title":"Logico-numerical abstract acceleration and application to the verification of data-flow programs","volume":"vol. 6887","author":"Schrammel","year":"2011"},{"key":"10.1016\/j.cola.2021.101032_b26","series-title":"Static Analysis, 12th International Symposium, SAS 2005, Proceedings","first-page":"303","article-title":"Understanding the origin of alarms in Astr\u00e9e","volume":"vol. 3672","author":"Rival","year":"2005"},{"issue":"1","key":"10.1016\/j.cola.2021.101032_b27","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1024480913162","article-title":"Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems","volume":"23","author":"Jeannet","year":"2003","journal-title":"Form. Methods Syst. Des."},{"key":"10.1016\/j.cola.2021.101032_b28","series-title":"Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. (Analyse Statique par Interpr\u00e9tation Abstraite de Propri\u00e9t\u00e9s Temporelles Fonctionnelles des Programmes)","author":"Urban","year":"2015"},{"key":"10.1016\/j.cola.2021.101032_b29","series-title":"Conference Record of the ACM Symposium on Principles of Programming Languages, (POPL\u201973)","first-page":"194","article-title":"A unified approach to global program optimization","author":"Kildall","year":"1973"},{"issue":"4","key":"10.1016\/j.cola.2021.101032_b30","first-page":"18:1","article-title":"Variability-aware static analysis at scale: An empirical study","volume":"27","author":"von Rhein","year":"2018","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10.1016\/j.cola.2021.101032_b31","doi-asserted-by":"crossref","unstructured":"E. Bodden, T. Tol\u00eado, M. Ribeiro, C. Brabrand, P. Borba, M. Mezini, SPLLIFT: statically analyzing software product lines in minutes instead of years, in: ACM SIGPLAN Conf. on PLDI \u201913, 2013, pp. 355\u2013364.","DOI":"10.1145\/2499370.2491976"},{"key":"10.1016\/j.cola.2021.101032_b32","series-title":"29th European Conf. on Object-Oriented Programming, ECOOP 2015","first-page":"247","article-title":"Variability abstractions: Trading precision for speed in family-based analyses","volume":"vol. 37","author":"Dimovski","year":"2015"},{"key":"10.1016\/j.cola.2021.101032_b33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.scico.2017.12.012","article-title":"Variability abstractions for lifted analysis","volume":"159","author":"Dimovski","year":"2018","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"10.1016\/j.cola.2021.101032_b34","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/s00165-019-00479-y","article-title":"Finding suitable variability abstractions for lifted analysis","volume":"31","author":"Dimovski","year":"2019","journal-title":"Formal Asp. Comput."},{"key":"10.1016\/j.cola.2021.101032_b35","series-title":"Proceedings of the 30th International Conference on Software Engineering (ICSE\u201908)","first-page":"311","article-title":"Granularity in software product lines","author":"K\u00e4stner","year":"2008"},{"issue":"1","key":"10.1016\/j.cola.2021.101032_b36","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1145\/2580950","article-title":"A classification and survey of analysis strategies for software product lines","volume":"47","author":"Th\u00fcm","year":"2014","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.cola.2021.101032_b37","series-title":"Analysis Strategies for Configurable Systems","author":"von Rhein","year":"2016"},{"key":"10.1016\/j.cola.2021.101032_b38","series-title":"30th IEEE\/ACM Inter. Conf. on Automated Software Engineering, ASE\u201915","first-page":"597","article-title":"Experiences from designing and validating a software modernization transformation (e)","author":"Iosif-Lazar","year":"2015"},{"key":"10.1016\/j.cola.2021.101032_b39","series-title":"Proceedings of the 31st IEEE\/ACM Intern. Conf. on Automated Software Engineering, ASE\u201916","first-page":"483","article-title":"On essential configuration complexity: measuring interactions in highly-configurable systems","author":"Meinicke","year":"2016"},{"key":"10.1016\/j.cola.2021.101032_b40","series-title":"ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201912, Beijing, China - June 11 - 16, 2012","first-page":"323","article-title":"SuperC: parsing all of C by taming the preprocessor","author":"Gazzillo","year":"2012"},{"issue":"8","key":"10.1016\/j.cola.2021.101032_b41","doi-asserted-by":"crossref","first-page":"1069","DOI":"10.1109\/TSE.2012.86","article-title":"Featured transition systems: Foundations for verifying variability-intensive systems and their application to LTL model checking","volume":"39","author":"Classen","year":"2013","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"10.1016\/j.cola.2021.101032_b42","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/s10009-016-0425-2","article-title":"Efficient family-based model checking via variability abstractions","volume":"19","author":"Dimovski","year":"2017","journal-title":"STTT"},{"key":"10.1016\/j.cola.2021.101032_b43","series-title":"Fundamental Approaches to Software Engineering - 22nd International Conference, FASE 2019, Proceedings","first-page":"192","article-title":"Variability abstraction and refinement for game-based lifted model checking of full CTL","volume":"vol. 11424","author":"Dimovski","year":"2019"},{"issue":"1","key":"10.1016\/j.cola.2021.101032_b44","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10009-019-00528-0","article-title":"CTL\u22c6 family-based model checking using variability abstractions and modal transition systems","volume":"22","author":"Dimovski","year":"2020","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.cola.2021.101032_b45","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.tcs.2017.09.029","article-title":"Verifying annotated program families using symbolic game semantics","volume":"706","author":"Dimovski","year":"2018","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.cola.2021.101032_b46","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1016\/j.tcs.2014.01.016","article-title":"Program verification using symbolic game semantics","volume":"560","author":"Dimovski","year":"2014","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.cola.2021.101032_b47","series-title":"6th International Conference on Formal Engineering Methods, ICFEM 2004, Proceedings","first-page":"146","article-title":"CSP Representation of game semantics for second-order idealized algol","volume":"vol. 3308","author":"Dimovski","year":"2004"},{"key":"10.1016\/j.cola.2021.101032_b48","series-title":"Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Proceedings","first-page":"67","article-title":"A decision tree lifted domain for analyzing program families with numerical features","volume":"vol. 12649","author":"Dimovski","year":"2021"},{"key":"10.1016\/j.cola.2021.101032_b49","series-title":"Semantics, Abstract Interpretation, and Reasoning About Programs: Essays Dedicated to David a. Schmidt on the Occasion of His Sixtieth Birthday, 2013","first-page":"161","article-title":"Modular construction of shape-numeric analyzers","volume":"vol. 129","author":"Chang","year":"2013"},{"key":"10.1016\/j.cola.2021.101032_b50","series-title":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015","first-page":"303","article-title":"Making numerical program analysis fast","author":"Singh","year":"2015"}],"container-title":["Journal of Computer Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2590118421000113?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2590118421000113?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,5,1]],"date-time":"2021-05-01T16:44:30Z","timestamp":1619887470000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2590118421000113"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4]]},"references-count":50,"alternative-id":["S2590118421000113"],"URL":"http:\/\/dx.doi.org\/10.1016\/j.cola.2021.101032","relation":{},"ISSN":["2590-1184"],"issn-type":[{"value":"2590-1184","type":"print"}],"subject":[],"published":{"date-parts":[[2021,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A binary decision diagram lifted domain for analyzing program families","name":"articletitle","label":"Article Title"},{"value":"Journal of Computer Languages","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.cola.2021.101032","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2021 Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"101032"}}