On the verification problem for weak memory models MF Atig, A Bouajjani, S Burckhardt, M Musuvathi Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2010 | 158 | 2010 |
Stateless model checking for TSO and PSO PA Abdulla, S Aronis, MF Atig, B Jonsson, C Leonardsson, K Sagonas Acta Informatica 54 (8), 789-818, 2017 | 119 | 2017 |
String constraints for verification PA Abdulla, MF Atig, YF Chen, L Holík, A Rezine, P Rümmer, J Stenman International Conference on Computer Aided Verification, 150-166, 2014 | 82 | 2014 |
Dense-timed pushdown automata PA Abdulla, MF Atig, J Stenman 2012 27th Annual IEEE Symposium on Logic in Computer Science, 35-44, 2012 | 79 | 2012 |
Emptiness of multi-pushdown automata is 2ETIME-complete MF Atig, B Bollig, P Habermehl International Conference on Developments in Language Theory, 121-133, 2008 | 74 | 2008 |
Getting rid of store-buffers in TSO analysis MF Atig, A Bouajjani, G Parlato International Conference on Computer Aided Verification, 99-115, 2011 | 70 | 2011 |
Norn: An SMT solver for string constraints PA Abdulla, MF Atig, YF Chen, L Holík, A Rezine, P Rümmer, J Stenman International Conference on Computer Aided Verification, 462-469, 2015 | 68 | 2015 |
Counter-example guided fence insertion under TSO PA Abdulla, MF Atig, YF Chen, C Leonardsson, A Rezine International Conference on Tools and Algorithms for the Construction and …, 2012 | 66 | 2012 |
Context-bounded analysis for concurrent programs with dynamic creation of threads MF Atig, A Bouajjani, S Qadeer International Conference on Tools and Algorithms for the Construction and …, 2009 | 60 | 2009 |
On the reachability analysis of acyclic networks of pushdown systems MF Atig, A Bouajjani, T Touili International Conference on Concurrency Theory, 356-371, 2008 | 51 | 2008 |
Stateless model checking for POWER PA Abdulla, MF Atig, B Jonsson, C Leonardsson International Conference on Computer Aided Verification, 134-156, 2016 | 49 | 2016 |
Context-bounded analysis for concurrent programs with dynamic creation of threads MF Atig, A Bouajjani, S Qadeer arXiv preprint arXiv:1111.1011, 2011 | 49 | 2011 |
What’s decidable about weak memory models? MF Atig, A Bouajjani, S Burckhardt, M Musuvathi European Symposium on Programming, 26-46, 2012 | 45 | 2012 |
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO PA Abdulla, MF Atig, YF Chen, C Leonardsson, A Rezine International Conference on Tools and Algorithms for the Construction and …, 2013 | 39 | 2013 |
Flatten and conquer: a framework for efficient analysis of string constraints PA Abdulla, MF Atig, YF Chen, BP Diep, L Holík, A Rezine, P Rümmer ACM SIGPLAN Notices 52 (6), 602-617, 2017 | 37 | 2017 |
Optimal stateless model checking under the release-acquire semantics PA Abdulla, MF Atig, B Jonsson, TP Ngo Proceedings of the ACM on Programming Languages 2 (OOPSLA), 1-29, 2018 | 36 | 2018 |
On Yen's path logic for Petri nets MF Atig, P Habermehl International Journal of Foundations of Computer Science 22 (04), 783-799, 2011 | 35 | 2011 |
Automatic fence insertion in integer programs via predicate abstraction PA Abdulla, MF Atig, YF Chen, C Leonardsson, A Rezine International Static Analysis Symposium, 164-180, 2012 | 33 | 2012 |
Detecting fair non-termination in multithreaded programs MF Atig, A Bouajjani, M Emmi, A Lal International Conference on Computer Aided Verification, 210-226, 2012 | 33 | 2012 |
The best of both worlds: Trading efficiency and optimality in fence insertion for TSO PA Abdulla, MF Atig, TP Ngo European Symposium on Programming Languages and Systems, 308-332, 2015 | 31 | 2015 |