{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T04:46:17Z","timestamp":1768452377410,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T00:00:00Z","timestamp":1499644800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,7,10]]},"DOI":"10.1145\/3092703.3098239","type":"proceedings-article","created":{"date-parts":[[2017,7,11]],"date-time":"2017-07-11T20:17:18Z","timestamp":1499804238000},"page":"408-411","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Consistency checking in requirements analysis"],"prefix":"10.1145","author":[{"given":"Jaroslav","family":"Bend\u00edk","sequence":"first","affiliation":[{"name":"Masaryk University, Czech Republic"}]}],"member":"320","published-online":{"date-parts":[[2017,7,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_14"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-015-0348-9"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_4"},{"key":"e_1_3_2_1_4_1","volume-title":"FMICS (Lecture Notes in Computer Science)","author":"Barnat Jiri","unstructured":"Jiri Barnat , Jan Beran , Lubos Brim , Tomas Kratochvila , and Petr Rockai . 2012. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs . In FMICS (Lecture Notes in Computer Science) , Vol. 7437 . Springer , 78\u201392. Jiri Barnat, Jan Beran, Lubos Brim, Tomas Kratochvila, and Petr Rockai. 2012. Tool Chain to Support Automated Formal Verification of Avionics Simulink Designs. In FMICS (Lecture Notes in Computer Science), Vol. 7437. Springer, 78\u201392."},{"key":"e_1_3_2_1_5_1","volume-title":"CAV (Lecture Notes in Computer Science)","author":"Barnat Jiri","unstructured":"Jiri Barnat , Lubos Brim , Vojtech Havel , Jan Havl\u00edcek , Jan Kriho , Milan Lenco , Petr Rockai , Vladim\u00edr Still , and Jir\u00ed Weiser . 2013. DiVin E 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs . In CAV (Lecture Notes in Computer Science) , Vol. 8044 . Springer , 863\u2013868. Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havl\u00edcek, Jan Kriho, Milan Lenco, Petr Rockai, Vladim\u00edr Still, and Jir\u00ed Weiser. 2013. DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. In CAV (Lecture Notes in Computer Science), Vol. 8044. Springer, 863\u2013868."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008779610539"},{"key":"e_1_3_2_1_7_1","first-page":"123","article-title":"MUSer2: An Efficient MUS Extractor","volume":"8","author":"Belov Anton","year":"2012","unstructured":"Anton Belov and Jo\u00e3o Marques-Silva . 2012 . MUSer2: An Efficient MUS Extractor . JSAT 8 , 3\/4 (2012), 123 \u2013 128 . Anton Belov and Jo\u00e3o Marques-Silva. 2012. MUSer2: An Efficient MUS Extractor. JSAT 8, 3\/4 (2012), 123\u2013128.","journal-title":"JSAT"},{"key":"e_1_3_2_1_8_1","volume-title":"SEFM (Lecture Notes in Computer Science)","author":"Bend\u00edk Jaroslav","unstructured":"Jaroslav Bend\u00edk , Nikola Bene\u0161 , Ji\u0159\u00ed Barnat , and Ivana \u010cern\u00e1 . 2016. Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis . In SEFM (Lecture Notes in Computer Science) , Vol. 9763 . Springer , 121\u2013 136. Jaroslav Bend\u00edk, Nikola Bene\u0161, Ji\u0159\u00ed Barnat, and Ivana \u010cern\u00e1. 2016. Finding Boundary Elements in Ordered Sets with Application to Safety and Requirements Analysis. In SEFM (Lecture Notes in Computer Science), Vol. 9763. Springer, 121\u2013 136."},{"key":"e_1_3_2_1_9_1","volume-title":"FSTTCS (LIPIcs)","volume":"65","author":"Bend\u00edk Jaroslav","year":"2016","unstructured":"Jaroslav Bend\u00edk , Nikola Benes , Ivana Cern\u00e1 , and Jiri Barnat . 2016 . Tunable Online MUS\/MSS Enumeration . In FSTTCS (LIPIcs) , Vol. 65 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 50:1\u201350:13. Jaroslav Bend\u00edk, Nikola Benes, Ivana Cern\u00e1, and Jiri Barnat. 2016. Tunable Online MUS\/MSS Enumeration. In FSTTCS (LIPIcs), Vol. 65. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 50:1\u201350:13."},{"key":"e_1_3_2_1_10_1","volume-title":"Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau","author":"Bertello Matteo","year":"2016","unstructured":"Matteo Bertello , Nicola Gigante , Angelo Montanari , and Mark Reynolds . 2016 . Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau . In IJCAI. IJCAI\/AAAI Press , 950\u2013956. Matteo Bertello, Nicola Gigante, Angelo Montanari, and Mark Reynolds. 2016. Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau. In IJCAI. IJCAI\/AAAI Press, 950\u2013956."},{"key":"e_1_3_2_1_11_1","volume-title":"Izak van Langevelde, Bert Lisser, and Jaco van de Pol.","author":"Blom Stefan","year":"2001","unstructured":"Stefan Blom , Wan Fokkink , Jan Friso Groote , Izak van Langevelde, Bert Lisser, and Jaco van de Pol. 2001 . Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, and Jaco van de Pol. 2001."},{"key":"e_1_3_2_1_12_1","volume-title":"CAV (Lecture Notes in Computer Science)","unstructured":"\u00b5CRL : A Toolset for Analysing Algebraic Specifications . In CAV (Lecture Notes in Computer Science) , Vol. 2102 . Springer , 250\u2013254. \u00b5CRL: A Toolset for Analysing Algebraic Specifications. In CAV (Lecture Notes in Computer Science), Vol. 2102. Springer, 250\u2013254."},{"key":"e_1_3_2_1_13_1","unstructured":"Alessandro Cimatti Edmund M. Clarke Enrico Giunchiglia Fausto Giunchiglia Marco Pistore Marco Roveri Roberto Sebastiani and Armando Tacchella. 2002.  Alessandro Cimatti Edmund M. Clarke Enrico Giunchiglia Fausto Giunchiglia Marco Pistore Marco Roveri Roberto Sebastiani and Armando Tacchella. 2002."},{"key":"e_1_3_2_1_14_1","volume-title":"CAV (Lecture Notes in Computer Science)","author":"SMV","unstructured":"Nu SMV 2 : An OpenSource Tool for Symbolic Model Checking . In CAV (Lecture Notes in Computer Science) , Vol. 2404 . Springer , 359\u2013364. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In CAV (Lecture Notes in Computer Science), Vol. 2404. Springer, 359\u2013364."},{"key":"e_1_3_2_1_15_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2001","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 2001 . Model checking. MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2001. Model checking. MIT Press."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.68.5"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1378727.1378742"},{"key":"e_1_3_2_1_19_1","volume-title":"SAT-Based Explicit LTL Reasoning. In Haifa Verification Conference (Lecture Notes in Computer Science)","volume":"9434","author":"Li Jianwen","unstructured":"Jianwen Li , Shufang Zhu , Geguang Pu , and Moshe Y. Vardi . 2015 . SAT-Based Explicit LTL Reasoning. In Haifa Verification Conference (Lecture Notes in Computer Science) , Vol. 9434 . Springer, 209\u2013224. Jianwen Li, Shufang Zhu, Geguang Pu, and Moshe Y. Vardi. 2015. SAT-Based Explicit LTL Reasoning. In Haifa Verification Conference (Lecture Notes in Computer Science), Vol. 9434. Springer, 209\u2013224."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-015-9183-0"},{"key":"e_1_3_2_1_21_1","first-page":"27","article-title":"Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores","volume":"9","author":"Nadel Alexander","year":"2014","unstructured":"Alexander Nadel , Vadim Ryvchin , and Ofer Strichman . 2014 . Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores . JSAT 9 (2014), 27 \u2013 51 . Alexander Nadel, Vadim Ryvchin, and Ofer Strichman. 2014. Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores. JSAT 9 (2014), 27\u201351.","journal-title":"JSAT"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_23_1","volume-title":"Vardi","author":"Rozier Kristin Y.","year":"2011","unstructured":"Kristin Y. Rozier and Moshe Y . Vardi . 2011 . A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. In FM (Lecture Notes in Computer Science), Vol. 6664 . Springer , 417\u2013431. Kristin Y. Rozier and Moshe Y. Vardi. 2011. A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. In FM (Lecture Notes in Computer Science), Vol. 6664. Springer, 417\u2013431."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2010.11.004"},{"key":"e_1_3_2_1_25_1","volume-title":"ATVA (Lecture Notes in Computer Science)","author":"Schuppan Viktor","unstructured":"Viktor Schuppan and Luthfi Darmawan . 2011. Evaluating LTL Satisfiability Solvers . In ATVA (Lecture Notes in Computer Science) , Vol. 6996 . Springer , 397\u2013 413. Abstract 1 Introduction 2 Related Work 3 Research questions and Contributions 4 Methodology and Evaluation 4.1 Methodology 4.2 Evaluation 5 Research Status 6 Conclusion References Viktor Schuppan and Luthfi Darmawan. 2011. Evaluating LTL Satisfiability Solvers. In ATVA (Lecture Notes in Computer Science), Vol. 6996. Springer, 397\u2013 413. Abstract 1 Introduction 2 Related Work 3 Research questions and Contributions 4 Methodology and Evaluation 4.1 Methodology 4.2 Evaluation 5 Research Status 6 Conclusion References"}],"event":{"name":"ISSTA '17: International Symposium on Software Testing and Analysis","location":"Santa Barbara CA USA","acronym":"ISSTA '17","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092703.3098239","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3092703.3098239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:37:27Z","timestamp":1750217847000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092703.3098239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,10]]},"references-count":25,"alternative-id":["10.1145\/3092703.3098239","10.1145\/3092703"],"URL":"https:\/\/doi.org\/10.1145\/3092703.3098239","relation":{},"subject":[],"published":{"date-parts":[[2017,7,10]]},"assertion":[{"value":"2017-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}