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.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
- Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
- Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier: Program logics for certified compilers (2014)
- Amtoft, Torben; Dodds, Josiah; Zhang, Zhi; Appel, Andrew; Beringer, Lennart; Hatcliff, John; Ou, Xinming; Cousino, Andrew: A certificate infrastructure for machine-checked proofs of conditional information flow (2012)
- Roşu, Grigore; Ştefănescu, Andrei: Towards a unified theory of operational and axiomatic semantics (2012)
- Roşu, Grigore; Ştefănescu, Andrei: From hoare logic to matching logic reachability (2012)
Further publications can be found at: http://vst.cs.princeton.edu/#papers