Toolchain

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.


References in zbMATH (referenced in 19 articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Paviotti, Marco; Bengtson, Jesper: Formally verifying exceptions for low-level code with separation logic (2018)
  2. Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
  3. Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
  4. Krebbers, Robbert; Jung, Ralf; Bizjak, Aleš; Jourdan, Jacques-Henri; Dreyer, Derek; Birkedal, Lars: The essence of higher-order concurrent separation logic (2017)
  5. Krebbers, Robbert: A formal C memory model for separation logic (2016)
  6. Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
  7. Naumann, David A.: Towards patterns for heaps and imperative lambdas (2016)
  8. Svendsen, Kasper; Sieczkowski, Filip; Birkedal, Lars: Transfinite step-indexing: decoupling concrete and logical steps (2016)
  9. Tan, Jiaqi; Tay, Hui Jun; Gandhi, Rajeev; Narasimhan, Priya: AUSPICE-R: automatic safety-property proofs for realistic features in machine code (2016)
  10. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  11. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight verifast (2015)
  12. Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)
  13. Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier: Program logics for certified compilers (2014)
  14. 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)
  15. Appel, Andrew W.: Verified software toolchain (2012) ioport
  16. Roşu, Grigore; Ştefănescu, Andrei: From hoare logic to matching logic reachability (2012)
  17. Roşu, Grigore; Ştefănescu, Andrei: Towards a unified theory of operational and axiomatic semantics (2012)
  18. Appel, Andrew W.: Verified software toolchain (invited talk) (2011)
  19. Beringer, Lennart: Relational decomposition (2011)


Further publications can be found at: http://vst.cs.princeton.edu/#papers