Bibliography

1
H. Amjad.
BDD representation judgements in HOL.
In R. J. Boulton and P. B. Jackson, editors, Emerging Trends track of Theorem Proving in Higher Order Logics (TPHOLs), number EDI-INF-RR-0046 in Technical Reports, pages 17-26. Informatics Division, University of Edinburgh, 2001.

2
H. Amjad.
Formalizing the translation of CTL into L\({}_\mu\).
In David A. Basin and Burkhart Wolff, editors, Emerging Trends track of Theorem Proving in Higher Order Logics (TPHOLs), number 187 in Technical Reports, pages 207-217. Institut für Informatik, Albert-Ludwigs-Universität, 2003.

3
H. Amjad.
Implementing abstraction refinement for model checking in HOL.
In David A. Basin and Burkhart Wolff, editors, Emerging Trends track of Theorem Proving in Higher Order Logics (TPHOLs), number 187 in Technical Reports, pages 219-228. Institut für Informatik, Albert-Ludwigs-Universität, 2003.

4
H. Amjad.
Programming a symbolic model checker in a fully expansive theorem prover.
In David A. Basin and Burkhart Wolff, editors, Theorem Proving in Higher Order Logics, volume 2758 of LNCS, pages 171-187. Springer-Verlag, 2003.

5
H. Amjad.
Combining model checking and theorem proving.
Technical Report UCAM-CL-TR-601, University of Cambridge Computer Laboratory, 2004.
Ph. D. Thesis.

6
H. Amjad.
Model checking the AMBA protocol in HOL.
Technical Report UCAM-CL-TR-601, University of Cambridge Computer Laboratory, 2004.

7
H. Amjad.
Shallow lazy proofs.
In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, volume 3603 of LNCS, pages 35-49. Springer, 2005.

8
H. Amjad.
Verification of AMBA using a combination of model checking and theorem proving.
In R. Lazic and R. Nagarajan, editors, Automated Verification of Critical Systems, volume 145 of Electronic Notes in Theoretical Computer Science, pages 45-61. Springer, 2005.
To appear.

9
H. Amjad.
Compressing propositional refutations.
In S. Merz and T. Nipkow, editors, Automated Verification of Critical Systems, volume 1829 of ENTCS. Springer, 2006.

10
H. Amjad.
A compressing translation of propositional resolution to natural deduction.
In Boris Konev and Frank Wolter, editors, Frontiers of Combining Systems, volume 4720 of LNAI. Springer, 2007.

11
H. Amjad.
LCF-style propositional simplification with BDDs and SAT solvers.
In César Muñoz Otmane Ait Mohamed and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of LNCS. Springer, 2008.

12
H. Amjad and R. Bornat.
Towards automatic stability analysis for rely-gurantee proofs.
In Neil Jones and Markus Müller-Olm, editors, Verification, Model Checking and Abstract Interpretation (VMCAI), LNCS. Springer, 2009.
To appear.

13
Tjark Weber and Hasan Amjad.
Efficiently checking propositional refutations in HOL theorem provers.
JAL, 2007.
In press.



Hasan 2008-11-06