Cogent swMATH ID: 1300 Software Authors: Cook, Byron; Kroening, Daniel; Sharygina, Natasha Description: Cogent: Accurate theorem proving for program verification. Many symbolic software verification engines such as Slam and ESC/Java rely on automatic theorem provers. The existing theorem provers, such as Simplify, lack precise support for important programming language constructs such as pointers, structures and unions. This paper describes a theorem prover, Cogent, that accurately supports all ANSI-C expressions. The prover’s implementation is based on a machine-level interpretation of expressions into propositional logic, and supports finite machine-level variables, bit operations, structures, unions, references, pointers and pointer arithmetic. When used by Slam during the model checking of over 300 benchmarks, Cogent’s improved accuracy reduced the number of Slam timeouts by half, increased the number of true errors found, and decreased the number of false errors Homepage: http://research.microsoft.com/en-us/um/cambridge/projects/terminator/cogent.pdf Related Software: SatAbs; SIMPLIFY; SPIN; Bebop; MiniSat; FOCI; Chaff; SLAM; Yices; Bandera; ASTREE; Java PathFinder; Korat; Zing; ESC/Java; MOCHA; NuSMV; gs2; SOLPS-ITER; Chombo Cited in: 11 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Cogent: Accurate theorem proving for program verification. Zbl 1081.68673Cook, Byron; Kroening, Daniel; Sharygina, Natasha 2005 all top 5 Cited by 31 Authors 6 Kröning, Daniel 3 Sharygina, Natasha 2 Cook, Byron 2 Dorf, Mikhail A. 2 Dorr, Milo R. 2 Ghosh, Debojyoti 2 Hittinger, Jeffrey A. F. 1 Amani, Sidney 1 Biere, Armin 1 Brady, Bryan A. 1 Bryant, Randal E. 1 Chen, Zilin 1 Clarke, Edmund Melson jun. 1 Colella, Phillip 1 Engel, Christian 1 Hähnle, Reiner 1 Jain, Himanshu 1 Klein, Gerwin 1 Leavens, Gary T. 1 Leino, K. Rustan M. 1 Lim, Japheth 1 Müller, Peter 1 Murray, Toby 1 Nagashima, Yutaka 1 O’Connor, Liam 1 Ouaknine, Joel O. 1 Rizkallah, Christine 1 Schwartz, Peter O. 1 Seshia, Sanjit Arunkumar 1 Sewell, Thomas D. 1 Strichman, Ofer Cited in 3 Serials 2 Journal of Computational Physics 1 Formal Aspects of Computing 1 Formal Methods in System Design Cited in 5 Fields 9 Computer science (68-XX) 2 Numerical analysis (65-XX) 1 Mathematical logic and foundations (03-XX) 1 Partial differential equations (35-XX) 1 Fluid mechanics (76-XX) Citations by Year