General Topics on September 22, 2024

Presenter: Linyu Yang Author: Tom Schrijvers Abstract: Abstract algebra provides powerful design patterns for structuring algorithms and data structures. In particular, once you start looking for the humble monoid structure in programs, you will start seeing it everywhere in one of its many forms.

Presenter: Yutao Sun Authors: Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, Christian Szegedy Abstract: Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs.

Presenter: Zhiyang Li Authors: Haokun Li, Bican Xia & Tianqi Zhao Abstract: Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combinations of polynomial equations and inequalities with integer coefficients and real variables.

Presenter: Xiaqing Zhou Authors: Gerhard Goos, Juris Hartmanis, Elisa Bertino, Wen Gao, Bernhard Steffen, Moti Yung Abstract: CompCert is a formally verified compiler for C that is specified, programmed and proved correct with the Coq proof assistant.

Presenter: Zhongyi Wang Authors: Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang & Patrick Cousot Abstract: When applying abstract interpretation to verification, it may suffer from the problem of getting too conservative over-approximations to verify a given target property, and being hardly able to generate counter-examples when the property does not hold.