
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Mark Aagaard, Miriam Leeser, "Verifying a LogicSynthesis Algorithm and Implementation: A Case Study in Software Verification," IEEE Transactions on Software Engineering, vol. 21, no. 10, pp. 822833, October, 1995.  
BibTex  x  
@article{ 10.1109/32.469458, author = {Mark Aagaard and Miriam Leeser}, title = {Verifying a LogicSynthesis Algorithm and Implementation: A Case Study in Software Verification}, journal ={IEEE Transactions on Software Engineering}, volume = {21}, number = {10}, issn = {00985589}, year = {1995}, pages = {822833}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.469458}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Verifying a LogicSynthesis Algorithm and Implementation: A Case Study in Software Verification IS  10 SN  00985589 SP822 EP833 EPD  822833 A1  Mark Aagaard, A1  Miriam Leeser, PY  1995 KW  Software verification KW  theorem proving KW  logic synthesis KW  weak division KW  hardware verification. VL  21 JA  IEEE Transactions on Software Engineering ER   
[1] R.K. Brayton and C. McMullen,“Decomposition and factorization of boolean expressions,” Int’l Symp. on Circuits and Systems, 1982.
[2] M.D. Aagaard and M.E. Leeser,“A methodology for efficient hardware verification,” Formal Methods in System Design, vol. 5, no. 1&2, pp. 95117, July 1994.
[3] R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[4] M. Leeser,R. Chapman,M. Aagaard,M. Linderman,, and S. Meier,“High level synthesis and generating FPGAs with the BEDROC system,” J. of VLSI Signal Processing, vol. 6, no. 2, pp. 193216, Aug. 1993.
[5] M.D. Aagaard,“A verified system for logic synthesis,” Master’s thesis, School of Electrical Engineering, Cornell Univ., Jan. 1992.
[6] M.D. Aagaard and M.E. Leeser,“A theorem proving based methodology for software verification,” Tech. Rep. Cornell CS:TR931335, Dept. of Computer Science, Cornell Univ., Mar. 1993.
[7] M.D. Aagaard and M.E. Leeser,“PBS: Proven Boolean simplification,” IEEE Transactions on Computer Aided Design, vol. 13, no. 4, Apr. 1994.
[8] J.M. Wing,“A specifier’s introduction to formal methods,” IEEE Computer, vol. 23, pp. 824, Sept. 1990.
[9] P.A. Lindsay,“A survey of mechanical support for formal reasoning,” Software Eng. J., pp. 327, Jan. 1988.
[10] D.R. Musser,“Abstract data type specification in the AFFIRM system,” IEEE Transactions on Software Engineering, vol. 6, no. 1, pp. 2432, 1980.
[11] D. Kapur and P. Narendran,“The rewrite rule laboratory (RRL),” J. Siekman, ed., Conf. on Automated Deduction.New York: SpringerVerlag, July 1986.
[12] S.J. Garland and J.V. Guttag,“An overview of LP, the Larch proof assistant,” Rewriting Techniques, 1989, pp. 137151.
[13] M. Broy,“Experiences with software specification and verification using LP, the Larch proof assistant,” Tech. Rep., 93, DEC Systems Research Center, 1992.
[14] D.I. Good,“Mechanical proofs about computer programs,” C.A.R. Hoare and J.C. Shepherdson, eds., Mathematical Logic and Programming Languages.Englewood Cliffs, N.J.: Prentice Hall, 1984.
[15] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[16] J. of Automated Reasoning, Dec. 1989, Special Issue on BoyerMoore Theorem Prover.
[17] Y. Yu,“Automated proofs of object code for a widely used microprocessor,” Tech. Rep. 113, DEC Systems Research Center, Oct. 1993.
[18] M. Gordon,R. Milner,, and C. Wadsworth,Edinburgh LCF: A Mechanized Logic of Computation, vol. 78. New York: Springer Verlag, 1979, Lecture Notes in Computer Science.
[19] M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0521441897. Cambridge Univ. Press, 1993.
[20] L. Paulson and T. Nipkow,“Isabelle tutorial and user’s manual,” Tech. Rep. 189, Cambridge Univ. Computer Laboratory, Jan. 1990.
[21] N. Shankar,S. Owre,, and J.M. Rushby,“The PVS proof checker: A reference manual,” draft tech. rep., SRI International, 1993.
[22] A. Bundy,F. Van Harmelen,J. Hesketh,, and A. Smaill,“Experiments with proof plans for induction,” J. of Automated Reasoning, vol. 7, no. 3, pp. 303324, 1991.
[23] T. Melham,“Formalizing abstraction mechanisms for hardware verification in higher order logic,” PhD thesis, Cambridge Univ. Computer Laboratory, Aug. 1990, Technical Report no. 201.
[24] J. Camilleri and T. Melham,“Reasoning with inductively defined relations in the HOL theorem prover,” Tech. Rep. 265, Univ. of Cambridge Computer Laboratory, Aug 1992.
[25] J. Rushby and F. von Henke, "Formal Verification of Algorithms for Critical Systems," IEEE Trans. Software Engineering, vol. 19, no. 1, pp. 1323, Jan. 1993.
[26] ——,“The notion of proof in hardware verification,”J. Automated Reasoning, vol. 5, pp. 127–139, 1989.
[27] R.K. Brayton,R. Rudell, et al., “MIS: A multiplelevel logic optimization system,” IEEE Transactions on Computer Aided Design, vol. 6, no. 6, 1987.
[28] R. Milner,M. Tofte,, and R. Harper,The Definition of Standard ML.Cambridge, Mass.: MIT Press, 1990.
[29] M. VanInwegen and E. Gunter,“HOLML,” J.J. Joyce and C.J.H. Seger, eds., Higher Order Logic Theorem Proving and Its Applications.New York: Springer Verlag, 1993.
[30] D. Syme,“Reasoning with the formal definition of Standard ML in HOL,” J.J. Joyce and C.J.H. Seger, eds., Higher Order Logic Theorem Proving and Its Applications.New York: Springer Verlag, 1993.
[31] S. Maharaj and E. Gunter,“Studying the ML module system in HOL,” T.F. Melham and J. Camilleri, eds., Higher Order Logic Theorem Proving and Its Applications.New York: Springer Verlag, pp. 346361, 1994.