| 111 | -- | 143 | Eugene Goldberg, Panagiotis Manolios. Quantifier elimination by dependency sequents |
| 144 | -- | 164 | Jiazhao Xu, Mark Williams, Hari Mony, Jason Baumgartner. Scalable reachability analysis via automated dynamic netlist-based hint generation |
| 165 | -- | 188 | Alessandro Cimatti, Sergio Mover, Stefano Tonetta. Quantifier-free encoding of invariants for hybrid systems |
| 189 | -- | 212 | Alexey Lvov, Luis Alfonso Lastras-Montaño, Barry M. Trager, Viresh Paruthi, Robert Shadowen, Ali El-Zein. Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry |
| 213 | -- | 245 | Martin Brain, Vijay D'Silva, Alberto Griggio, Leopold Haller, Daniel Kroening. Deciding floating-point logic with abstract conflict driven clause learning |
| 246 | -- | 272 | Chao Yan, Mark R. Greenstreet, Suwen Yang. Verifying global start-up for a Möbius ring-oscillator |
| 273 | -- | 301 | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman. Budget-bounded model-checking pushdown systems |