There is an interesting paper on external sound static analysis tools (verification tools like SMT and SAT solvers) in Frama-C to increase effectiveness of opti

There is an interesting paper on external sound static analysis tools (verification tools like SMT and SAT solvers) in Frama-C to increase effectiveness of optimizations and generating better, in terms of performance and not just correctness, code. http://link.springer.com/chapter/10.1007/978-3-662-46081-8_17 http://link.springer.com/chapter/10.1007/978-3-662-46081-8_1...