Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. A critical phase of the co-design process is to decompose a program into hardware and software. This paper proposes an algebraic partitioning algorithm whose correctness is verified in program algebra. The authors introduce a program analysis phase before program partitioning and develop a collection of syntax-based splitting rules. The former provides the information for moving operations from software to hardware and reducing the interaction between components, and the latter supports a compositional approach to program partitioning. The work is partially supported by the National Natural Science Foundation of China under grant Nos.69873003 and 69983001. QIN Shengchao was born in 1974. He is a Ph.D. candidate in Department of Informatics, School of Mathematical Science, Peking University. He got his B.S. degree in the same department in 1997. His research interests include formal methods and semantics, unifying theories to programming, and formal engineering approaches. HE Jifeng is a senior research fellow of UNU/IIST. He was a senior research fellow of the programming research group, Oxford University before 1998. He is a professor of computer science in East China Normal University since 1986, Shanghai. His research interest lies in the sound methods of specification of computer systems, communications, application of standards, and the techniques for designing and implementing those specifications in software and/or hardware with high reliability and low cost. QIU Zongyan is a professor of computer science and deputy head of the Department of Informatics, Peking University. His research interests are formal methods, programming languages, and real-time systems. ZHANG Naixiao is a professor of computer science in the Department of Informatics, Peking University. His research interests are formal methods and domain-specific languages.