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 25 articles )

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

1 2 next

  1. Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben: Safe functional systems through integrity types and verified assembly (2021)
  2. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David: System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (2020)
  3. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (2019)
  4. Ştefănescu, Andrei; Ciobâcă, Stefan; Mereuta, Radu; Moore, Brandon; Roşu, Grigore; Şerbănuṭă, Traian Florin: All-path reachability logic (2019)
  5. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
  6. Jung, Ralf; Krebbers, Robbert; Jourdan, Jacques-Henri; Bizjak, Aleš; Birkedal, Lars; Dreyer, Derek: Iris from the ground up: a modular foundation for higher-order concurrent separation logic (2018)
  7. Paviotti, Marco; Bengtson, Jesper: Formally verifying exceptions for low-level code with separation logic (2018)
  8. Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
  9. Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael: Verified characteristic formulae for CakeML (2017)
  10. Krebbers, Robbert; Jung, Ralf; Bizjak, Aleš; Jourdan, Jacques-Henri; Dreyer, Derek; Birkedal, Lars: The essence of higher-order concurrent separation logic (2017)
  11. Krebbers, Robbert: A formal C memory model for separation logic (2016)
  12. Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
  13. Naumann, David A.: Towards patterns for heaps and imperative lambdas (2016)
  14. Svendsen, Kasper; Sieczkowski, Filip; Birkedal, Lars: Transfinite step-indexing: decoupling concrete and logical steps (2016)
  15. Tan, Jiaqi; Tay, Hui Jun; Gandhi, Rajeev; Narasimhan, Priya: AUSPICE-R: automatic safety-property proofs for realistic features in machine code (2016)
  16. Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
  17. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight VeriFast (2015)
  18. Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)
  19. Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier: Program logics for certified compilers (2014)
  20. 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)

1 2 next


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