Lava: Hardware Design in Haskell. - Per Bjesse; Koen Claessen; Mary Sheeran; Satnam Singh (ICFP, 1998)

Automatic Verification of Combinatorial and Pipelined FFT. - Per Bjesse (CAV, 1999)

SAT-Based Verification without State Space Traversal. - Per Bjesse; Koen Claessen (FMCAD, 2000)

Symbolic Reachability Analysis Based on SAT-Solvers. - Parosh Aziz Abdulla; Per Bjesse; Niklas Eén (TACAS, 2000)

Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. - Per Bjesse; Tim Leonard; Abdel Mokkedem (CAV, 2001)

Gate Level Description of Synchronous Hardware and Automatic Verification Based on Theorem Proving. - Per Bjesse (2001)

A proof engine approach to solving combinational design automation problems. - Gunnar Andersson; Per Bjesse; Byron Cook; Ziyad Hanna (DAC, 2002)

Industrial Model Checking Based on Satisfiability Solvers. - Per Bjesse (SPIN, 2002)

Guiding SAT Diagnosis with Tree Decompositions. - Per Bjesse; James H. Kukula; Robert F. Damiano; Ted Stanion; Yunshan Zhu (SAT, 2003)

Design automation with mixtures of proof strategies for propositional logic. - Gunnar Andersson; Per Bjesse; Byron Cook; Ziyad Hanna (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2003)

Using Counter Example Guided Abstraction Refinement to Find Complex Bugs. - Per Bjesse; James H. Kukula (DATE, 2004)

DAG-aware circuit compression for formal verification. - Per Bjesse; Arne Borälv (ICCAD, 2004)

Automatic generalized phase abstraction for formal verification. - Per Bjesse; James H. Kukula (ICCAD, 2005)

Practical Issues in Sequential Equivalence Checking through Alignability: Handling Don't Cares and Generating Debug Traces. - In-Ho Moon; Per Bjesse; Carl Pixley (HLDVT, 2006)

A compositional approach to the combination of combinational and sequential equivalence checking of circuits without known reset states. - In-Ho Moon; Per Bjesse; Carl Pixley (DATE, 2007)

A Practical Approach to Word Level Model Checking of Industrial Netlists. - Per Bjesse (CAV, 2008)

Word-Level Sequential Memory Abstraction for Model Checking. - Per Bjesse (FMCAD, 2008)

Word level bitwidth reduction for unbounded hardware model checking. - Per Bjesse (Formal Methods Syst. Des., 2009)