Sitemap
A list of all the posts and pages found on the site. For you robots out there, there is an XML version available for digesting as well.
Pages
Posts
books
女性的权利
Published:
《女性的权利》(A Vindication of the Rights of Woman)是女性主义先驱玛丽·沃斯通克拉夫特于1792年发表的一部开创性的女权宣言，被视为现代女性主义开山之作。时值法国大革命时期，“人权”观念席卷欧洲，玛丽·沃斯通克拉夫特敏锐地发现，所谓的“人权”并未将女性包含其中，这促使她提笔为女性的权利呐喊。在这部作品中，玛丽·沃斯通克拉夫特犀利地批判了女性教育的重大缺陷，这种教育旨在把女性培养成男性的附属品，而非有尊严的独立个体。她驳斥了女性天生柔弱、理性不足的流行偏见，深刻地指出女性表现出的无知与顺从并非天性，而是后天被剥夺发展机会的结果。她强烈主张女性应当获得与男性同等的理性教育、政治权利和社会地位。作为历史上首部系统性的女性主义著作，《女性的权利》为后世的性别平等进程奠定了思想基石，玛丽沃斯通克拉夫特也因此被公认为现代女性主义思想的开拓者。
当下的力量
Published:
《当下的力量》堪称心灵读物经典，作者埃克哈特·托利指出了我们日常痛苦的主要来源——被大脑思维所控制、焦虑过去和未来而非活在当下。但实际上，我们只能活在当下，活在此时此刻。通过向当下的臣服，你才能找到真正的力量，获得内在的智慧和真正的喜悦。作者在《当下的力量》中提出了几个非常实用的方法，让自己认清时间的幻象，活在当下。《当下的力量》对于普遍焦虑、抑郁、压力大的现代大众读者来说，是一本切实有用的好书，将让我们认清时间的幻象，活在当下，找到真正的力量，发现平和与宁静的入口。
portfolio
publications
Accurate Inference of Termination Conditions
Published in IEEE/ACM 48th International Conference on Software Engineering (ICSE’26), 2026
We present the first approach to infer accurate termination conditions of programs. It builds on a simple but effective framework where non-terminating states are iteratively identified and removed, and a termination prover is employed to validate the current condition. We instantiate the framework with data-driven provers and design a multi-way data sharing mechanism to enhance their interaction. Our proofs show that this method is correct, accurate, terminating, and relatively complete. Additionally, we introduce generalization techniques for recurrent sets to accelerate the iteration process. Evaluation on a benchmark of programs from the literature shows that our implementation significantly outperforms the state-of-the-art tool Acabar, producing much more accurate termination conditions, with the proposed techniques playing a crucial role in speeding up the convergence of the process.
LLM-Guided Loop Bound Generation for Program Termination Verification
Published in the 43rd International Conference on Machine Learning (ICML’26), 2026
Program termination is a fundamental liveness property in software verification. Proving termination of a given program is a formidable challenge due to the undecidability of the problem. In this paper, we propose LIFT, a termination verification framework that leverages LLMs to generate loop bounds within a guess-and-check workflow. LIFT couples this generation with a sound formal validation procedure that both guarantees all reported terminations and refutes invalid loop bounds via violation analysis. Experiments on publicly accessible termination benchmarks show that LIFT significantly outperforms existing termination verification tools.