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 (Q5944310)

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öller, 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çois; 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érard; 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öter, 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ño, Víctor; Dowek, Gilles; Muñoz, César}, 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]