@inproceedings{conf/ispdc/SavvasK07,
	title = {Efficient Load Balancing on Irregular Network Topologies Using B+tree Structures.},
	author = {Ilias K. Savvas and M. Tahar Kechadi},
	booktitle = {ISPDC},
	crossref = {conf/ispdc/2007},
	pages = {185-192},
	publisher = {IEEE Computer Society},
	url = {http://dblp.uni-trier.de/db/conf/ispdc/ispdc2007.html#SavvasK07},
	year = {2007},
	biburl = {http://www.bibsonomy.org/bibtex/285cedd2d130e7f779f1cfc4c6c1ac596/dblp},
	description = {dblp},
	ee = {http://dx.doi.org/10.1109/ISPDC.2007.20}, date = {2008-11-19},
	keywords = {dblp }
}

@incollection{series/sci/HuangZK09,
	title = {Preprocessing Techniques for Online Handwriting Recognition.},
	author = {Bing Quan Huang and Y. B. Zhang and M. Tahar Kechadi},
	booktitle = {Intelligent Text Categorization and Clustering},
	crossref = {series/sci/2009-164},
	editor = {Nadia Nedjah and Luiza de Macedo Mourelle and Janusz Kacprzyk and Felipe Maia Galvão França and Alberto Ferreira de Souza},
	pages = {25-45},
	publisher = {Springer},
	series = {Studies in Computational Intelligence},
	url = {http://dblp.uni-trier.de/db/series/sci/sci164.html#HuangZK09},
	volume = {164},
	year = {2009},
	biburl = {http://www.bibsonomy.org/bibtex/2b91f87a85a7d9376cfd78808059446b1/dblp},
	description = {dblp},
	date = {2008-11-13}, ee = {http://dx.doi.org/10.1007/978-3-540-85644-3_2},
	keywords = {dblp }
}

@inproceedings{conf/pvm/KumarDBCMRSH08,
	title = {Architecture of the Component Collective Messaging Interface.},
	author = {Sameer Kumar and Gábor Dózsa and Jeremy Berg and Bob Cernohous and Douglas Miller and Joe Ratterman and Brian E. Smith and Philip Heidelberger},
	booktitle = {PVM/MPI},
	crossref = {conf/pvm/2008},
	editor = {Alexey L. Lastovetsky and Tahar Kechadi and Jack Dongarra},
	pages = {23-32},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/pvm/pvm2008.html#KumarDBCMRSH08},
	volume = {5205},
	year = {2008},
	biburl = {http://www.bibsonomy.org/bibtex/27b8d8ef463160ea448928725e01ecaa0/dblp},
	description = {dblp},
	date = {2008-11-10}, ee = {http://dx.doi.org/10.1007/978-3-540-87475-1_10}, isbn = {978-3-540-87474-4},
	keywords = {dblp }
}

@incollection{loepucl5137,
	title = {Formally linking MDG and HOL based on a verified MDG system},
	address = {Heidelberg},
	author = {H. Xiong and P. Curzon and S. Tahar and A. Blandford},
	booktitle = {Integrated Formal Methods},
	editor = {G. Goos and J. Hartmanis and J. van Leeuwen},
	note = {The original publication is available at www.springerlink.com},
	number = {2335},
	pages = {205--224},
	publisher = {Springer Berlin},
	series = {Lecture Notes in Computer Science},
	url = {http://eprints.ucl.ac.uk/5137/},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/2ec11cf40d7478fe9f37970344d625b69/uclic},
	description = {UCLIC eprints as of October 2008},
	abstract = {We describe an approach for formally linking a symbolic state enumeration system and a theorem proving system based on a verified version of the former. It has been realized using a simplified version of the MDG system and the HOL system. Firstly, we have verified aspects of correctness of a simplified version of the MDG system. We have made certain that the semantics of a program is preserved in those of its translated form. Secondly, we have provided a formal linkage between the MDG system and the HOL system based on importing theorems. The MDG verification results can be formally imported into HOL to form a HOL theorem. Thirdly, we have combined the translator correctness theorems and importing theorems. This allows the MDG verification results to be imported in terms of a high level language (MDG-HDL) rather than a low level language. We also summarize a general method to prove existential theorems for the design. The feasibility of this approach is demonstrated in a case study that integrates two applications: hardware verification (in MDG) and usability verification (in HOL). A single HOL theorem is proved that integrates the two results.},
	keywords = {deductive-theorem-proving hardware-verification hybrid-verification-systems symbolic-state-enumeration usability-verification }
}

@article{loepucl5153,
	title = {Providing a formal linkage between MDG and HOL},
	author = {H.Y. Xiong and P. Curzon and S. Tahar and A. Blandford},
	journal = {Formal Methods in System Design},
	month = {April},
	note = {The original publication is available at www.springerlink.com},
	number = {2},
	pages = {83--116},
	url = {http://eprints.ucl.ac.uk/5153/},
	volume = {30},
	year = {2007},
	biburl = {http://www.bibsonomy.org/bibtex/294c56d0895b952b0a45e54032f24f29a/uclic},
	description = {UCLIC eprints as of October 2008},
	abstract = {We describe an approach for formally verifying the linkage between a symbolic state enumeration system and a theorem proving system. This involves the following three stages of proof. Firstly we prove theorems about the correctness of the translation part of the symbolic state system. It interfaces between low level decision diagrams and high level description languages. We ensure that the semantics of a program is preserved in those of its translated form. Secondly we prove linkage theorems: theorems that justify introducing a result from a state enumeration system into a proof system. Finally we combine the translator correctness and linkage theorems. The resulting new linkage theorems convert results to a high level language from the low level decision diagrams that the result was actually proved about in the state enumeration system. They justify importing low-level external verification results into a theorem prover. We use a linkage between the HOL system and a simplified version of the MDG system to illustrate the ideas and consider a small example that integrates two applications from MDG and HOL to illustrate the linkage theorems.},
	keywords = {Formal-hardware-verification Verification-system-correctness hybrid-verification-systems usability-verification }
}

@incollection{loepucl5137,
	title = {Formally linking MDG and HOL based on a verified MDG system},
	address = {Heidelberg},
	author = {H. Xiong and P. Curzon and S. Tahar and A. Blandford},
	booktitle = {Integrated Formal Methods},
	editor = {G. Goos and J. Hartmanis and J. van Leeuwen},
	note = {The original publication is available at www.springerlink.com},
	number = {2335},
	pages = {205--224},
	publisher = {Springer Berlin},
	series = {Lecture Notes in Computer Science},
	url = {http://eprints.ucl.ac.uk/5137/},
	year = {2002},
	biburl = {http://www.bibsonomy.org/bibtex/2ec11cf40d7478fe9f37970344d625b69/spdegabrielle},
	description = {UCLIC},
	abstract = {We describe an approach for formally linking a symbolic state enumeration system and a theorem proving system based on a verified version of the former. It has been realized using a simplified version of the MDG system and the HOL system. Firstly, we have verified aspects of correctness of a simplified version of the MDG system. We have made certain that the semantics of a program is preserved in those of its translated form. Secondly, we have provided a formal linkage between the MDG system and the HOL system based on importing theorems. The MDG verification results can be formally imported into HOL to form a HOL theorem. Thirdly, we have combined the translator correctness theorems and importing theorems. This allows the MDG verification results to be imported in terms of a high level language (MDG-HDL) rather than a low level language. We also summarize a general method to prove existential theorems for the design. The feasibility of this approach is demonstrated in a case study that integrates two applications: hardware verification (in MDG) and usability verification (in HOL). A single HOL theorem is proved that integrates the two results.},
	keywords = {UCLIC deductive enumeration, hardware hybrid proving, state symbolic systems, theorem usability verification verification, }
}

@article{loepucl5153,
	title = {Providing a formal linkage between MDG and HOL},
	author = {H.Y. Xiong and P. Curzon and S. Tahar and A. Blandford},
	journal = {Formal Methods in System Design},
	month = {April},
	note = {The original publication is available at www.springerlink.com},
	number = {2},
	pages = {83--116},
	url = {http://eprints.ucl.ac.uk/5153/},
	volume = {30},
	year = {2007},
	biburl = {http://www.bibsonomy.org/bibtex/294c56d0895b952b0a45e54032f24f29a/spdegabrielle},
	description = {UCLIC},
	abstract = {We describe an approach for formally verifying the linkage between a symbolic state enumeration system and a theorem proving system. This involves the following three stages of proof. Firstly we prove theorems about the correctness of the translation part of the symbolic state system. It interfaces between low level decision diagrams and high level description languages. We ensure that the semantics of a program is preserved in those of its translated form. Secondly we prove linkage theorems: theorems that justify introducing a result from a state enumeration system into a proof system. Finally we combine the translator correctness and linkage theorems. The resulting new linkage theorems convert results to a high level language from the low level decision diagrams that the result was actually proved about in the state enumeration system. They justify importing low-level external verification results into a theorem prover. We use a linkage between the HOL system and a simplified version of the MDG system to illustrate the ideas and consider a small example that integrates two applications from MDG and HOL to illustrate the linkage theorems.},
	keywords = {Formal Hybrid UCLIC Usability Verification correctness; hardware system systems; verification verification; }
}

@inproceedings{conf/ispass/HasanT08,
	title = {Performance Analysis of ARQ Protocols using a Theorem Prover.},
	author = {Osman Hasan and Sofiene Tahar},
	booktitle = {ISPASS},
	crossref = {conf/ispass/2008},
	pages = {85-94},
	publisher = {IEEE},
	url = {http://dblp.uni-trier.de/db/conf/ispass/ispass2008.html#HasanT08},
	year = {2008},
	biburl = {http://www.bibsonomy.org/bibtex/21d78438a4b5afa3765c72687a6aa4cec/dblp},
	description = {dblp},
	ee = {http://dx.doi.org/10.1109/ISPASS.2008.4510741}, date = {2008-10-22},
	keywords = {dblp }
}

@inproceedings{conf/tphol/Miller08,
	title = {Will This Be Formal?},
	author = {Steven P. Miller},
	booktitle = {TPHOLs},
	crossref = {conf/tphol/2008},
	editor = {Otmane Aït Mohamed and César Muñoz and Sofiène Tahar},
	pages = {6-11},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/tphol/tphol2008.html#Miller08},
	volume = {5170},
	year = {2008},
	biburl = {http://www.bibsonomy.org/bibtex/290496c44490dab38d9f9a52bb8f907dd/dblp},
	description = {dblp},
	date = {2008-10-20}, ee = {http://dx.doi.org/10.1007/978-3-540-71067-7_2}, isbn = {978-3-540-71065-3},
	keywords = {dblp }
}

@inproceedings{conf/tphol/CockKS08,
	title = {Secure Microkernels, State Monads and Scalable Refinement.},
	author = {David Cock and Gerwin Klein and Thomas Sewell},
	booktitle = {TPHOLs},
	crossref = {conf/tphol/2008},
	editor = {Otmane Aït Mohamed and César Muñoz and Sofiène Tahar},
	pages = {167-182},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	url = {http://dblp.uni-trier.de/db/conf/tphol/tphol2008.html#CockKS08},
	volume = {5170},
	year = {2008},
	biburl = {http://www.bibsonomy.org/bibtex/222aa6c7ae6dfade1ce29ce26b3a7e321/dblp},
	description = {dblp},
	date = {2008-10-20}, ee = {http://dx.doi.org/10.1007/978-3-540-71067-7_16}, isbn = {978-3-540-71065-3},
	keywords = {dblp }
}