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 | 993 | 2013 |
Kodkod: A relational model finder E Torlak, D Jackson International Conference on Tools and Algorithms for the Construction and …, 2007 | 669 | 2007 |
A lightweight symbolic virtual machine for solver-aided host languages E Torlak, R Bodik ACM SIGPLAN Notices 49 (6), 530-541, 2014 | 301 | 2014 |
Growing solver-aided languages with rosette E Torlak, R Bodik Proceedings of the 2013 ACM international symposium on New ideas, new …, 2013 | 296 | 2013 |
Angelic debugging S Chandra, E Torlak, S Barman, R Bodik Proceedings of the 33rd International Conference on Software Engineering …, 2011 | 184 | 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 | 153 | 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 | 146 | 2017 |
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 | 145 | 2008 |
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 | 126 | 2019 |
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 | 119 | 2016 |
Finding minimal unsatisfiable cores of declarative specifications E Torlak, FSH Chang, D Jackson FM 2008: Formal Methods: 15th International Symposium on Formal Methods …, 2008 | 115 | 2008 |
MemSAT: checking axiomatic specifications of memory models E Torlak, M Vaziri, J Dolby ACM Sigplan Notices 45 (6), 341-350, 2010 | 103 | 2010 |
A constraint solver for software engineering: finding models and cores of large relational specifications E Torlak Massachusetts Institute of Technology, 2009 | 97 | 2009 |
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 | 93 | 2016 |
Synthesizing memory models from framework sketches and litmus tests J Bornholt, E Torlak ACM SIGPLAN Notices 52 (6), 467-481, 2017 | 87 | 2017 |
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 | 87 | 2016 |
Effective interprocedural resource leak detection E Torlak, S Chandra Proceedings of the 32nd ACM/IEEE International Conference on Software …, 2010 | 77 | 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 | 71 | 2018 |
Correct refactoring of concurrent Java code M Schäfer, J Dolby, M Sridharan, E Torlak, F Tip ECOOP 2010–Object-Oriented Programming: 24th European Conference, Maribor …, 2010 | 70 | 2010 |
A type system for object models J Edwards, D Jackson, E Torlak ACM SIGSOFT Software Engineering Notes 29 (6), 189-199, 2004 | 66 | 2004 |