{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:08Z","timestamp":1750220828988,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,9]],"date-time":"2019-10-09T00:00:00Z","timestamp":1570579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","award":["200020_166288"],"award-info":[{"award-number":["200020_166288"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,10,9]]},"DOI":"10.1145\/3359986.3361214","type":"proceedings-article","created":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T12:21:06Z","timestamp":1570450866000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Lattice-based SMT for program verification"],"prefix":"10.1145","author":[{"given":"Karine","family":"Even-Mendoza","sequence":"first","affiliation":[{"name":"King's College London, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[{"name":"Universit\u00e0 della Svizzera italiana, Lugano, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[{"name":"King's College London, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[{"name":"Universit\u00e0 della Svizzera italiana, Lugano, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9149-2"},{"key":"e_1_3_2_1_2_1","volume-title":"Grigory Fedyukovich, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina.","author":"Alt Leonardo","year":"2017","unstructured":"Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even Mendoza, Grigory Fedyukovich, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2017. HiFrog: SMT-based Function Summarization for Software Verification. In TACAS (LNCS), Vol. 10206. Springer, 207--213."},{"volume-title":"VSTTE (LNCS)","author":"Alt Leonardo","key":"e_1_3_2_1_3_1","unstructured":"Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2015. A Proof-Sensitive Approach for Small Propositional Interpolants. In VSTTE (LNCS), Vol. 9593. Springer, 1--18."},{"volume-title":"Duality-based interpolation for quantifier-free equalities and uninterpreted functions","author":"Alt Leonardo","key":"e_1_3_2_1_4_1","unstructured":"Leonardo Alt, Antti E. J. Hyv\u00e4rinen, Sepideh Asadi, and Natasha Sharygina. 2017. Duality-based interpolation for quantifier-free equalities and uninterpreted functions. In FMCAD. IEEE, 39--46."},{"volume-title":"HVC (LNCS)","author":"Alt Leonardo","key":"e_1_3_2_1_5_1","unstructured":"Leonardo Alt, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2017. LRA Interpolants from No Man's Land. In HVC (LNCS), Vol. 10629. Springer, 195--210."},{"volume-title":"SPIN (LNCS)","author":"Armando Alessandro","key":"e_1_3_2_1_6_1","unstructured":"Alessandro Armando, Jacopo Mantovani, and Lorenzo Platania. 2006. Bounded model checking of software using SMT solvers instead of SAT solvers. In SPIN (LNCS), Vol. 3925. Springer, 146--162."},{"key":"e_1_3_2_1_7_1","volume-title":"Lattice Theory","author":"Birkhoff Garrett","unstructured":"Garrett Birkhoff. 1967. Lattice Theory (3rd ed.). AMS.","edition":"3"},{"key":"e_1_3_2_1_8_1","volume-title":"A case study in formal verification of a Java program. arXiv preprint arXiv:1809.03162","author":"Brizhinev Dmitry","year":"2018","unstructured":"Dmitry Brizhinev and Rajeev Gor\u00e9. 2018. A case study in formal verification of a Java program. arXiv preprint arXiv:1809.03162 (2018)."},{"key":"e_1_3_2_1_9_1","unstructured":"cbmc [n.d.]. http:\/\/www.cprover.org\/cbmc\/"},{"volume-title":"TACAS (LNCS)","author":"Cimatti Alessandro","key":"e_1_3_2_1_10_1","unstructured":"Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2017. Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. In TACAS (LNCS), Vol. 10205. Springer, 58--75."},{"volume-title":"CADE (LNCS)","author":"Cimatti Alessandro","key":"e_1_3_2_1_11_1","unstructured":"Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2017. Satisfiability Modulo Transcendental Functions via Incremental Linearization. In CADE (LNCS), Vol. 10395. Springer, 95--113."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230639"},{"key":"e_1_3_2_1_13_1","volume-title":"Bastiaan Joost Schaafsma, and Roberto Sebastiani","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. 2013. The mathsat5 SMT solver. In TACAS (LNCS), Vol. 7795. Springer, 93--107."},{"volume-title":"TACAS (LNCS)","author":"Clarke Edmund","key":"e_1_3_2_1_14_1","unstructured":"Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In TACAS (LNCS), Vol. 2988. Springer, 168--176."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_1_17_1","unstructured":"Competition on Software Verification (SV-COMP) 2018. https:\/\/svcomp.sosy-lab.org\/2018\/"},{"volume-title":"SARA (LNCS)","author":"Cousot Patrick","key":"e_1_3_2_1_18_1","unstructured":"Patrick Cousot. 2000. Partial Completeness of Abstract Fixpoint Checking. In SARA (LNCS), Vol. 1864. Springer, 1--25."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In POPL. ACM 269--282.","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2395116.2395120"},{"key":"e_1_3_2_1_22_1","volume-title":"Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. 22, 3","author":"Craig William","year":"1957","unstructured":"William Craig. 1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. 22, 3 (1957), 269--285."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.213"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.128"},{"volume-title":"TACAS (LNCS)","author":"Moura Leonardo De","key":"e_1_3_2_1_25_1","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337--340."},{"volume-title":"CADE (LNCS)","author":"Moura Leonardo De","key":"e_1_3_2_1_26_1","unstructured":"Leonardo De Moura and Grant Olney Passmore. 2013. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In CADE (LNCS), Vol. 7898. Springer, 178--192."},{"volume-title":"FM (LNCS)","author":"Denman William","key":"e_1_3_2_1_27_1","unstructured":"William Denman and C\u00e9sar Mu\u00f1oz. 2014. Automated Real Proving in PVS via MetiTarski. In FM (LNCS), Vol. 8442. Springer, 194--199."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Vijay D'Silva Leopold Haller and Daniel Kroening. 2014. Abstract Satisfaction. In POPL. ACM 139--150.","DOI":"10.1145\/2578855.2535868"},{"volume-title":"VMCAI (LNCS)","author":"D'Silva Vijay","key":"e_1_3_2_1_30_1","unstructured":"Vijay D'Silva, Mitra Purandare, Georg Weissenbacher, and Daniel Kroening. 2010. Interpolant Strength. In VMCAI (LNCS), Vol. 5944. Springer, 129--145."},{"volume-title":"VSTTE (LNCS)","author":"Even-Mendoza Karine","key":"e_1_3_2_1_31_1","unstructured":"Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyv\u00e4rinen, Hana Chockler, and Natasha Sharygina. 2018. Lattice-Based Refinement in Bounded Model Checking. In VSTTE (LNCS), Vol. 11294. Springer, 50--68."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190012"},{"key":"e_1_3_2_1_33_1","volume-title":"Clarke","author":"Gao Sicun","year":"2013","unstructured":"Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories over the Reals. In CADE (LNAI), Vol. 7898. Springer, 208--214."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0475-0"},{"volume-title":"SAS (LNCS)","author":"Giacobazzi Roberto","key":"e_1_3_2_1_35_1","unstructured":"Roberto Giacobazzi and Elisa Quintarelli. 2001. Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking. In SAS (LNCS), Vol. 2126. Springer, 356--373."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_1_37_1","unstructured":"Git Repository of Evaluation of Lattice-based Refinement Approach 2019. https:\/\/github.com\/karineek\/latticeref\/"},{"key":"e_1_3_2_1_38_1","unstructured":"Git Repository of HiFrog [n.d.]. https:\/\/scm.ti-edu.ch\/projects\/hifrog\/"},{"key":"e_1_3_2_1_39_1","unstructured":"Leopold Haller. 2013. Abstract Satisfaction. Ph.D. Dissertation. Uni. Oxford."},{"volume-title":"FMCAD (LNCS)","author":"Harrison John","key":"e_1_3_2_1_40_1","unstructured":"John Harrison. 2000. Formal Verification of Floating Point Trigonometric Functions. In FMCAD (LNCS), Vol. 1954. Springer, 217--233."},{"key":"e_1_3_2_1_41_1","unstructured":"HiFrog - Tool Usage Page 2017. http:\/\/verify.inf.usi.ch\/hifrog\/tool-usage"},{"key":"e_1_3_2_1_42_1","unstructured":"Yen-Sheng Ho Pankaj Chauhan Pritam Roy Alan Mishchenko and Robert Brayton. 2016. Efficient Uninterpreted Function Abstraction and Refinement for Word-level Model Checking. In FMCAD. ACM 65--72."},{"volume-title":"SAT (LNCS)","author":"Hyv\u00e4rinen Antti E. J.","key":"e_1_3_2_1_43_1","unstructured":"Antti E. J. Hyv\u00e4rinen, Sepideh Asadi, Karine Even-Mendoza, Grigory Fedyukovich, Hana Chockler, and Natasha Sharygina. 2017. Theory Refinement for Program Verification. In SAT (LNCS), Vol. 10491. Springer, 347--363."},{"volume-title":"SAT (LNCS)","author":"Hyv\u00e4rinen Antti E. J.","key":"e_1_3_2_1_44_1","unstructured":"Antti E. J. Hyv\u00e4rinen, Matteo Marescotti, Leonardo Alt, and Natasha Sharygina. 2016. OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. In SAT (LNCS), Vol. 9710. Springer, 547--553."},{"key":"e_1_3_2_1_45_1","volume-title":"PVAIR: Partial Variable Assignment InterpolatoR. In FASE (LNCS)","author":"Jan\u010d\u00edk Pavel","year":"2016","unstructured":"Pavel Jan\u010d\u00edk, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyv\u00e4rinen, Jan Kofro\u0148, and Natasha Sharygina. 2016. PVAIR: Partial Variable Assignment InterpolatoR. In FASE (LNCS), Vol. 9633. Springer, 419--434."},{"volume-title":"CAV (LNCS)","author":"Kahsai Temesghen","key":"e_1_3_2_1_46_1","unstructured":"Temesghen Kahsai, Philipp R\u00fcmmer, Huascar Sanchez, and Martin Sch\u00e4f. 2016. JayHorn: A framework for verifying Java programs. In CAV (LNCS), Vol. 9779. Springer, 352--358."},{"key":"e_1_3_2_1_47_1","volume-title":"Puschner","author":"Kirner Raimund","year":"2006","unstructured":"Raimund Kirner, Markus Gr\u00f6ssing, and Peter P. Puschner. 2006. Comparing WCET and Resource Demands of Trigonometric Functions Implemented as Iterative Calculations vs. Table-Lookup. In WCET (OASICS). Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0389-7"},{"key":"e_1_3_2_1_49_1","unstructured":"LB-CEGAR Page 2019. Trigonometric Functions Refinement Page Additional materials of the Paper. http:\/\/verify.inf.usi.ch\/content\/lattice-refinement\/"},{"key":"e_1_3_2_1_50_1","unstructured":"List of trigonometric identities Wikipedia the free encyclopedia [n.d.]. https:\/\/en.wikipedia.org\/wiki\/List_of_trigonometric_identities"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.09.005"},{"volume-title":"Guaranteed Proofs Using Interval Arithmetic","author":"Melquiond Guillaume","key":"e_1_3_2_1_52_1","unstructured":"Guillaume Melquiond and Cesar Munoz. 2005. Guaranteed Proofs Using Interval Arithmetic. In ARITH. IEEE, 188--195."},{"key":"e_1_3_2_1_53_1","unstructured":"Open Source Physics (OSP) Page [n.d.]. http:\/\/www.compadre.org\/osp\/"},{"volume-title":"LPAR (LNCS)","author":"Rollini Simone Fulvio","key":"e_1_3_2_1_54_1","unstructured":"Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2013. PeRIPLO: A Framework for Producing Effective Interpolants in SAT-based Software Verification. In LPAR (LNCS), Vol. 8312. Springer, 683--693."},{"key":"e_1_3_2_1_55_1","unstructured":"ROS Homepage [n.d.]. http:\/\/www.ros.org\/"},{"volume-title":"Exploring interpolants","author":"Rummer Philipp","key":"e_1_3_2_1_56_1","unstructured":"Philipp Rummer and Pavle Subotic. 2013. Exploring interpolants. In FMCAD. IEEE, 69--76."},{"key":"e_1_3_2_1_57_1","unstructured":"The Coq Proof Assistant Date Accessed May 01 2019. https:\/\/coq.inria.fr\/"},{"key":"e_1_3_2_1_58_1","unstructured":"Trigonometric tables Wikipedia the free encyclopedia [n.d.]. https:\/\/en.wikipedia.org\/wiki\/Trigonometric_tables"},{"volume-title":"Verification and testing of mobile robot navigation algorithms: A case study in SPARK","author":"Trojanek Piotr","key":"e_1_3_2_1_59_1","unstructured":"Piotr Trojanek and Kerstin Eder. 2014. Verification and testing of mobile robot navigation algorithms: A case study in SPARK. In IROS. IEEE, 1489--1494."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48487-6"}],"event":{"name":"MEMOCODE '19: 17th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"La Jolla California","acronym":"MEMOCODE '19"},"container-title":["Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359986.3361214","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3359986.3361214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:27Z","timestamp":1750202007000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3359986.3361214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,9]]},"references-count":60,"alternative-id":["10.1145\/3359986.3361214","10.1145\/3359986"],"URL":"https:\/\/doi.org\/10.1145\/3359986.3361214","relation":{},"subject":[],"published":{"date-parts":[[2019,10,9]]},"assertion":[{"value":"2019-10-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}