Infer

Infer: An automatic program verifier for memory safety of C programs. Infer is a new automatic program verification tool aimed at proving memory safety of C programs. It attempts to build a compositional proof of the program at hand by composing proofs of its constituent modules (functions/procedures). Bugs are extracted from failures of proof attempts. We describe the main features of Infer and some of the main ideas behind it.


References in zbMATH (referenced in 12 articles , 1 standard article )

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

  1. Garcia-Contreras, Isabel; Morales, José F.; Hermenegildo, Manuel V.: Incremental and modular context-sensitive analysis (2021)
  2. Kimura, Daisuke; Tatsuta, Makoto: Decidability for entailments of symbolic heaps with arrays (2021)
  3. Charguéraud, Arthur; Pottier, François: Temporary read-only permissions for separation logic (2017)
  4. Chen, Taolue; Song, Fu; Wu, Zhilin: Tractability of separation logic with inductive definitions: beyond lists (2017)
  5. Jansen, Christina; Katelaan, Jens; Matheja, Christoph; Noll, Thomas; Zuleger, Florian: Unified reasoning about robustness properties of symbolic-heap separation logic (2017)
  6. Reynolds, Andrew; Iosif, Radu; Serban, Cristina: Reasoning in the Bernays-Schönfinkel-Ramsey fragment of separation logic (2017)
  7. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  8. Gu, Xincai; Chen, Taolue; Wu, Zhilin: A complete decision procedure for linearly compositional separation logic with data constraints (2016)
  9. Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim: A decision procedure for separation logic in SMT (2016)
  10. Demri, Stéphane; Deters, Morgan: Separation logics and modalities: a survey (2015)
  11. Jacobs, Bart; Vogels, Frédéric; Piessens, Frank: Featherweight VeriFast (2015)
  12. Calcagno, Cristiano; Distefano, Dino: Infer: An automatic program verifier for memory safety of C programs (2011) ioport