{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:09:27Z","timestamp":1767236967699,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030452339"},{"type":"electronic","value":"9783030452346"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45234-6_9","type":"book-chapter","created":{"date-parts":[[2020,4,20]],"date-time":"2020-04-20T14:04:23Z","timestamp":1587391463000},"page":"182-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"9_CR1","unstructured":"Latte integrale. UC Davis, Mathematics."},{"key":"9_CR2","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Mateus Borges, Antonio Filieri, Marcelo d\u2019Amorim, Corina S. Pasareanu, and Willem Visser. Compositional solution space quantification for probabilistic software analysis. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI\u201914, page 15. ACM, 2014.","DOI":"10.1145\/2594291.2594329"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Fran\u00e7ois Bourdoncle. Abstract debugging of higher-order imperative languages. In Proceedings of the ACM SIGPLAN\u201993 Conference on Programming Language Design and Implementation (PLDI), pages 46\u201355. ACM, 1993.","DOI":"10.1145\/173262.155095"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"N.\u00a0V. Chernikova. Algorithm for finding a general formula for the non-negative solutions of a system of linear inequalities. USSR Computational Mathematics and Mathematical Physics, 5(2):228\u2013233, 1965.","DOI":"10.1016\/0041-5553(65)90045-5"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages (POPL\u201977), pages 238\u2013252. ACM, 1977.","DOI":"10.1145\/512950.512973"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In 6th Annual ACM Symposium on Principles of Programming Languages, POPL \u201979, pages 269\u2013282, 1979.","DOI":"10.1145\/567752.567778"},{"issue":"2\u20133","key":"9_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"Patrick Cousot","year":"1992","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. J. Log. Program., 13(2\u20133):103\u2013179, 1992.","journal-title":"J. Log. Program."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Patrick Cousot, Radhia Cousot, and Francesco Logozzo. Precondition inference from intermittent assertions and application to contracts on collections. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011. Proceedings, volume 6538 of LNCS, pages 150\u2013168. Springer, 2011.","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (POPL\u201978), pages 84\u201396. ACM Press, 1978.","DOI":"10.1145\/512760.512770"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Michael Monerau. Probabilistic abstract interpretation. In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012. Proceedings, volume 7211 of LNCS, pages 169\u2013193. Springer, 2012.","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Aleksandar\u00a0S. Dimovski. Program verification using symbolic game semantics. Theor. Comput. Sci., 560:364\u2013379, 2014.","DOI":"10.1016\/j.tcs.2014.01.016"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Aleksandar S. Dimovski. Probabilistic analysis based on symbolic game semantics and model counting. In Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20\u201322 September 2017., volume 256 of EPTCS, pages 1\u201315, 2017.","DOI":"10.4204\/EPTCS.256.1"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Aleksandar S. Dimovski. Lifted static analysis using a binary decision diagram abstract domain. In Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019, pages 102\u2013114. ACM, 2019.","DOI":"10.1145\/3357765.3359518"},{"key":"9_CR15","unstructured":"Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability abstractions: Trading precision for speed in family-based analyses. In 29th European Conf. on Object-Oriented Programming, ECOOP 2015, volume 37 of LIPIcs, pages 247\u2013270. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Aleksandar\u00a0S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Finding suitable variability abstractions for lifted analysis. Formal Asp. Comput., 31(2):231\u2013259, 2019.","DOI":"10.1007\/s00165-019-00479-y"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Antonio Filieri, Corina S. Pasareanu, and Willem Visser. Reliability analysis in symbolic pathfinder. In 35th International Conference on Software Engineering, ICSE\u201913, pages 622\u2013631. IEEE \/ ACM, 2013.","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser. Probabilistic symbolic execution. In International Symposium on Software Testing and Analysis, ISSTA 2012, pages 166\u2013176. ACM, 2012.","DOI":"10.1145\/2338965.2336773"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In Proceedings of the on Future of Software Engineering, FOSE 2014, pages 167\u2013181. ACM, 2014.","DOI":"10.1145\/2593882.2593900"},{"key":"9_CR20","unstructured":"Bertrand Jeannet. Dynamic partitioning in linear relation analysis: Application to the verification of reactive systems. Formal Methods in System Design, 23(1):5\u201337, 2003."},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"Bertrand Jeannet","year":"2009","unstructured":"Bertrand Jeannet and Antoine Min\u00e9. Apron: A library of numerical abstract domains for static analysis. In Computer Aided Verification, 21st International Conference, CAV 2009. Proceedings, volume 5643 of LNCS, pages 661\u2013667. Springer, 2009."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll\u00a0C. Morgan. Linear-invariant generation for probabilistic programs: - automated support for proof-based methods. In Static Analysis - 17th International Symposium, SAS 2010. Proceedings, volume 6337 of LNCS, pages 390\u2013406. Springer, 2010.","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"9_CR23","unstructured":"Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Jan Midtgaard, Aleksandar\u00a0S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program., 105:145\u2013170, 2015.","DOI":"10.1016\/j.scico.2015.04.005"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Antoine Min\u00e9. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31\u2013100, 2006.","DOI":"10.1007\/s10990-006-8609-1"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Antoine Min\u00e9. Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program., 93:154\u2013182, 2014.","DOI":"10.1016\/j.scico.2013.09.014"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"David Monniaux. An abstract monte-carlo method for the analysis of probabilistic programs. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 93\u2013101. ACM, 2001.","DOI":"10.1145\/373243.360211"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Xavier Rival. Understanding the origin of alarms in astr\u00e9e. In Static Analysis, 12th International Symposium, SAS 2005, Proceedings, volume 3672 of LNCS, pages 303\u2013319. Springer, 2005.","DOI":"10.1007\/11547662_21"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, pages 447\u2013458. ACM, 2013.","DOI":"10.1145\/2499370.2462179"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Caterina Urban and Antoine Min\u00e9. A decision tree abstract domain for proving conditional termination. In Static Analysis - 21st International Symposium, SAS 2014. Proceedings, volume 8723 of LNCS, pages 302\u2013318. Springer, 2014.","DOI":"10.1007\/978-3-319-10936-7_19"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45234-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,11]],"date-time":"2020-08-11T12:19:48Z","timestamp":1597148388000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45234-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452339","9783030452346"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45234-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"81","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}