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

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

1 2 3 ... 5 6 7 next

  1. Aarts, Fides; Jonsson, Bengt; Uijen, Johan; Vaandrager, Frits: Generating models of infinite-state communication protocols using regular inference with abstraction (2015)
  2. Methni, Amira; Lemerre, Matthieu; Ben Hedia, Belgacem; Haddad, Serge; Barkaoui, Kamel: Specifying and verifying concurrent C programs with TLA+ (2015)
  3. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015)
  4. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  5. Giacobazzi, Roberto; Ranzato, Francesco: Correctness kernels of abstract interpretations (2014)
  6. Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki: Automatic termination verification for higher-order functional programs (2014)
  7. Broadbent, Christopher; Carayol, Arnaud; Hague, Matthew; Serre, Olivier: C-SHORe: a collapsible approach to higher-order verification (2013)
  8. Grigore, Radu; Distefano, Dino; Petersen, Rasmus Lerchedahl; Tzevelekos, Nikos: Runtime verification based on register automata (2013)
  9. Kobayashi, Naoki: Model checking higher-order programs (2013)
  10. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  11. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  12. Popeea, Corneliu; Rybalchenko, Andrey: Threader: a verifier for multi-threaded programs. (Competition contribution) (2013)
  13. Simmonds, Jocelyn; Ben-David, Shoham; Chechik, Marsha: Monitoring and recovery for web service applications (2013)
  14. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: Whale: an interpolation-based algorithm for inter-procedural verification (2012)
  15. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)
  16. Bjørner, Nikolaj: Taking satisfiability to the next level with Z3. (Abstract) (2012)
  17. Donaldson, Alastair F.; Kaiser, Alexander; Kroening, Daniel; Tautschnig, Michael; Wahl, Thomas: Counterexample-guided abstraction refinement for symmetric concurrent programs (2012)
  18. Gallardo, M.M.; Joubert, C.; Merino, P.; Sanán, D.: A model-extraction approach to verifying concurrent C programs with CADP (2012)
  19. Hatcliff, John; Leavens, Gary T.; Leino, K.Rustan M.; Müller, Peter; Parkinson, Matthew: Behavioral interface specification languages (2012)
  20. Hoder, Kryštof; Bjørner, Nikolaj: Generalized property directed reachability (2012)

1 2 3 ... 5 6 7 next

Further publications can be found at: