| 2008 | CAV | A Practical Approach to Word Level Model Checking of Industrial Netlists. | Per Bjesse |
| 2008 | FMCAD | Word-Level Sequential Memory Abstraction for Model Checking. | Per Bjesse |
| 2007 | DATE | 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 |
| 2005 | ICCAD | Automatic generalized phase abstraction for formal verification. | Per Bjesse, James H. Kukula |
| 2004 | DATE | Using Counter Example Guided Abstraction Refinement to Find Complex Bugs. | Per Bjesse, James H. Kukula |
| 2004 | ICCAD | DAG-aware circuit compression for formal verification. | Per Bjesse, Arne Borlv |
| 2003 | SAT | Guiding SAT Diagnosis with Tree Decompositions. | Per Bjesse, James H. Kukula, Robert F. Damiano, Ted Stanion, Yunshan Zhu |
| 2002 | DAC | A proof engine approach to solving combinational design automation problems. | Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna |
| 2001 | CAV | Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. | Per Bjesse, Tim Leonard, Abdel Mokkedem |
| 2000 | FMCAD | SAT-Based Verification without State Space Traversal. | Per Bjesse, Koen Claessen |
| 2000 | TACAS | Symbolic Reachability Analysis Based on SAT-Solvers. | Parosh Aziz Abdulla, Per Bjesse, Niklas En |
| 1999 | CAV | Automatic Verification of Combinatorial and Pipelined FFT. | Per Bjesse |
| 1998 | ICFP | Lava: Hardware Design in Haskell. | Per Bjesse, Koen Claessen, Mary Sheeran, Satnam Singh |