Interproc is an interprocedural analyzer for a small imperative language with (recursive) procedure calls. It infers invariants on the numerical variables of analyzed program. It it intended as a pedagogical and experimental tool. It also demonstrates the features of the APRON library and the use of the Fixpoint libraries. It is implemented in OCaml.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Sharma, Rahul; Nori, Aditya V.; Aiken, Alex: Bias-variance tradeoffs in program analysis (2014)
- Wu, Xueguang; Chen, Liqian; Wang, Ji: An abstract domain to infer symbolic ranges over nonnegative parameters (2014)
- Amato, Gianluca; Parton, Maurizio; Scozzari, Francesca: Discovering invariants via simple component analysis (2012)
- Vechev, Martin; Yahav, Eran; Raman, Raghavan; Sarkar, Vivek: Automatic verification of determinism for structured parallel programs (2010)
- Amjad, Hasan; Bornat, Richard: Towards automatic stability analysis for rely-guarantee proofs (2009)
- Pélegrin, Marc: The probable evolution of the “air segment” on a medium and a long term basis (1997)