{"entities":{"Q5944310":{"pageid":8121112,"ns":120,"title":"Item:Q5944310","lastrevid":25466726,"modified":"2024-03-04T22:44:38Z","type":"item","id":"Q5944310","labels":{"en":{"language":"en","value":"Correct hardware design and verification methods. 11th IFIP WG 10. 5 advanced research working conference, CHARME 2001, Livingston, Scotland, GB, September 4--7, 2001. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1653520"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5944310$E6A151A0-40B1-477E-98BE-EC047D088EA9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"098b36b13ddc850b3e9b2d6997a30da10c661357","datavalue":{"value":{"text":"Correct hardware design and verification methods. 11th IFIP WG 10. 5 advanced research working conference, CHARME 2001, Livingston, Scotland, GB, September 4--7, 2001. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5944310$55805588-900D-4DC6-9882-33E2DD606F89","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ca5268adc0cc782cec8774e5a121507f3907a1b1","datavalue":{"value":"0971.00031","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5944310$46C51478-4057-49FA-8019-7FA34D1315B1","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5944310$6183C813-E8C9-4E79-B9C5-9A56F4B55034","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d3e9ce93542d4f996722c3cc295b2a33bb96fb2","datavalue":{"value":{"time":"+2001-10-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5944310$9F043B16-0C24-4D38-969F-A3D506218B40","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"39cf272ee1d90c8d65ca0a71a2f0df5c9824cf6f","datavalue":{"value":"The articles of mathematical interest will be reviewed individually. The preceding conference (10th, 1999) has been reviewed (see Zbl 0929.00066).  Indexed articles:  \\textit{Johnson, Steven D.}, View from the fringe of the fringe. (Extended summary), 1-12 [Zbl 1003.68618]  \\textit{Mycroft, Alan; Sharp, Richard}, Hardware synthesis using SAFL and application to processor design (invited talk), 13-39 [Zbl 1002.68646]  \\textit{Beers, Robert; Ghughal, Rajnish; Aagaard, Mark}, Applications of hierarchical verification in model checking, 40-57 [Zbl 1002.68631]  \\textit{Shtrichman, Ofer}, Pruning techniques for the SAT-based bounded model checking problem, 58-70 [Zbl 1002.68511]  \\textit{M\u00f6ller, M. Oliver; Alur, Rajeev}, Heuristics for hierarchical partitioning with application to model checking, 71-85 [Zbl 1002.68509]  \\textit{Beyer, Dirk}, Efficient reachability analysis and refinement checking of timed automata using BDDs, 86-91 [Zbl 1002.68513]  \\textit{Siewe, Fran\u00e7ois; Hung, Dang Van}, Deriving real-time programs from duration calculus specifications, 92-97 [Zbl 1002.68508]  \\textit{Yorav, Karen; Katz, Sagi; Kiper, Ron}, Reproducing synchronization bugs with model checking, 98-103 [Zbl 1002.68659]  \\textit{Turner, Kenneth J.; He, Ji}, Formally-based design evaluation, 104-109 [Zbl 1002.68644]  \\textit{Berry, G\u00e9rard; Sentovich, Ellen}, Multiclock Esterel, 110-125 [Zbl 1002.68653]  \\textit{Albrecht, Alvin R.; Hu, Alan J.}, Register transformations with multiple clock domains, 126-139 [Zbl 1002.68658]  \\textit{Winstanley, Anthony; Greenstreet, Mark}, Temporal properties of self-timed rings, 140-154 [Zbl 1002.68664]  \\textit{Ratzaby, Gil; Ur, Shmuel; Wolfsthal, Yaron}, Coverability analysis using symbolic model checking, 155-160 [Zbl 1002.68637]  \\textit{He, Ji; Turner, Kenneth J.}, Specifying hardware timing with ET-LOTOS, 161-166 [Zbl 1002.68663]  \\textit{Seceleanu, Tiberiu; Plosila, Juha}, Formal pipeline design, 167-172 [Zbl 1003.68611]  \\textit{Radhakrishnan, Rajesh; Teica, Elena; Vemuri, Ranga}, Verification of basic block schedules using RTL transformations, 173-178 [Zbl 1003.68617]  \\textit{McMillan, K. L.}, Parameterized verification of the FLASH cache coherence protocol by compositional model checking, 179-195 [Zbl 1002.68674]  \\textit{Kaivola, Roope; Kohatsu, Katherine}, Proof engineering in the large: Formal verification of Pentium\\(^\\circledR\\) 4 floating-point divider, 196-211 [Zbl 1002.68677]  \\textit{McKeever, Steve; Luk, Wayne}, Towards provably-correct hardware compilation tools based on pass separation techniques, 212-227 [Zbl 1002.68673]  \\textit{Sharp, Richard; Mycroft, Alan}, A higher-level language for hardware synthesis, 228-243 [Zbl 1002.68621]  \\textit{Kort, Iskander; Tahar, Sofiene; Curzon, Paul}, Hierarchical verification using an MDG-HOL hybrid tool, 244-258 [Zbl 1002.68647]  \\textit{Tronci, Enrico; Della Penna, Giuseppe; Intrigila, Benedetto; Venturini Zilli, Marisa}, Exploiting transition locality in automatic verification, 259-274 [Zbl 1002.68642]  \\textit{Copty, Fady; Irron, Amitai; Weissberg, Osnat; Kropp, Nathan; Kamhi, Gila}, Efficient debugging in a formal verification environment, 275-292 [Zbl 1002.68639]  \\textit{Chauhan, P.; Clarke, E.; Jha, S.; Kukula, J.; Veith, H.; Wang, D.}, Using combinatorial optimization methods for quantification scheduling, 293-309 [Zbl 1002.68512]  \\textit{Esparza, Javier; Schr\u00f6ter, Claus}, Net reductions for LTL model-checking, 310-324 [Zbl 1002.68510]  \\textit{Berg, Christoph; Jacobi, Christian}, Formal verification of the VAMP floating point unit, 325-339 [Zbl 1002.68643]  \\textit{Shimizu, Kanna; Dill, David L.; Chou, Ching-Tsun}, A specification methodology by a collection of compact properties as applied to the Intel\\(^\\circledR\\) Itanium\\(^{\\text{TM}}\\) processor bus protocol, 340-354 [Zbl 1002.68679]  \\textit{Claessen, Koen; Sheeran, Mary; Singh, Satnam}, The design and verification of a sorter core, 355-369 [Zbl 1002.68665]  \\textit{Kong, Xiaohua; Negulescu, Radu; Ying, Larry Weidong}, Refinement-based formal verification of asynchronous wrappers for independently clocked domains in systems on chip, 370-385 [Zbl 1002.68672]  \\textit{Bhadra, Jayanta; Martin, Andrew; Abraham, Jacob; Abadir, Magdy}, Using abstract specifications to verify \\(\\text{PowerPC}^{\\text{TM}}\\) custom memories by symbolic trajectory evaluation, 386-402 [Zbl 1003.68619]  \\textit{Butler, Ricky; Carre\u00f1o, V\u00edctor; Dowek, Gilles; Mu\u00f1oz, C\u00e9sar}, Formal verification of conflict detection algorithms, 403-417 [Zbl 1002.68516]  \\textit{Gascard, Eric; Pierre, Laurence}, Induction-oriented formal verification in symmetric interconnection networks, 418-432 [Zbl 1002.68648]  \\textit{Aagaard, Mark D.; Cook, Byron; Day, Nancy A.; Jones, Robert B.}, A framework for microprocessor correctness statements, 433-448 [Zbl 1002.68500]  \\textit{Zhu, Huibiao; Bowen, Jonathan P.; He, Jifeng}, From operational semantics to denotational semantics for Verilog, 449-464 [Zbl 1002.68507]  \\textit{Li, Xuandong; Pei, Yu; Zhao, Jianhua; Li, Yong; Zheng, Tao; Zheng, Guoliang}, Efficient verification of a class of linear hybrid automata using linear programming, 465-479 [Zbl 1002.68506]","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$A6D080EC-4CEF-4277-8CBE-245DC4637E91","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5944310$EB86F669-743C-457C-9EB3-2FADCA24851C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5944310$7205911E-DD46-404F-8DAF-7E02EECAD5AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5660fa98e757386c89b5eaaace43a72021a48756","datavalue":{"value":"68Mxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5944310$1765614B-4816-4F2E-B4B8-5967BF024FA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5944310$1992D21A-9AB3-42F7-9E61-88544D9F0E2A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"93e1e48bc7c50b14dd2591152e8ff68e7db51219","datavalue":{"value":"1653520","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5944310$D2577F81-B4D3-4069-AECF-491AE3BC9121","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05d39bb5aa213addb68f23627efa51bbb1c69e9a","datavalue":{"value":"Livingstone, Scotland (GB)","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$72799CCF-695B-4A49-A42C-44EE84E69D01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d83ae477e518ffecea78688f13a2aaaeca13299","datavalue":{"value":"Conference","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$E1C26999-F77B-4F64-B48C-8EC5A0CA3F14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$6E3793FF-92A6-4E14-85BC-16E53818A040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c7987c74676604a5a4e6821706a60fa4524a38fa","datavalue":{"value":"CHARME 2001","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$EEA64D3F-CD8A-422F-8FE7-AA6B3D5EFFE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3457552c8d8240e9757186e049802a19ed160b64","datavalue":{"value":"Hardware design","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$BB1BFB47-B8A9-4523-AF70-F6F91E9EFF9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b7474caa1fe4023a485c900222c2470f8696080","datavalue":{"value":"Verification methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q5944310$6F7A8E43-300E-4604-A1D2-68686AE610A9","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5944310$21ED14BC-DA1B-4952-A40E-C45AFCB3B7D3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5944310","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5944310"}}}}}