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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

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