{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T17:40:02Z","timestamp":1742492402590,"version":"3.40.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper we propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provides the reduction technique, the specification and the system under verification. Then, using Higher Order Logic he verifies automatically if the reduction technique is soundly applied. The method is completely defined in an MDG\u2013HOL special integration platform that combines an automatic high level model checking tool Multiway Decision Graphs (MDGs) within the HOL theorem prover. We provide two case studies, the first one is the reduction using SAT\u2013MDG of an Island Tunnel Controller and the second one is the MDG\u2013HOL assume-guarantee reduction of the Look-Aside Interface. The obtained results of our approach offer a considerable gain in terms of the correctness of heuristics and reduction techniques as applied to commercial model checking, however a small penalty is paid in terms of CPU time and memory usage.<\/jats:p>","DOI":"10.1007\/s00165-012-0223-x","type":"journal-article","created":{"date-parts":[[2012,2,13]],"date-time":"2012-02-13T13:52:27Z","timestamp":1329141147000},"page":"971-991","source":"Crossref","is-referenced-by-count":0,"title":["Automatic verification of reduction techniques in Higher Order Logic"],"prefix":"10.1145","volume":"25","author":[{"given":"Sa\u2019ed","family":"Abed","sequence":"first","affiliation":[{"name":"Department of Computer Engineering, Hashemite University, Zarqa, Jordan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Otmane","family":"Ait Mohamed","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ghiath","family":"Al Sammane","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-009-9205-8"},{"key":"e_1_2_1_2_2_2","unstructured":"Abed S (2009) The verification of MDG algorithms using HOL theorem prover. http:\/\/www.ece.concordia.ca\/~s_abed\/Project.htm"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Amjad H (2003) Programming a symbolic model checker in a fully expansive theorem prover. In: Proceedings of the 16th international conference on theorem proving in higher order logics. Lecture notes in computer science vol 2758. Springer-Verlag Berlin pp 171\u2013187","DOI":"10.1007\/10930755_11"},{"key":"e_1_2_1_2_4_2","unstructured":"Abed S Ait Mohamed O Al Sammane G (2008) HOL based reduction techniques for MDGs model checking. Technical Report 2008-1-Abed ECE Department Concordia University Montreal Canada January 2008"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Abed S Ait Mohamed O Al Sammane G (2008) The performance of combining multiway decision graphs and HOL theorem prover. In: Forum on Specification and Design Languages (IEEE FDL\u201908) pp 136\u2013141","DOI":"10.1145\/1363686.1363774"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00345-0"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Abed S Ait Mohamed O Yang Z Al Sammane G (2007) Integrating SAT with multiway decision graphs for efficient model checking. In: Proceedings of IEEE ICM\u201907 Egypt. IEEE Press USA pp 129\u2013132","DOI":"10.1109\/ICM.2007.4497677"},{"key":"e_1_2_1_2_8_2","unstructured":"Bryant R Kroening D Ouaknine J Seshia SA Strichman O Brady B (2007) Deciding bit-vector arithmetic with abstraction. In: Proceedings of TACAS 2007 March 2007"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bensalem S Lakhnech Y Owre S (1998) InVeSt: a tool for the verification of invariants. In: Hu AJ Vardi MY (eds) Computer-aided verification CAV \u201998 vol 1427 Vancouver Canada. Springer-Verlag Berlin pp 505\u2013510","DOI":"10.1007\/BFb0028771"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Cai L Gajski D (2003) Transaction level modeling: an overview. In: Hardware\/Software codesign and system synthesis 2003. First IEEE\/ACM\/IFIP international conference on 1\u20133 Oct pp 19\u201324","DOI":"10.1145\/944645.944651"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61455-2_16","volume-title":"Model checking. In: Nato ASI, F, vol 152","author":"Clarke EM","year":"1996"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/39071"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Chou CT Peled D (1996) Formal verification of a partial-order reduction technique for model checking. In: In proceedings of the second international workshop on tools and algorithms for the construction and analysis of systems. Springer-Verlag Berlin pp 241\u2013257","DOI":"10.1007\/3-540-61042-1_48"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Corella F Zhou Z Song X Langevin M Cerny E (1997) Multiway decision graphs for automated hardware verification. In: Formal methods in system design vol 10 pp 7\u201346 February 1997","DOI":"10.1023\/A:1008663530211"},{"key":"e_1_2_1_2_16_2","unstructured":"Long D (1993) Model checking abstraction and compositional verification. PhD thesis Pittsburgh PA USA"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Toma D Borrione D Al Sammane G (2004) Combining several paradigms for circuit validation and verification. In: CASSIS Selected Papers LNCS vol 3362\/2005 Marseille France. Springer-Verlag GmbH Berlin pp 229\u2013249","DOI":"10.1007\/978-3-540-30569-9_12"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625970"},{"key":"e_1_2_1_2_20_2","unstructured":"Fisler K Johnson K (1995) Integrating design and verification environments through a logic supporting hardware daigrams. In: Proceedings of IFIP conference on hardware description languages and their applications (CHDL\u201995) Chiba Japan August 1995"},{"key":"e_1_2_1_2_21_2","unstructured":"Network Processing Forum. Look-aside (LA-1) interface implementation agreement revision 1.1 15 April 2004"},{"volume-title":"Introduction to HOL: a theorem proving environment for higher order logic","year":"1993","author":"Gordon MJC","key":"e_1_2_1_2_22_2"},{"volume-title":"Lecture Notes in Computer Science, vol 78","year":"1979","author":"Gordon M","key":"e_1_2_1_2_23_2"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.05.017"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxm085"},{"key":"e_1_2_1_2_26_2","unstructured":"Hussain K (2007) Abstract property verifier based on multiway decision graphs. Master thesis Concordia University Montreal Canada"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hazelhurst S Weissberg O Kamhi G Fix L (2002) A hybrid verification approach: getting deep into the design. In: DAC \u201902: proceedings of the 39th conference on design automation. ACM New York NY USA pp 111\u2013116","DOI":"10.1145\/513918.513948"},{"key":"e_1_2_1_2_28_2","unstructured":"Hou J Cerny E (2000) Model reductions in MDG-based model checking. In: 13th Annual IEEE international ASIC\/SOC conference. IEEE USA pp 347\u2013351"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"McMillan K (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr Fabio Somenzi (eds) Proceedings of the international conference on computer aided verification vol 2725. Springer-Verlag Berlin pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Kumar R Blumenr\u00f6hr C Eisenbiegler D Schmid D (1996) Formal synthesis in circuit design\u2014a classification and survey. In: FMCAD \u201996: proceedings of the first international conference on formal methods in computer-aided design London UK. Springer-Verlag Berlin pp 294\u2013309","DOI":"10.1007\/BFb0031817"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Kupferschmid S Dr\u00e4ger K Hoffmann J Finkbeiner B Dierks H Podelski A Behrmann G (2007) Uppaal\/DMC\u2014abstraction-based heuristics for directed model checking. In: Grumberg O Huth M (eds) Proceedings of the 13th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science vol 4424. Springer-Verlag Berlin Heidelberg pp 679\u2013682","DOI":"10.1007\/978-3-540-71209-1_52"},{"volume-title":"Computer-Aided Reasoning: An Approach","year":"2000","author":"Kaufmann M","key":"e_1_2_1_2_32_2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"McMillan K (1999) Verification of infinite state systems by compositional model checking. In: CHARME \u201999: proceedings of the 10th IFIP WG 10.5 advanced research working conference on correct hardware design and verification methods London UK. Springer-Verlag Berlin pp 219\u2013234","DOI":"10.1007\/3-540-48153-2_17"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881842"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.040"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Namjoshi K Kurshan R (2000) Syntactic program transformations for automatic abstraction. In: CAV \u201900: proceedings of the 12th international conference on computer aided verification London UK. Springer-Verlag Berlin pp 435\u2013449","DOI":"10.1007\/10722167_33"},{"key":"e_1_2_1_2_37_2","unstructured":"Sorensson N Een N (2005) Minisat v1.13 a SAT solver with conflict-clause minimizationn. In: Eighth international conference on theory and applications of satisfiability testing (SAT 2005) vol 3569 St. Andrews UK. Springer-Verlag Berlin"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/113906"},{"key":"e_1_2_1_2_39_2","first-page":"123","volume-title":"In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems","author":"Pnueli A","year":"1985"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Jones R Seger C-J Dill D (1996) Self-consistency checking. In: Srivas M Camilleri A (eds) First international conference on formal methods in computer-aided design vol 1166 Palo Alto CA USA Springer-Verlag Berlin pp 159\u2013171","DOI":"10.1007\/BFb0031806"},{"key":"e_1_2_1_2_41_2","unstructured":"Ray S Matthews J Tuttle M (2003) Certifying compositional model checking algorithms in ACL2. In: Hunt WA Jr Kaufmann M Moore JS (eds) 4th International workshop on the ACL2 theorem prover and its applications (ACL2 2003) Boulder CO July 2003"},{"key":"e_1_2_1_2_42_2","unstructured":"SAT07 (2007) Competition homepage. http:\/\/www.satcompetition.org\/2007\/"},{"key":"e_1_2_1_2_43_2","unstructured":"Al Sammane G (2005) Symbolic simulation of circuits described at algorithmic level. PhD thesis Joseph Fourier University"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Al Sammane G Abed S Ait Mohamed O (2007) High level reduction technique for multiway decision graphs based model checking. In: First international workshop on verification and evaluation of computer and communication systems (VECoS 2007) Algiers Algeria May 2007. The British Computer Society Australia","DOI":"10.14236\/ewic\/VECOS2007.9"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Hazelhurst S Seeger C-JH (1997) Symbolic trajectory evaluation. In: Formal hardware verification\u2014methods and systems in comparison. Springer-Verlag London UK pp 3\u201378","DOI":"10.1007\/3-540-63475-4_1"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Graf S Saidi H (1996) Verifying invariants using theorem proving. In: Alur R Henzinger TA (eds) Proceedings of the eighth international conference on computer aided verification CAV vol 1102. New Brunswick NJ USA. Springer-Verlag Berlin pp 196\u2013207","DOI":"10.1007\/3-540-61474-5_69"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Henzinger T Nicollin X Sifakis J Yovine S (1992) Symbolic model checking for real-time systems. In: 7th. Symposium of logics in computer science Santa-Cruz California. IEEE Computer Scienty Press Los Alamitos pp 394\u2013406","DOI":"10.1109\/LICS.1992.185551"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Valmari A (1991) A stubborn attack on state explosion. In: CAV \u201990: Proceedings of the 2nd international workshop on computer aided verification London UK Springer-Verlag Berlin pp 156\u2013165","DOI":"10.1007\/BFb0023729"},{"key":"e_1_2_1_2_49_2","unstructured":"Velev M (2004) Using automatic case splits and efficient CNF translation to guide a SAT-solver when formally verifying out-of-order processors. In: The 8th international symposium on artificial intelligence and mathematics Fort Lauderdale Florida USA Jan 2004"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/47.1.71"},{"key":"e_1_2_1_2_51_2","unstructured":"Zhou Z Boulerice N (1996) MDGs Tools (V1.0) User\u2019s Manual. D\u2019IRO University of Montreal June 1996"},{"issue":"3","key":"e_1_2_1_2_52_2","first-page":"223","article-title":"VOC: a methodology for the translation validation of optimizing compilers","volume":"9","author":"Zuck L","year":"2003","journal-title":"J Univers Comput Sci"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Zhou Z Song X Tahar S Cerny E Corella F Langevin M (1996) Formal verification of the island tunnel controller using multiway decision graphs. In: FMCAD \u201996: proceedings of the first international conference on formal methods in computer-aided design London UK. Springer-Verlag Berlin pp 233\u2013247","DOI":"10.1007\/BFb0031811"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0223-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0223-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0223-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T16:58:02Z","timestamp":1742489882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0223-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":53,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1007\/s00165-012-0223-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0223-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2013,11]]}}}