| Syntax-guided synthesis R Alur, R Bodik, G Juniwal, MMK Martin, M Raghothaman, SA Seshia, ... 2013 Formal Methods in Computer-Aided Design, 1-8, 2013 | 1133 | 2013 |
| Kodkod: A relational model finder E Torlak, D Jackson International Conference on Tools and Algorithms for the Construction and …, 2007 | 701 | 2007 |
| A lightweight symbolic virtual machine for solver-aided host languages E Torlak, R Bodik ACM SIGPLAN Notices 49 (6), 530-541, 2014 | 342 | 2014 |
| Growing solver-aided languages with rosette E Torlak, R Bodik Proceedings of the 2013 ACM international symposium on New ideas, new …, 2013 | 337 | 2013 |
| Angelic debugging S Chandra, E Torlak, S Barman, R Bodik Proceedings of the 33rd International Conference on Software Engineering …, 2011 | 190 | 2011 |
| {Push-Button} verification of file systems via crash refinement H Sigurbjarnarson, J Bornholt, E Torlak, X Wang 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2016 | 178 | 2016 |
| Hyperkernel: Push-button verification of an OS kernel L Nelson, H Sigurbjarnarson, K Zhang, D Johnson, J Bornholt, E Torlak, ... Proceedings of the 26th Symposium on Operating Systems Principles, 252-269, 2017 | 171 | 2017 |
| Scaling symbolic evaluation for automated verification of systems code with Serval L Nelson, J Bornholt, R Gu, A Baumann, E Torlak, X Wang Proceedings of the 27th ACM Symposium on Operating Systems Principles, 225-242, 2019 | 169 | 2019 |
| Controlled physical random functions and applications B Gassend, MV Dijk, D Clarke, E Torlak, S Devadas, P Tuyls ACM Transactions on Information and System Security (TISSEC) 10 (4), 1-22, 2008 | 151 | 2008 |
| Optimizing synthesis with metasketches J Bornholt, E Torlak, D Grossman, L Ceze Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016 | 133 | 2016 |
| Finding minimal unsatisfiable cores of declarative specifications E Torlak, FSH Chang, D Jackson International symposium on formal methods, 326-341, 2008 | 122 | 2008 |
| Specifying and checking file system crash-consistency models J Bornholt, A Kaufmann, J Li, A Krishnamurthy, E Torlak, X Wang Proceedings of the Twenty-First International Conference on Architectural …, 2016 | 114 | 2016 |
| MemSAT: checking axiomatic specifications of memory models E Torlak, M Vaziri, J Dolby ACM Sigplan Notices 45 (6), 341-350, 2010 | 104 | 2010 |
| A constraint solver for software engineering: finding models and cores of large relational specifications E Torlak Massachusetts Institute of Technology, 2009 | 103 | 2009 |
| Scalable verification of border gateway protocol configurations with an SMT solver K Weitz, D Woos, E Torlak, MD Ernst, A Krishnamurthy, Z Tatlock Proceedings of the 2016 acm sigplan international conference on object …, 2016 | 102 | 2016 |
| Specification and verification in the field: Applying formal methods to {BPF} just-in-time compilers in the linux kernel L Nelson, J Van Geffen, E Torlak, X Wang 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2020 | 95 | 2020 |
| Synthesizing memory models from framework sketches and litmus tests J Bornholt, E Torlak ACM SIGPLAN Notices 52 (6), 467-481, 2017 | 89 | 2017 |
| Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design R Alur, R Bodik, G Juniwal, MMK Martin, M Raghothaman, SA Seshia, ... IEEE, 1ś8, 2013 | 81 | 2013 |
| Effective interprocedural resource leak detection E Torlak, S Chandra Proceedings of the 32nd ACM/IEEE International Conference on Software …, 2010 | 81 | 2010 |
| Nickel: A framework for design and verification of information flow control systems H Sigurbjarnarson, L Nelson, B Castro-Karney, J Bornholt, E Torlak, ... 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2018 | 76 | 2018 |