Titlebook: Verified Software: Theories, Tools, Experiments; First IFIP TC 2/WG 2 Bertrand Meyer,Jim Woodcock Book 2008 Springer-Verlag Berlin Heidelbe

较早

啪心儿跳动

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.

胎儿

施魔法

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

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

bisphosphonate

反复无常

IOTA

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.

木讷

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.