较早 发表于 2025-3-25 06:08:29
http://reply.papertrans.cn/99/9818/981749/981749_21.png啪心儿跳动 发表于 2025-3-25 09:15:44
It Is Time to Mechanize Programming Language Metatheory the . challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses.胎儿 发表于 2025-3-25 14:48:33
http://reply.papertrans.cn/99/9818/981749/981749_23.png施魔法 发表于 2025-3-25 18:38:04
A Mini Challenge: Build a Verifiable Filesystemreliable and secure. The paper argues why we believe a filesystem is the right candidate for a mini challenge and describes a project in which we are building a small embedded filesystem for use with flash memory.legislate 发表于 2025-3-25 23:01:06
Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers id to use automatic, but not interactive, verification. The focus of this proposal is to integrate these two approaches into a single theoretical and practical framework, leveraging the benefits of each approach.BOOST 发表于 2025-3-26 02:52:32
http://reply.papertrans.cn/99/9818/981749/981749_26.pngbisphosphonate 发表于 2025-3-26 05:47:48
http://reply.papertrans.cn/99/9818/981749/981749_27.png反复无常 发表于 2025-3-26 09:48:23
http://reply.papertrans.cn/99/9818/981749/981749_28.pngIOTA 发表于 2025-3-26 13:17:14
Software Verification and Software Engineering a Practitioner’s Perspectivefying Compiler..I want to question whether this long-standing challenge is really relevant to the greater goal of achieving trustworthy software. Instead, I suggest that research in verification needs to support a larger effort to improve the software engineering process.木讷 发表于 2025-3-26 17:38:17
Automatic Verification of Strongly Dynamic Software Systemsthe progress we have made in automated verification of strongly dynamic systems using abstract interpretation with three-valued logical structures. We then enumerate a number of challenges that must be tackled in order for such techniques to be widely adopted.