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 151 articles , 2 standard articles )

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

1 2 3 ... 6 7 8 next

  1. Hajdu, Ákos; Micskei, Zoltán: Efficient strategies for CEGAR-based model checking (2020)
  2. Lu, Xu; Duan, Zhenhua; Tian, Cong; Du, Hongwei: Verify heaps via unified model checking (2020)
  3. Bueno, Denis; Sakallah, Karem A.: EUFORIA: complete software model checking with uninterpreted functions (2019)
  4. Alur, Rajeev; Bouajjani, Ahmed; Esparza, Javier: Model checking procedural programs (2018)
  5. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  6. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  7. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  8. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  9. Dams, Dennis; Grumberg, Orna: Abstraction and abstraction refinement (2018)
  10. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  11. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  12. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  13. Kurshan, Robert P.: Transfer of model checking to industrial practice (2018)
  14. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  15. Greitschus, Marius; Dietsch, Daniel; Podelski, Andreas: Loop invariants from counterexamples (2017)
  16. Kafle, Bishoksan; Gallagher, John P.: Horn clause verification with convex polyhedral abstraction and tree automata-based refinement (2017)
  17. Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits: Generating models of infinite-state communication protocols using regular inference with abstraction (2015)
  18. Methni, Amira; Lemerre, Matthieu; Ben Hedia, Belgacem; Haddad, Serge; Barkaoui, Kamel: Specifying and verifying concurrent C programs with TLA+ (2015) ioport
  19. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  20. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)

1 2 3 ... 6 7 8 next


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