I am a former PhD-student at the department of Computer Science, Chalmers Tekniska Högskola. After graduation, I moved to Portland, Oregon to work for Prover Technology as a member of the research staff. I am currently working in Synopsys Advanced Technology group doing research on formal verification techniques for hardware.

• I will chair the "Advances in SAT" session at ICCAD in November.
• I chaired the "Advances in SAT" session at DATE in Paris in February.
• I was on the program commitee for the verification track of Design, Automation, and Test in Europe DATE'04.
• I chaired the "Advances in SAT" session at DAC'03 in Anaheim.
• I am on the program committee for BMC'03, a workshop associated with CAV'03.
• In August 2002, I gave a talk titled "An On-the-fly Compression Approach to Fast Boolean Circuit Minimization" at the Dagstuhl workshop on formal equivalence verification.
• In June 2002, I presented a paper on the architecture of Prover's proof engine framework. The paper includes a comparison between the mixtures of individual proof techniques that we use, and methods like BDDs and the search-based SAT solver Chaff on public and industrial benchmarks.
• I was on the program committe for DCC'02, an affiliated workshop with the ETAPS conferences.
• I gave an invited presentation on industrial model checking using satisfiability solvers at the SPIN'02 workshop.
• In November 2001, I gave an invited tutorial on model checking using SAT solvers at ICCAD 2001.

• DAG-Aware Circuit Compression For Formal Verification, Per Bjesse, Arne Boralv, ICCAD'04, 2004
• Using Counter Example Guided Abstraction Refinement to Find Complex Bugs, Per Bjesse, James Kukula, DATE'04, 2004
• Guiding SAT Diagnosis with Tree Decompositions, Per Bjesse, James Kukula, Robert Damiano, Ted Stanion, Yunshan Zhu, SAT'03, 2003 © Springer-Verlag
• Design Automation with Mixtures of Proof Strategies for Propositional Logic, Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna, Transactions on Computer Aided Design, August 2003
• A Proof Engine Approach to Solving Combinational Design Automation Problems, Gunnar Andersson, Per Bjesse, Byron Cook, Ziyad Hanna, DAC'02
• Gate Level Description of Synchronous Hardware and Automatic Verification Based on Theorem Proving, Per Bjesse, PhD-thesis
• SAT-based Approaches to Model Checking: An Overview and Tutorial, Per Bjesse, Mary Sheeran, Gunnar Stålmarck, submitted for publication
• Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers, Per Bjesse, Tim Leonard, Abdel Mokkedem, CAV'01, 2001 © Springer-Verlag
• SAT-based Verification without State Space Traversal, Per Bjesse, Koen Claessen, FMCAD'00, 2000 © Springer-Verlag
• Symbolic Reachability Analysis based on SAT-Solvers, Parosh Aziz Abdulla, Per Bjesse, Niklas Eén, TACAS'00, 2000 © Springer-Verlag (Got the EAPLS award---best paper presented in any of the five ETAPS conferences)
• Symbolic Model Checking with Sets of States Represented as Formulas , Per Bjesse, Technical Report CS-1999-102 (June 1999) (supersedes CS-1999-100 (March 1999)), Dept. of Computer Science, Chalmers University of Technology and Göteborg University
• Automatic Verification of Combinational and Pipelined FFT Circuits, Per Bjesse, CAV'99, 1999 © Springer-Verlag
• Lava: Hardware design in Haskell, Per Bjesse, Koen Claessen, Mary Sheeran, Satnam Singh, ICFP'98, 1998
• Specification of signal processing programs in a pure functional language and compilation to distributed architectures, Master's Thesis, 1997

My primary areas of interest include theorem proving, formal methods and logic. I organized the seminar series of the formal methods group from 1998 to 2000.

My thesis work included exploration of alternatives to traditional model checking, hardware verification by automated theorem proving, and development of the Lava hardware verification platform.

During the autumn of 2000, I interned three months at Compaq's Alpha development group outside of Boston. This was the last work on my thesis (which I successfully defended on the 7th of May, 2001).

I, Mary Sheeran, Koen Claessen, and Carl Johan Block developed two new courses in the area of formal methods 1998, that we gave three times during my time at the department:

• Formal methods for software
• Hardware description and verification

Why not check out some of my interests?