| The temporal rover and the ATG rover D Drusinsky International SPIN Workshop on Model Checking of Software, 323-330, 2000 | 367 | 2000 |
| Using statecharts for hardware description and synthesis D Drusinsky, D Harel IEEE Transactions on Computer-Aided Design of Integrated Circuits and …, 1989 | 269 | 1989 |
| Modeling and verification using UML statecharts: a working guide to reactive system design, Runtime Monitoring and Execution-based Model Checking D Drusinsky Elsevier, 2011 | 203* | 2011 |
| Experimental evaluation of verification and validation tools on martian rover software G Brat, D Drusinsky, D Giannakopoulou, A Goldberg, K Havelund, ... Formal Methods in System Design 25 (2), 167-198, 2004 | 119 | 2004 |
| On the power of bounded concurrency I: Finite automata D Drusinsky, D Harel Journal of the ACM (JACM) 41 (3), 517-539, 1994 | 112 | 1994 |
| Experiments with test case generation and runtime analysis C Artho, D Drusinksy, A Goldberg, K Havelund, M Lowry, C Pasareanu, ... International Workshop on Abstract State Machines, 87-108, 2003 | 83 | 2003 |
| Monitoring temporal rules combined with time series D Drusinsky International Conference on Computer Aided Verification, 114-117, 2003 | 72 | 2003 |
| Implementing a finite state machine using concurrent finite state machines with delayed communications and no shared control signals D Drusinsky US Patent App. 09/825,138, 2002 | 70 | 2002 |
| A visual tradeoff space for formal verification and validation techniques D Drusinsky, JB Michael, MT Shing IEEE Systems Journal 2 (4), 513-519, 2008 | 34 | 2008 |
| A state assignment procedure for single-block implementation of state charts D Drusinsky-Yoresh IEEE transactions on computer-aided design of integrated circuits and …, 1991 | 33 | 1991 |
| Electronic controller based on the use of state charts as an abstract model D Drusinsky, D Harel US Patent 4,799,141, 1989 | 32 | 1989 |
| Verification and validation for trustworthy software systems JB Michael, D Drusinsky, TW Otani, MT Shing IEEE software 28 (6), 86-92, 2011 | 31 | 2011 |
| Semantics and runtime monitoring of tlcharts: Statechart automata with temporal logic conditioned transitions D Drusinsky Electronic Notes in Theoretical Computer Science 113, 3-21, 2005 | 31 | 2005 |
| Validating UML statechart-based assertions libraries for improved reliability and assurance D Drusinsky, JB Michael, TW Otani, MT Shing 2008 Second International Conference on Secure System Integration and …, 2008 | 28 | 2008 |
| Creating and validating embedded assertion statecharts D Drusinsky, MT Shing, KA Demir IEEE Distributed Systems Online 8 (5), 3-3, 2007 | 28 | 2007 |
| On the power of cooperative concurrency D Drusinsky, D Harel International Conference on Concurrency, 74-103, 1988 | 27 | 1988 |
| Specification, validation and run-time monitoring of soa based system-of-systems temporal behaviors TS Cook, D Drusinksy, MT Shing 2007 IEEE International Conference on System of Systems Engineering, 1-6, 2007 | 26 | 2007 |
| Extended state diagrams and reactive systems D Drusinsky | 24 | 1994 |
| Creation and validation of embedded assertion statecharts D Drusinsky, MT Shing, KA Demir Seventeenth IEEE International Workshop on Rapid System Prototyping (RSP'06 …, 2006 | 23 | 2006 |
| Monitoring temporal logic specifications combined with time series constraints D Drusinsky, MT Shing | 22 | 2003 |
David HarelProfessor of Computer Science, The Weizmann InstituteVerified email at weizmann.ac.il
