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 ANSIC expressions. The prover’s implementation is based on a machinelevel interpretation of expressions into propositional logic, and supports finite machinelevel 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/enus/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; SOLPSITER; 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.68673 Cook, Byron; Kroening, Daniel; Sharygina, Natasha 
2005

all
top 5
Cited by 31 Authors
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 (68XX) 
2  Numerical analysis (65XX) 
1  Mathematical logic and foundations (03XX) 
1  Partial differential equations (35XX) 
1  Fluid mechanics (76XX) 