UNIVERSITY OF CALIFORNIA, BERKELEY
SANTA BARBARA • SANTA CRUZ


BERKELEY  • DAVIS • IRVINE • LOS ANGELES  • MERCED •  RIVERSIDE  • SAN DIEGO  • SAN FRANCISCO








Professor Koushik Sen        BERKELEY, CALIFORNIA 94720
Computer Science Division
735 Soda Hall #1776
University of California
Berkeley CA 94720-1776
PHONE: (510) 642-2420
FAX: (510) 642-3962
EMAIL: ksen@cs.berkeley.edu


September 11, 2026




To whom it may concern: 


It is my great honor to write this letter of recommendation for Kevin Laeufer.  I have known Kevin for a decade.  I was Kevin’s Ph.D. advisor at UC Berkeley.  Kevin is smart, hard-working, and driven.  He has excellent communication skills and is an exemplary mentor.  He is well on his way to becoming a world-class researcher and teacher.
 
Kevin joined UC Berkeley in Fall of 2016 as an exchange student from Germany.  In the Fall of 2016, Kevin took my graduate course on Advanced Topics in Testing, Debugging, and Program Analysis.  I was impressed by Kevin’s drive and dedication to research.  He was one of the sharpest students in the class.  He is kind of a perfectionist, takes his research seriously, and pays attention to details. I encouraged him to apply for a Ph.D.  Kevin got accepted to all top schools, including UC Berkeley, MIT, and Stanford.  I was thrilled that I managed to recruit and keep him at UC Berkeley. 
   
