You May Also Enjoy
diffViz: Observe “diff” in an aligned visualization
1 minute read
Published:
If I want to explain my Ph.D. work for my nephew in his sixth grade in the simplest way, I would say “I am making software for other computer programmers to understand their program and its behavior”. That would pretty much wrap up my work as I am applying different techniques to convert raw execution traces to meaningful information that brings insight into the actual behavior of the program.
My first exposure to AST instrumentation in Go
6 minute read
Published:
Due to its simplicity and functionality, Go is receiving attention among developers. However, there are not that many tools to focus on the correctness of Go concurrency. Two recent Go static verification papers (1, 2) extract a system of type equations from the Go source code SSA IR 1 equivalent. A calculus mirrors channel-based behaviors of Go programs (goroutines, functions, channel create/communicate/close, etc.) in the form of mutually recursive definitions. Table1 explains the syntax of MiGo. The behavioral typing system derives from MiGo can be checked for liveness and safety in three steps:
Single Static Assignment (SSA) is a form property of Intermediate Representation (IR), which requires that each variable assigned precisely once. Go has a package that generates SSA IR from source. ↩