3 papers
cs.PL2025
Verified VCG and Verified Compiler for Dafny
Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan
Dafny is a verification-aware programming language that comes with a compiler and static program verifier. However, neither the compiler nor the verifier is proved correct; in fact…
cs.LG2025
Efficient Certified Reasoning for Binarized Neural Networks
Jiong Yang, Yong Kiam Tan, Mate Soos +2
Neural networks have emerged as essential components in safety-critical applications -- these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNN…
cs.LO2024
Formally Certified Approximate Model Counting
Yong Kiam Tan, Jiong Yang, Mate Soos +2
Approximate model counting is the task of approximating the number of solutions to an input Boolean formula. The state-of-the-art approximate model counter for formulas in conjunct…