Kevin’s primary research falls under the area of hardware design verification, testing, debugging, and repair.  One of his early research projects focused on efficient fuzz testing of RTL circuits.  Fuzz testing is a light-weight automated test generation technique for software that has gained massive traction in industry. Fuzz testing has found vast numbers of critical bugs and security vulnerabilities in real-world software. The recent success in fuzz testing has come from the coverage-guided fuzzing (CGF) algorithm. Conventional fuzz testing works by generating test inputs randomly from scratch or by randomly mutating a set of seed test inputs. The key innovation behind coverage-guided fuzzing over conventional fuzzing is that it takes the coverage information into account while generating new random inputs. Specifically, if CGF finds that some randomly generated input discovers a new coverage point, it treats the input as "interesting." In subsequent rounds, CGF keeps mutating the interesting inputs hoping that the mutated inputs will discover new coverage points. One of the leading CGF tools, American Fuzzy Lop (or simply AFL) (http://lcamtuf.coredump.cx/afl/ ) developed by Google, has found vulnerabilities in a broad array of programs (e.g., Firefox, Internet Explorer, OpenSSH, PCRE, GCC).


After joining UC Berkeley, Kevin worked on an effective technique for fuzzing RTL circuits.  Dynamic verification is widely used to increase confidence in the correctness of RTL circuits during the pre-silicon design phase. Despite numerous attempts over the last decades to automate the stimuli generation based on coverage feedback, coverage-guided fuzzing (CGF) has yet to find the widespread adoption that one would expect in testing and verifying hardware designs.  Kevin proposed a new approach to the CGF problem, which requires minimal setup and takes advantage of FPGA-accelerated simulation for rapid testing.  While working on the project, Kevin found that resetting a circuit is a crucial bottleneck in CGF.  Kevin proposed and implemented a series of transformation passes that make it feasible to reset arbitrary RTL designs quickly, a requirement for deterministic test execution. He also developed a fully-featured implementation of the testing methodology, called RFUZZ, and released it as open-source software to the research community. Both Jonathan Bachrach and I were hands-off on the project.  Kevin figured out how to speed up fuzzing for RTL circuits.  A paper based on this technique appeared at ICCAD 2018, one of the two top conferences in computer-aided design.  It is rare to see a first-year Ph.D. student carry out a research project with so little help from his advisors and get a paper accepted.  The paper has had a significant impact and has inspired many follow-up projects on hardware fuzzing in the research community.


While working on RFUZZ, Kevin realized that fuzzing could be improved if he could collect various other coverage information during a circuit simulation.  However, many open-source and academic RTL circuit simulators do not support collecting rich or custom coverage information.  Kevin created an elegant approach to collecting automated coverage metrics, including line, toggle, and finite state machine coverage, so the implementation is independent of the backend simulator.  Kevin came up with the key insight that if every simulator implements a single new cover primitive, then other metrics can be implemented through a compiler pass.  Kevin built a prototype for the Chisel hardware construction language and demonstrated support across three software simulators, the FPGA-accelerated FireSim simulator, and a formal tool. Kevin further demonstrated for the first time that he could collect detailed line coverage while booting Linux with FireSim at a target frequency of 65 MHz.  Kevin’s work showed a general approach to how coverage of high-level features can be captured with one simple primitive for new hardware languages.  Kevin’s work on coverage metrics is ground-breaking in that with Kevin’s tool, now every simulator can implement Kevin’s single cover primitive and get a rich set of coverage information for free, which is necessary for testing and debugging RTL circuits.  A paper based on this work appeared at the prestigious ACM conference ASPLOS 2023.  Kevin has also made the tool publicly available. Again, Kevin ran the show here: he came up with the idea, implemented it, and demonstrated its effectiveness in the real world.  I merely listened to what Kevin was doing in our one-on-one research meetings.




Kevin made a major contribution to the widely popular and open-source hardware construction language Chisel, which made a formal technique called bounded model checking (BMC) accessible to regular developers.  Specifically, Kevin added bounded model checking as part of the ChiselTest library which is used by many Chisel projects. Hardware construction languages (HCL) aim to improve design performance by enabling developers to create generators that describe an entire design space, not just a single instance of a circuit block. Kevin’s tool showed how generators could make even simple formal techniques like bounded model checking more powerful, making it easy to create checkers that are parameterized on signal sizes, FIFO depths, and more.  Moreover, Kevin’s work investigates exact replay, which allows debugging infrastructure for dynamic testing to be re-used.  Kevin’s contribution has been widely recognized: the upstream Chisel project used Kevin’s tool to verify library components, and it has already uncovered several bugs in FIFO implementations, inspired further work within the community, and has even been integrated into a formal verification course at UC Santa Cruz.  I am proud of Kevin’s work because it made formal verification available to developers who may not be formal verification experts.


Debugging highly parallel hardware designs is complex and time-consuming, with manual inspection of signal traces being the most common approach.  Automated program repair was initially proposed as a fully autonomous solution but faced limitations due to incomplete tests, leading to deficient or incorrect repairs.  Kevin developed a novel idea that reframed automatic program repair as a debugging tool, focusing on providing rapid repair suggestions. The idea allows users to concentrate on simpler bugs and review multiple suggestions. Kevin's repair tool for RTL circuits in Verilog combines symbolic repair templates and SMT-based bounded model checking, outperforming the state-of-the-art tool, CirFix, in effectiveness and speed.  A key challenge in repairing hardware designs is the length of failing tests, which can require an SMT solver to examine thousands of system unrollings. Kevin overcame this by using an adaptable window for unrolling around the bug manifestation time step, enabling the approach to scale to long tests and resulting in a more efficient repair process.  In the experimental evaluation, Kevin’s tool correctly repairs half of the benchmarks, while the current state-of-the-art tool CirFix only correctly repairs one-third. Moreover, Kevin’s tool provides an answer in less than ten seconds, while CirFix often takes minutes or hours to generate a single repair.  This speed makes the tool practical to use during debugging.  I am very excited about the tool and the results.  The paper on this work, RTL-Repair: Fast Symbolic Repair of Hardware Design Code, appeared at ASPLOS 2024. 


After completing his Ph.D. at UC Berkeley in 2024, Kevin moved to Cornell University as a Research Associate, where he has continued to do excellent research.  He co-authored Zoomie, a software-like debugging tool for FPGAs, which also appeared at ASPLOS 2024.  He is a co-author of Surfer, a modern, extensible, open-source waveform viewer published at CAV 2025.  Surfer translates bit vectors into semantically meaningful values and integrates with simulation and formal verification tools; hardware classes at Cornell, MIT, UC Santa Cruz, and JKU Linz recommend it to their students, and it builds on wellen, a waveform library that Kevin wrote and maintains.  Most recently, Kevin conceived and led Paso, a domain-specific language for specifying RTL communication protocols as succinct imperative programs.  The same Paso program can both drive and monitor transactions, and a novel reconstructor algorithm infers a transaction-level trace directly from a waveform.  Paso has already uncovered protocol violation bugs in real-world Wishbone and AXI-Stream implementations.  Kevin wrote the Paso paper with a Ph.D. student and two undergraduate researchers he has mentored at Cornell, and it is currently under submission at a top conference.


Kevin’s proposal writing skills are remarkable.  Kevin not only came up with the project idea to add formal verification to ChiselTest, but he also wrote a full proposal for the Semiconductor Research Corporation (SRC) grant, one of the most competitive grants.  Jonathan Bachrach and I helped him at a high level to structure the proposal.  We did not contribute to the proposed ideas and the proposal's contents.  His proposal got accepted for funding for three years.  It is rare for a proposal written by a second-year graduate student to win one of these highly competitive grants.  More recently, in 2026, Kevin wrote a successful proposal for a Jane Street Hardware Research Collaboration Grant, with Adrian Sampson as PI, to fund his work on Paso.  Kevin won’t have any problem raising funds for his research.
 
Kevin’s participation in the open-source community is exemplary.  We have already seen how research in programming languages and software engineering has benefited from using mature open-source software ecosystems. However, the hardware community has been behind in this area, limiting the scope of research topics for academic researchers who cannot access or modify commercial tools. Fortunately, a new generation of open-source hardware tools is emerging from academia and the open-source community. Kevin's Ph.D. research projects used the FIRRTL hardware compiler, part of the open-source hardware construction language Chisel. Kevin has been an active member of the Chisel community since 2019, participating in developer meetings, presenting at conferences, and providing support to users. He has also been the maintainer of the official ChiselTest verification library since 2020. 


Teaching is Kevin’s passion, and he does it really well.  Kevin has taught three distinct classes at UC Berkeley, focusing on course and instructional design.  In Fall 2025, he co-taught CS 3410, Computer System Organization and Programming, at Cornell as a visiting lecturer; he revamped the lab sections, previously one of the least popular parts of the class, and students responded with very positive feedback. His teaching approach strives for continuous improvement, eliminating barriers to learning, and incorporating visualization and experimentation in assignments. With experience as a TA for various classes and as a guest lecturer at UC Santa Cruz, Kevin is well-equipped to teach undergraduate and graduate-level computer science courses and is keenly interested in developing a class on automated bug-finding and verification techniques. His teaching philosophy revolves around feedback-driven instructional design, respecting students' time, and utilizing experiments and visualization to enhance learning.


Kevin has already mentored nearly twenty undergraduate and graduate students at UC Berkeley and Cornell.  He is an excellent mentor.  Kevin adopts a student-centered approach as a mentor in our research meetings, concentrating on student-defined goals and fostering a welcoming community. His mentoring method involves setting and updating goals in semesterly meetings, providing students with opportunities, helping them overcome challenges, and nurturing a sense of community.  Below I highlight some feedback Kevin got from his mentees:


Undergraduate Student A: 
"I was very fortunate to work with Kevin as my research mentor, and he changed the course of my academic career. Kevin consistently went above and beyond to provide guidance, support, and opportunities that helped me grow both personally and professionally, such as inviting me to weekly lunches with other researchers and helping me attend a research school that I would not have known about if not for him. Kevin's commitment to the success of his students is unmatched, and he consistently demonstrated a genuine interest in my academic and career goals. He is an exceptional mentor and I have no doubt that Kevin will improve the lives of many students to come."
                                                
Undergraduate Student B: 
“I am immensely grateful for Kevin's outstanding mentorship, which has enabled me to achieve remarkable learning and growth opportunities that I wouldn't have been able to access otherwise.
Kevin went above and beyond to support my and my fellow mentees' passion, offering us diverse opportunities to explore our interests and linking us up with various research-oriented events, job opportunities, and REUs.                        
Kevin went out of his way in securing funding for me and my fellow undergraduates, demonstrating his deep concern for our academic and personal success.
Kevin exemplifies exceptional teaching and mentorship skills.
Working with Kevin was transformative to my appreciation for computer science and research, largely influencing those passions which I pursue today.
                        
I was honored to work with someone as amazing as Kevin.
Kevin is a major reason that I was able to reach the goals I have achieved today, instilling me with a feeling that I can do what I desire academically if I set my mind to it.”
                                                
Undergraduate Student C: 
“Kevin is a great mentor. At the beginning of the semester, I wasn't very sure what I would like to achieve with my research project. Kevin helped narrow down the scope of my project and proposed what a minimal viable research prototype looked like. Kevin and I would sync up weekly, with extra meetings scheduled on demand. We would discuss the implementation issues I was confronted with, and the plan for next week. His communication was effective, helping me make steady progress on my project and comfortable, never once in a meeting did I feel pushed. It was a perfect balance of motivation and discipline. He had both the technical expertise to provide hands-on and practical suggestions to the problem I'm having, and was patient as a rubber duck listening to me clumsily explain myself. When our opinion diverges, he would “nudge” me in the right direction by forecasting potential issues and hinting at pitfalls. More importantly, Kevin is a caring person. It would not be an overstatement to say that the Ph.D. position I got today owe partly to Kevin. He helped proofread my application and offered advice [...] I was a bit overwhelmed by the heavy course load and application anxiety. Kevin was not shy of opening up and speaking about the challenges he met during his graduate studies, empathizing with and motivating me.” 




Kevin has everything it takes to be a leader in both research and teaching. He has a vision. He's independent. He's driven, hard-working. He communicates well. He's a perfectionist. He is a better version of Michael Pradel, my former post-doc and now a full professor at the University of Stuttgart, Germany. I give Kevin my strongest recommendation without any reservations for a faculty position in your department.




Sincerely,
 signature 

Koushik Sen
Professor, 
Computer Science Division,
University of California, Berkeley