swMATH ID: 9517
Software Authors: Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier
Description: Verified Software Toolchain: The software toolchain includes static analyzers to check assertions about your program; optimizing compilers to translate your program to machine language; operating systems and libraries to supply context for your program. The Verified Software Toolchain project assures with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context.
Homepage: http://vst.cs.princeton.edu/
Related Software: Coq; K Prover; z3; seL4; Charge!; GitHub; VCC; Dafny; Maude; HIP; Rust; VeriFast; Bedrock; Boogie; Smallfoot; HACL*; Infer; Haskell; CompCert; VST-Floyd
Cited in: 30 Publications
Further Publications: http://vst.cs.princeton.edu/#papers

Citations by Year