| Model checking EM Clarke Foundations of Software Technology and Theoretical Computer Science: 17th …, 1997 | 15954 | 1997 |
| Automatic verification of finite-state concurrent systems using temporal logic specifications EM Clarke, EA Emerson, AP Sistla ACM Transactions on Programming Languages and Systems (TOPLAS) 8 (2), 244-263, 1986 | 6352 | 1986 |
| Design and synthesis of synchronization skeletons using branching time temporal logic EM Clarke, EA Emerson Workshop on logic of programs, 52-71, 1981 | 5126 | 1981 |
| Symbolic model checking: 1020 states and beyond JR Burch, EM Clarke, KL McMillan, DL Dill, LJ Hwang Information and computation 98 (2), 142-170, 1992 | 4684 | 1992 |
| Symbolic model checking without BDDs A Biere, A Cimatti, E Clarke, Y Zhu Tools and Algorithms for the Construction and Analysis of Systems: 5th …, 1999 | 3468 | 1999 |
| Counterexample-guided abstraction refinement E Clarke, O Grumberg, S Jha, Y Lu, H Veith Computer Aided Verification: 12th International Conference, CAV 2000 …, 2000 | 2679 | 2000 |
| Nusmv 2: An opensource tool for symbolic model checking A Cimatti, E Clarke, E Giunchiglia, F Giunchiglia, M Pistore, M Roveri, ... Computer Aided Verification: 14th International Conference, CAV 2002 …, 2002 | 2595 | 2002 |
| Model checking and abstraction EM Clarke, O Grumberg, DE Long ACM transactions on Programming Languages and Systems (TOPLAS) 16 (5), 1512-1542, 1994 | 2385 | 1994 |
| Formal methods: State of the art and future directions EM Clarke, JM Wing ACM Computing Surveys (CSUR) 28 (4), 626-643, 1996 | 2272 | 1996 |
| A tool for checking ANSI-C programs E Clarke, D Kroening, F Lerda Tools and Algorithms for the Construction and Analysis of Systems: 10th …, 2004 | 1971 | 2004 |
| Bounded model checking A Biere Handbook of satisfiability, 739-764, 2021 | 1722 | 2021 |
| The complexity of propositional linear temporal logics AP Sistla, EM Clarke Journal of the ACM (JACM) 32 (3), 733-749, 1985 | 1696 | 1985 |
| Counterexample-guided abstraction refinement for symbolic model checking E Clarke, O Grumberg, S Jha, Y Lu, H Veith Journal of the ACM (JACM) 50 (5), 752-794, 2003 | 1331 | 2003 |
| Bounded model checking using satisfiability solving E Clarke, A Biere, R Raimi, Y Zhu Formal methods in system design 19, 7-34, 2001 | 1116 | 2001 |
| Symbolic model checking using SAT procedures instead of BDDs A Biere, A Cimatti, EM Clarke, M Fujita, Y Zhu Proceedings of the 36th annual ACM/IEEE Design Automation Conference, 317-320, 1999 | 1072 | 1999 |
| Using branching time temporal logic to synthesize synchronization skeletons EA Emerson, EM Clarke Science of Computer programming 2 (3), 241-266, 1982 | 1062 | 1982 |
| NuSMV: A new symbolic model verifier A Cimatti, E Clarke, F Giunchiglia, M Roveri Computer Aided Verification: 11th International Conference, CAV’99 Trento …, 1999 | 986 | 1999 |
| NuSMV: a new symbolic model checker A Cimatti, E Clarke, F Giunchiglia, M Roveri International journal on software tools for technology transfer 2, 410-425, 2000 | 961 | 2000 |
| Symbolic model checking for sequential circuit verification JR Burch, EM Clarke, DE Long, KL McMillan, DL Dill IEEE Transactions on Computer-Aided Design of Integrated Circuits and …, 1994 | 860 | 1994 |
| Handbook of model checking EM Clarke, TA Henzinger, H Veith, R Bloem Springer 10, 978-3, 2018 | 807 | 2018 |
Orna GrumbergProfessor of Computer Science, TechnionVerified email at cs.technion.ac.il
