Applications of Formal and Semi-formal Verification on Software Testing, High-level Synthesis and Energy Internet

Speaker: Min Gao
Affiliation: Ph.D. Candidate - UCLA

Abstract: Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property. With the increasing power of computers and advances in constraint solving technologies, formal and semi-formal verification have received great attentions on many applications.

In this talk, we describe the applications of formal and semi-formal verification in three different fields. In software testing field, we improve concolic testing by bounded model checking (BMC). During concolic testing, we identify program regions that can be encoded by BMC on-the-fly so that program paths within these regions are checked simultaneously. Our implementation LLSPLAT shows on average 16% relative branch coverage improvement on the GNU Coreutils set.

In High-level Synthesis (HLS) field, we propose a functional verification flow for HLS utilizing symbolic execution on both C and Verilog directly. On the Verilog level, we design a light-weight pure symbolic execution framework to collect Verilog’s time invariant version-based traces. Extensive experiments on circuits from numerical computing and CHStone benchmark verify the validity and effectiveness of the flow.

In the energy internet filed, we provide probabilistic model checking solutions for investigating energy router (ER) based system’s reliability and quantitative properties by proposing continuous-time Markov chain and Markov decision process models. Extensive experiments verify the effectiveness of the proposed models.

Biography:  Min Gao is currently a Ph.D. candidate in the Department of Electrical and Computer Engineering under the mentorship of Professor Lei He. He received the M.S. degree in electrical engineering in 2012 from UCLA, and B.E. degree in electrical engineering and automation from Nanjing University of Technology, Nanjing, China, in 2011. He was a visiting scholar with Max Planck Institute for Software Systems, Kaiserslautern, Germany, and State Key Laboratory of VLSI and Systems, Fudan University, Shanghai, China. He also worked as an intern in Synopsys, Fudan Microelectronics and Google.

For more information contact Professor Lei He (lhe@ee.ucla.edu)

Date/Time:
Date(s) - May 24, 2018
11:45 am - 1:45 pm

Location:
E-IV Faraday Room #67-124
420 Westwood Plaza - 6th Flr., Los Angeles CA 90095