×

Infer

swMATH ID: 20862
Software Authors: Calcagno, C., Distefano, D.
Description: 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.
Homepage: http://dl.acm.org/citation.cfm?id=1986345
Related Software: Slide; Smallfoot; HIP; Coq; Toolchain; VeriFast; z3; Predator; SLAyer; Viper; GRASShopper; seL4; CVC4; Charge!; jStar; HACL*; TacticToe; Caper; VeriMAP; IncA
Cited in: 13 Publications

Standard Articles

1 Publication describing the Software Year
Infer: An automatic program verifier for memory safety of C programs
Calcagno, Cristiano; Distefano, Dino
2011

Citations by Year