| An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic | 12 | 0.61 | 2015 |
| A Widening Approach to Multithreaded Program Verification. | 13 | 0.61 | 2014 |
| satabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). | 1 | 0.36 | 2012 |
| Counterexample-guided abstraction refinement for symmetric concurrent programs | 12 | 0.57 | 2012 |
| An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic | 40 | 1.46 | 2011 |
| Symmetry-aware predicate abstraction for shared-variable concurrent programs | 28 | 0.93 | 2011 |
| Symmetry-Aware Predicate Abstraction for Shared-Variable Concurrent Programs (Extended Technical Report) | 2 | 0.40 | 2011 |
| Linear completeness thresholds for bounded model checking | 13 | 0.65 | 2011 |
| Beyond quantifier-free interpolation in extensions of Presburger arithmetic | 14 | 0.66 | 2011 |
| Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays. | 6 | 0.41 | 2010 |
| BOOM: taking boolean program model checking one step further | 9 | 0.56 | 2010 |
| Dynamic cutoff detection in parameterized concurrent programs | 54 | 1.40 | 2010 |
| Replication and Abstraction: Symmetry in Automated Formal Verification | 9 | 0.51 | 2010 |
| Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic (Extended Technical Report) | 0 | 0.34 | 2010 |
| Mixed abstractions for floating-point arithmetic | 33 | 1.34 | 2009 |
| Symbolic Counter Abstraction for Concurrent Software | 20 | 0.75 | 2009 |
