SLAM

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine.


References in zbMATH (referenced in 145 articles , 2 standard articles )

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

1 2 3 ... 6 7 8 next

  1. Alur, Rajeev; Bouajjani, Ahmed; Esparza, Javier: Model checking procedural programs (2018)
  2. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  3. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  4. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  5. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  6. Dams, Dennis; Grumberg, Orna: Abstraction and abstraction refinement (2018)
  7. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  8. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  9. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  10. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)
  11. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  12. Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
  13. Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits: Generating models of infinite-state communication protocols using regular inference with abstraction (2015)
  14. Methni, Amira; Lemerre, Matthieu; Ben Hedia, Belgacem; Haddad, Serge; Barkaoui, Kamel: Specifying and verifying concurrent C programs with TLA+ (2015) ioport
  15. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  16. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  17. Giacobazzi, Roberto; Ranzato, Francesco: Correctness kernels of abstract interpretations (2014)
  18. Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki: Automatic termination verification for higher-order functional programs (2014)
  19. Broadbent, Christopher; Carayol, Arnaud; Hague, Matthew; Serre, Olivier: C-SHORe: a collapsible approach to higher-order verification (2013)
  20. Grigore, Radu; Distefano, Dino; Petersen, Rasmus Lerchedahl; Tzevelekos, Nikos: Runtime verification based on register automata (2013)

1 2 3 ... 6 7 8 next


Further publications can be found at: http://research.microsoft.com/en-us/projects/slam/