PAGAI swMATH ID: 13095 Software Authors: Julien Henry , David Monniaux , Matthieu Moy Description: PAGAI: A Path Sensitive Static Analyser. We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs. Homepage: http://www.sciencedirect.com/science/article/pii/S1571066112000734 Related Software: Apron; PPL; HyTech; PHAVer; Sawja; ASTREE; 4ti2; polco; efmtool; polymake; Verimag Polyhedra Library; CIL; vZ; BOXES; UFO; SYMBA; Mjollnir; JavaSMT; FOCI; Chaff Cited in: 9 Documents all top 5 Cited by 19 Authors 3 Monniaux, David P. 2 Zaffanella, Enea 1 Aiken, Alex 1 Becchi, Anna 1 Chen, Liqian 1 Hermant, Olivier 1 Irigoin, François 1 Jiang, Jiahong 1 Karpenkov, Egor George 1 Maisonneuve, Vivien 1 Maréchal, Alexandre 1 Mirliaz, Solène 1 Nori, Aditya Vithal 1 Périn, Michael 1 Pichardie, David 1 Sharma, Rahul Kumar 1 Wang, Ji 1 Wendler, Philipp 1 Wu, Xueguang Cited in 1 Serial 1 Information and Computation Cited in 4 Fields 8 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) 1 Convex and discrete geometry (52-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year